Document 240987

Sample PTL Axioms
What is TL?
Temporal Logic
⊢
Axioms
⊢ (start ⇒
Normal Form
[Esoterica]
(A ⇒ B ) ⇒ (
A⇒
B)
Characterising TL
A) ⇒
A
¨
Buchi
Automata
⊢
Fixpoints
Quantification
⊢
¬A ⇔ ¬ ♦ A
❤(A ∧ B ) ⇔ ❤A ∧
❤B
⊢ AU(B ∧ AUC ) ⇒ AUC
Michael Fisher
Department of Computer Science, University of Liverpool, UK
Key axiom describing how this form of temporal logic works
is the induction axiom:
[[email protected]]
⊢
(ϕ ⇒ ❤ϕ) ⇒ (ϕ ⇒
ϕ)
An Introduction to Practical Formal Methods Using Temporal Logic
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 1 / 20
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
What is Temporal Logic?
What is TL?
Axioms
Characterising TL
Normal Form
Now that we have seen both syntax and semantics for PTL,
together with a variety of examples expressed in its
language, we can reconsider the more philosophical question
Fixpoints
“what is temporal logic?”
What is TL?
Axioms
Characterising TL
Normal Form
Fixpoints
Quantification
Quantification
While we have given a formal description of the PTL logic,
there are a number of alternative formalisations providing
different, and interesting, ways to view PTL.
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 2 / 20
– 3 / 20
“PTL corresponds to a specific, decidable
(PSPACE-complete) fragment of classical
first-order logic (with arithmetic operations).”
As above,
i |=
start
is represented by
i =0
i |=
❤p
is represented by
p(i + 1)
i |=
♦p
is represented by
∃j . ( j ≥ i ) ∧ p ( j )
is represented by
∀j . ( j ≥ i ) ⇒ p ( j )
i |=
In the following we will briefly examine a few of these, as
this is useful in shedding light on the precise nature of
(propositional) temporal logic.
c
Michael
Fisher
LOGIC : ESOTERICA ]
1: PTL as First-Order Logic
¨
Buchi
Automata
¨
Buchi
Automata
[ TEMPORAL
c
Michael
Fisher
p
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 4 / 20
Example
What is TL?
Axioms
What is TL?
Using the above translation,
Characterising TL
Characterising TL
♦q
Normal Form
¨
Buchi
Automata
Fixpoints
¨
Buchi
Automata
now becomes
Recall that the key axiom describing how PTL works is the
(ϕ ⇒ ❤ϕ) ⇒ (ϕ ⇒
ϕ)
induction axiom: ⊢
Fixpoints
Quantification
Quantification
∀i .
“PTL captures a simple form of arithmetical induction.”
Axioms
q ⇒
Normal Form
2: PTL Characterises Induction
(∀j . (j ≥ i ) ⇒ q (j ))
⇒
(∃k . (k ≥ i ) ∧ q (k ))
As we saw above, this can be described as
[ϕ(0) ∧ ∀i . ϕ(i ) ⇒ ϕ(i + 1)] ⇒ ∀j . ϕ(j )
This should now be familiar as the arithmetical induction
principle, i.e. if we can
Through some (first-order) logical manipulation this can be
shown to be true as long as quantification occurs over a
non-empty domain.
1. show ϕ(0), and
2. show that, for any i , if we already know ϕ(i ) then we can
establish ϕ(i + 1)
Since the domain here corresponds to the set of moments in
time, then the domain should actually be infinite.
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 5 / 20
then ϕ(i ) is true for all elements, i , of the domain.
c
Michael
Fisher
Induction Axiom Again
What is TL?
Axioms
Characterising TL
¨
Buchi
Automata
Fixpoints
Quantification
What is TL?
So, re-using the translations above:
Characterising TL
Axioms
LOGIC : ESOTERICA ]
– 7 / 20
“PTL can be seen as a multi-modal logic, comprising
two modalities, [1] and [∗], which interact closely.”
Normal Form
i |= ❤p
i |= ♦ p
p
i |=
→
→
→
p(i + 1)
∃j . ( j ≥ i ) ∧ p ( j )
∀j . ( j ≥ i ) ⇒ p ( j )
¨
Buchi
Automata
Fixpoints
Quantification
In our syntax, ‘[1]’ is usually represented as ‘ ❤’, while ‘[∗]’ is
usually represented as ‘ ’. So, the induction axiom in PTL
⊢
The Induction Axiom can be translated as
ϕ)
⊢ [∗](ϕ ⇒ [1]ϕ) ⇒ (ϕ ⇒ [∗]ϕ)
which easily transforms into
in a modal logic with two modalities.
[ϕ(0) ∧ ∀i . ϕ(i ) ⇒ ϕ(i + 1)] ⇒ ∀j . ϕ(j )
An Introduction to Practical Formal Methods Using Temporal Logic
(ϕ ⇒ ❤ϕ) ⇒ (ϕ ⇒
can now be viewed as the interaction axiom
[∀i . ϕ(i ) ⇒ ϕ(i + 1)] ⇒ [ϕ(0) ⇒ ∀j . ϕ(j )]
c
Michael
Fisher
[ TEMPORAL
3: PTL as a Multi-Modal Logic
One way to view PTL logic is as a fragment of classical logic.
Normal Form
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
There are here two distinct accessibility relations, but [∗]
represents the reflexive transitive closure of [1].
– 6 / 20
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 8 / 20
4: PTL Describes Sequences
What is TL?
Normal Form for PTL
What is TL?
“PTL can be thought of as a logic over sequences.”
Axioms
Axioms
Characterising TL
Characterising TL
Normal Form
¨
Buchi
Automata
As mentioned earlier, the models for PTL are infinite
sequences.
Normal Form
¨
Buchi
Automata
Fixpoints
Quantification
Fixpoints
So, a sequence-based semantics can be given for PTL:
si , si +1 , . . . |= ❤p
si , si +1 , . . . |=
si , si +1 , . . . |=
♦p
p
Quantification
It is often useful to replace one complex formula by several
simpler formulae. We will use a particular normal form
where PTL formulae are represented by
if, and only if, si +1 , . . . |= p
n
^
if, and only if, there exists a j ≥ i
such that sj , . . . |= p
where each of the Ri , termed a rule, is an implication in the
style
if, and only if, for all j ≥ i
then sj , . . . |= p
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 9 / 20
formula about current behaviour
⇒
formula about current and future behaviour
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
5: PTL Describes ω-automata
What is TL?
Axioms
Characterising TL
Axioms
Characterising TL
Fixpoints
Quantification
¨
Buchi
Automata
Fixpoints
[ TEMPORAL
LOGIC : ESOTERICA ]
– 11 / 20
r
_
(an initial rule)
lb
b=1
g
^
ka
⇒
❤
a=1
formulae such as
(p ⇒ ❤q ) give constraints on
possible transitions between automaton states;
formulae such as
♦ r give constraints on accepting
states within an automaton, i.e. states that must be
visited infinitely often; and
formulae such as s ⇒
t describe global invariants
within an automaton.
An Introduction to Practical Formal Methods Using Temporal Logic
start ⇒
Quantification
Correspondingly, temporal formulae might be used to
describe certain automata. Intuitively:
c
Michael
Fisher
LOGIC : ESOTERICA ]
Separated Normal Form (SNF) additionally restricts each Ri
to be of one of the following forms
Normal Form
Models of PTL can be seen as strings accepted by a class of
¨
finite automata — Buchi
Automata.
[ TEMPORAL
Separated Normal Form
What is TL?
“PTL can be seen as a syntactic characterisation of
certain finite-state automata over infinite words.”
Normal Form
¨
Buchi
Automata
Ri
i =1
In this way, PTL can be seen as a logic for describing such
infinite sequences.
c
Michael
Fisher
PTL formulae can become quite complex and difficult to
understand.
g
^
r
_
lb
(a step rule)
b=1
ka
⇒
♦l
(a sometime rule)
a=1
Note, here, that each ka , lb , or l is simply a literal.
– 10 / 20
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 12 / 20
Examples
What is TL?
Axioms
Characterising TL
What is TL?
The example formulae below correspond to the three
different types of SNF rules.
Axioms
Characterising TL
Normal Form
¨
Buchi
Automata
Fixpoints
Quantification
Example Automaton (1)
Consider the formula ‘ ❤(a ∨ ❤b)’. We can generate a
corresponding automaton:
Normal Form
I NITIAL :
S TEP :
S OMETIME :
start ⇒ losing ∨ hopeful
(losing ∧ ¬hopeful ) ⇒ ❤losing
hopeful ⇒ ♦ ¬losing
¨
Buchi
Automata
Fixpoints
Quantification
i
s0
a
s1
b
Any PTL formula can be transformed into a set of SNF rules
that have (essentially) equivalent behaviours at the expense
of only a polynomial increase in both the size of the
representation and the number of atomic propositions used
within the representation.
s2
Notation: ‘i ’ represents an initial state and a double circle
represents an accepting state (one of which must be visited
infinitely often).
An edge with no label accepts any value.
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 13 / 20
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
¨
Buchi
Automata and PTL
What is TL?
Axioms
Characterising TL
Normal Form
¨
Buchi
Automata
Fixpoints
LOGIC : ESOTERICA ]
– 15 / 20
Example Automaton (2)
Models for PTL are essentially infinite, discrete, linear
sequences, with an identified start state.
What is TL?
Thus, each temporal formula corresponds to a set of models
on which that formula is satisfied.
Normal Form
Axioms
Characterising TL
Quantification
[ TEMPORAL
a’ has more
The automaton translation of the formula ‘
interesting infinite behaviour:
¨
Buchi
Automata
Fixpoints
Quantification
s0
Now, look again at these models. See them as strings.
a
a
i
Viewing models as strings allows us to utilise the large
amount of previous work on finite automata.
In particular, we can define a finite automaton that accepts
exactly the strings we are interested in and so we can use
finite automata to represent temporal models.
Thus, now, the “infinite tail” has to always accept an ‘a’.
The automata needed are a specific form of automata over
¨
infinite strings, often termed ‘ω-automata’, or Buchi
automata. (We will discuss them in detail later.)
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 14 / 20
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 16 / 20
What are Fixpoints?
What is TL?
Axioms
Characterising TL
Normal Form
In general, fixpoints are solutions to recursive equations,
such as x = f (x ); in basic algebra, we know that a = 0 is a
solution of a = (a ∗ 5).
Temporal Fixpoint Examples
What is TL?
Axioms
Characterising TL
Normal Form
¨
Buchi
Automata
¨
Buchi
Automata
Fixpoints
Fixpoints
Quantification
There can often be several solutions to fixpoint equations;
a = 0 and a = 1 are both solutions of a = (a ∗ a).
Quantification
As we often wish to distinguish solutions, we select using
ϕ
♦ϕ
≡
≡
νξ. (ϕ ∧ ❤ξ)
µξ. (ϕ ∨ ❤ξ)
ϕ is defined as the maximal fixpoint (ξ) of the
Here,
formula ξ ⇔ (ϕ ∧ ❤ξ). Thus, the maximal fixpoint above
effectively defines
ϕ as the ‘infinite’ formula
ϕ ∧ ❤ϕ ∧ ❤ ❤ϕ ∧ ❤ ❤ ❤ϕ ∧ . . .
ν, representing the maximal (greatest) fixpoint, or
µ, representing the minimal (least) fixpoint.
Note that the minimal fixpoint of ξ ⇔ (ϕ ∧ ❤ξ) is ‘false’,
since putting false in place of ‘ξ’ is legitimate and false is
the minimal solution.
For example, we write down ν a. (a ∗ a) to denote the maximal
fixpoint of a = (a ∗ a); similarly with ‘µ’.
N.B: minimality/maximality are defined in relation to ‘⇒’; so
‘false is the minimal element while ‘true’ is the maximal.
It is important to note that, in some cases no fixpoint exists.
Note: when only one exists, maximal and minimal versions
coincide.
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 17 / 20
c
Michael
Fisher
What are Temporal Fixpoints?
What is TL?
Axioms
Characterising TL
Axioms
Fixpoints
Quantification
Normal Form
A fixpoint solution to the formula ‘ψ ⇔ (ϕ ∧ ❤ψ)’ is some
formula ‘ψ’ that makes the statement true.
Taking ψ ≡
LOGIC : ESOTERICA ]
– 19 / 20
PTL can be extended with quantification.
Characterising TL
Normal Form
¨
Buchi
Automata
[ TEMPORAL
A Little Quantification
What is TL?
The µ (least fixpoint) and ν (greatest fixpoint) operators
have been transferred to temporal logics.
An Introduction to Practical Formal Methods Using Temporal Logic
¨
Buchi
Automata
Fixpoints
Quantification
Full first-order quantification is complex, so might allow
quantification, but only over Boolean valued variables
(specifically, propositions of the language).
ϕ does make this formula true, since
ϕ ⇔ (ϕ ∧ ❤
Thus, using such a logic, called Quantified Propositional
Temporal Logic (QPTL), it is possible to write formulae such
as
∃p. p ∧ ❤ ❤p ∧ ♦ ¬p
ϕ)
is valid, while ψ ≡ ❤ϕ does not, since
❤ϕ 6⇔ (ϕ ∧ ❤ ❤ϕ) .
where p is a propositional variable.
The fixpoint operators, together with ‘next’, form the basis of
a powerful temporal logic called νTL.
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 18 / 20
c
Michael
Fisher
An Introduction to Practical Formal Methods Using Temporal Logic
[ TEMPORAL
LOGIC : ESOTERICA ]
– 20 / 20
`