Information Technology Reference
In-Depth Information
3 LTL
FO
—Formal Definitions and Notation
Let us now introduce our first-order specification language LTL
FO
and related concepts
in more detail. The first concept we need is that of a
sorted first-order signature
,given
as
Γ
=(
S
,
F
,
R
),where
S
is a finite non-empty set of sorts,
F
a finite set of function
symbols and
R
=
U
∪
I
a finite set of a priori uninterpreted and interpreted predicate
symbols, s.t.
U
. The former set of predicate symbols are
referred to as
U
-operators and the latter as
I
-operators. As is common, 0-ary functions
symbols are also referred to as constant symbols. We assume that all operators in
Γ
have a given arity that ranges over the sorts given by
S
, respectively. We also assume an
infinite supply of variables,
V
, that also range over
S
and where
V
∩
I
=
∅
and
R
∩
F
=
∅
∩
(
F
∪
R
)=
∅
.Let
us refer to the first-order language determined by
Γ
as
L
(
Γ
). While
terms
in
L
(
Γ
) are
L
(
Γ
) are defined as follows:
made up of variables and function symbols,
formulae
of
ϕ
::=
p
(
t
1
,...,t
n
)
|
r
(
t
1
,...,t
n
)
|¬
ϕ
|
ϕ
∧
ϕ
|
X
ϕ
|
ϕ
U
ϕ
|∀
(
x
1
,...,x
n
):
p. ϕ,
where
t
1
,...,t
n
are terms,
p
∈
U
,
r
∈
I
,and
x
1
,...,x
n
∈
V
. As variables are sorted,
in the quantified formula
∀
(
x
1
,...,x
n
):
p.ϕ
,the
U
-operator
p
with arity
τ
1
×
...
×
τ
n
,
defines the sorts of variables
x
1
,...,x
n
to be
τ
1
,...,τ
n
, with
τ
i
∈
S
, respectively. For
terms
t
1
,...,t
n
, we say that
p
(
t
1
,...,t
n
) is well-sorted if the sort of every
t
i
is
τ
i
.
This notion is inductively applicable to terms. Moreover, we consider only well-sorted
formulae and refer to the set of all well-sorted
(
Γ
) formulae over a signature
Γ
in
terms of LTL
F
Γ
. When a specific
Γ
is either irrelevant or clear from the context, we will
simply write LTL
FO
instead. When convenient and a certain index is of no importance
in the given context, we also shorten notation of a vector (
x
1
,...,x
n
) by a (bold)
x
.
A
Γ
-structure
,orjust
first-order structure
is a pair
L
A
=(
|
A
|
,I
),where
|
A
|
=
|
A
|
1
∪
...
|
A
|
i
is either a non-
empty finite or countable set (e.g., set of all integers or strings) and
I
an interpretation.
I
assigns to each sort
τ
i
∈
∪|
A
|
n
, is a non-empty set called domain, s.t. every sub-domain
S
a specific sub-domain
τ
i
=
|
A
|
i
, to each function symbol
f
∈
F
of arity
τ
1
×
...
×
τ
l
−→
τ
m
a function
f
I
:
|
A
|
1
×
...
×|
A
|
l
−→ |
A
|
m
,and
to every
I
-operator
r
with arity
τ
1
× ...× τ
m
a relation
r
I
⊆|
A
|
1
× ...×|
A
|
m
.We
restrict ourselves to computable relations and functions. In that regard, we can think
of
I
as a mapping between
I
-operators (resp. function symbols) and the corresponding
algorithms which compute the desired return values, each conforming to the symbols'
respective arities. Note that the interpretation of
U
-operators is rather different from
I
-operators, as it is closely tied to what we call a trace and therefore discussed after we
introduce the necessary notions and notation.
We model observed system behaviour in terms of
actions
:Let
p
∈
U
with arity
τ
1
×
...
×|
A
|
m
, then we call (
p,
d
) an
action
. We refer to finite
sets of actions as
events
. A system's behaviour is therefore a finite
trace
of events, which
we also denote as a sequence of sets of ground terms
×
τ
m
and
d
∈
D
p
=
|
A
|
1
×
...
{
sms
(1234)
}{
login
(“user”)
}
...
when we mean the sequence of tuples
{
(
sms,
1234)
}{
(
login,
“user”)
}
...
Therefore
the occurrence of some action
sms
(1234) in the trace at position
i
∈
N
0
, written
sms
(1234)
w
i
, indicates that, at time
i
,
sms
(1234) holds (or, from a practical point
of view, an SMS was sent to number 1234). We follow the convention that only sym-
bols from
U
appear in a trace, which therefore gives these symbols their respective
interpretations. The following formalises this notion.
∈
