The linear time temporal logic LTL

(1)

The linear time temporal logic LTL

Valentin Goranko DTU Informatics

October 2010

Valentin Goranko DTU Informatics () The linear time temporal logic LTL October 2010 1 / 26

(2)

The linear time temporal logic LTL: introduction

• Using temporal logics for specification and verification of concurrent and reactive systems was first suggested by Pnueli in his landmark 1977 paper ”The Temporal Logic of Programs”.

For this and related work, he received the Turing Award in 1996.

• The linear time temporal logic LTL was first introduced and studied by Gabbay, Pnueli, Shelah and Stavi in 1980.

• Extends propositional logic with temporal operators for discrete linear time.

• Used to reason about properties of single computations.

(3)

Temporal operators in LTL: Nexttime

Whereas ϕstates a property of the current state, Xϕstates that the next state satisfies ϕ.

Xϕ: nexttime ϕ

Xϕ ϕ · · ·

Thus, ϕ∨Xϕ states thatϕis satisfied now or at the next state.

For instance,alert→Xhalt means that if the system currently is in a state of alert, then next state will be a halting state.

(4)

Temporal operators in LTL: Sometime

Fϕclaims that some future (or possibly, the current) state satisfiesϕ without specifying which one, i.e., that “ϕwill be true sometime in the future”.

Fϕ: sometimeϕ

Fϕ ϕ · · ·

Thus, alert→F halt means that if the system currently is in a state of alert, then it will sometime later be in a halt state.

(5)

Temporal operators in LTL: Always

Gϕclaims that all the future states (including the current one) satisfy ϕ, i.e., that “ϕ will always be true”.

Gϕ: alwaysϕ

Gϕ, ϕ ϕ ϕ ϕ ϕ · · ·

Thus, G(alert→F halt) means that whenever in the future the system is in a state of alert, it will sometime later be in a halt state.

G is thedual of F: Gϕand ¬F¬ϕare equivalent.

(6)

Temporal operators in LTL: Until

The binary operator U is more expressive than the operator F.

The formula ϕUψstates that ϕis true untilψ is true.

More precisely: ψwill be true at some future state, and ϕwill hold in the meantime.

ϕUψ : ϕuntilψ

ϕUψ,ϕ ϕ ϕ ϕ ψ · · ·

The exampleG(alert→F halt) can be refined with the statement that

“starting from a state of alert, the alarm remains activated until the halt state is eventually reached”:

G(alert→(alarmU halt)).

Note that the operator F is a special case of U: Fϕ≡trueUϕ.

(7)

Temporal operators in LTL: Other operators

Weak until: Intuitively, the statement ϕWψ still expresses “ϕ untilψ”, but without the inevitable occurrence of ψ; ifψ never occurs, thenϕmust remain true forever. Thus:

ϕWψ≡Gϕ∨(ϕUψ).

Before: Defined as dual of U on the first argument:

ϕBψ:=¬(¬ϕUψ).

Meaning: before every occurrence of ψthere is an occurrence of ϕ.

Release: Defined as the full dual of U:

ϕRψ:=¬(¬ϕU¬ψ).

Meaning: ϕRψ the truth ofϕreleases the requirement for the truth ofψ.

More precisely, it means that, unless ψ is true in all future states, ϕmust be true sometime in the future and ψ must hold between the current state and that future state.

(8)

Formulae and syntax of LTL

LTL formulae:

ϕ::=

propositional logic

z }| {

⊥ | p | ¬ϕ | ϕ∧ψ |

temporal extension

z }| {

Xϕ | Fϕ | Gϕ | ϕUψ where pranges over a countable set ofatomic propositions AP={p₀,p₁, ...}, obtained by abstracting properties.

Since a formula only contains finitely many atomic propositions, whenever suitable we can assume that APis finite.

F and G can be regarded as definable in terms of U.

Some abbreviations:

ϕ→ψ:=¬ϕ∨ψ,

F^∞ϕ:= GFϕ (”ϕholds infinitely often”).

G^∞ϕ:= FGϕ(”ϕholds eventually”).

ϕBψ:=¬(¬ϕUψ); ϕRψ:=¬(¬ϕU¬ψ).

(9)

Expressing properties of computations with LTL

(safety) init→G safe, (liveness) G(p→Fq),

(total correctness) (init∧p)→F(end∧q), (strong fairness) F^∞enabled→F^∞executed.

(10)

Expressing properties with LTL: exercises

“Every time when a message is sent, it will not be marked as ’sent’ before an acknowledgment of receipt is returned.”

G(Sent→(¬MarkedSent U AckReturned)).

“Every occurrence of p will be followed immediately by an occurrence of q which will hold true until p ceases to be true.”

G(p →X(q∧qU¬p)).

“Between every two green signals there will be a red signal”

G(Green→X(¬GreenW Red))?

or:

G(Green∧FGreen→X(¬GreenU Red))?

or

G(Green→X(GreenB Red))?

Precise formal semantics of LTL is needed!

(11)

Linear models for LTL

The standard models for LTL are single computations in ITS, hereafter just called (linear) LTL-models.

Formally, an LTL-model is an infinite sequence σ:N→ P(PROP).

For example, here are the five first states of an LTL-model:

{p} {q} { } {p,q,r} {q} · · ·

Every linear LTL-model can also be viewed as an infinite (ω-) wordin the alphabetP(PROP).

For instance, the model above corresponds to the infinite word {p}{q}{}{p,q,r}{q}. . .

(12)

Semantics of LTL

Given an LTL-modelσ, a position i ∈N, and a formula ϕ, we define inductively the satisfaction relation|= as follows:

• σ,i 6|=⊥,

• σ,i |=piff p∈σ(i), for every p∈PROP,

• σ,i |=¬ϕ iff σ,i 6|=ϕ,

• σ,i |=ϕ∧ψ iff σ,i |=ϕ andσ,i |=ψ,

• σ,i |= Xϕ iff σ,i+ 1|=ϕ,

• σ,i |= Fϕiff there is j ≥i such that σ,j |=ϕ,

• σ,i |= Gϕ iff for allj ≥i, we haveσ,j |=ϕ,

• σ,i |=ϕUψ iff there is j ≥i such that σ,j |=ψand σ,k |=ϕfor all i ≤k <j.

We writeσ |=ϕinstead ofσ,0|=ϕ and say thatσ is a model of the formulaϕ.

(13)

Semantics of LTL: exercises

p r p,q q p,q,r p · · ·

The valuation defining the model σ: V(p) ={s_2k |k ∈N}, V(q) ={s_k |2≤k ≤4 or 100≤k}, V(r) ={s_3k₊₁|k ∈N}.

Determine:

σ,0

?

|=q∨XX¬r Y;σ,1

?

|= F(q∧XX¬p) Y;σ,2

?

|= G(p →X¬p) Y σ

?

|=¬qU (p∧r) N; σ

?

|=¬qU (qUr) Y σ

?

|= G^∞¬(p∧q) N; σ

?

|= F^∞¬(p∧q) Y σ

?

|= FGF(p∧q∧r) Y; σ

?

|= F^∞((p∧ ¬r)Ur) Y σ

?

|= G^∞(¬p∨F¬q∨X¬r)N; σ

?

|= GF(r U X(¬p∧Xr)). Y

(14)

Models of an LTL-formula as infinite words

PROP(ϕ) denotes the set of propositional variables occurring in ϕ.

The set Mod(ϕ) of all models for a formula ϕcan be viewed as a formal language over the alphabet P(PROP(ϕ)):

Mod(ϕ) ={σ ∈(P(PROP(ϕ)))^ω |σ |=ϕ}.

Formal languages over infinite words generated in this way by LTL formulae can be recognized byB¨uchi automataon infinite words.

This fact is at the heart of the automata based methodfor verification of LTL formulae.

(15)

Satisfiability and validity of LTL-formulae

An LTL-formula ϕissatisfiableif Mod(ϕ) is non-empty.

ϕ isvalidif ¬ϕis not satisfiable, i.e.,Mod(¬ϕ) is empty.

The satisfiability problemfor LTL, denoted bySAT(LTL):

Input: anLTL formulaϕ,

Question: Is there someLTL-modelσ such that σ|=ϕ?

Equivalently, is it the case thatMod(ϕ)6=∅?

The validity problem VAL(LTL):

Input: anLTL formulaϕ,

Question: Is the case thatσ|=ϕfor all LTL-models σ?

Equivalently, is it the case thatMod(¬ϕ) =∅?

(16)

Some important validities of LTL formulae

• G^∞ϕ→F^∞ϕ

• Gϕ∧Fψ→ϕUψ

• ϕ∧G(ϕ→Xϕ)→Gϕ

• ϕ∧G(ϕ→XFϕ)→GFϕ

• Fϕ↔ϕ∨XFϕ

• Gϕ↔ϕ∧XGϕ

• (ϕ→χ)Uψ∧ϕUψ→χUψ

• ϕUψ↔(ψ∨(ϕ∧X(ϕUψ)))

• ψU(ϕ∨χ)↔(ψUϕ∨ψUχ)

• G((ψ∨(ϕ∧Xθ))→θ)→(ϕUψ→θ)

(17)

Truth of LTL-formulae in interpreted transition systems

Every rooted ITS generates a set of linear LTL-models, viz. all computations starting from the root.

Traces(M,s) denotes the set of all computations in (M,s).

So, LTLformulae can be evaluated in (rooted) ITS (M,s):

(M,s)|=ϕiff σ |=ϕfor all computationsσ starting ats.

So, we define universal truth ofϕat (M,s), denoted M,s |=∀ϕ.

Likewise, we define existentialtruth of ϕat (M,s), denoted M,s |=∃ ϕ.

An ITSM= (S,R,L) is finiteif each of S, the image of L, and each set in that image are finite sets.

A finite ITS can generate an uncountable set of computations.

(18)

Preservation of truth of LTL-formulae in unfoldings

Recall that paths and computations in an ITS Mand in its unfoldingMc are in one-to-one correspondence: the last state of a path in Mc is actually the corresponding path in M.

Therefore, for every LTL-formula ϕ, interpreted transition systemMand a state s in it:

M,s |=∃ ϕ iff M,c bs |=∃ ϕ and likewise,

M,s |=∀ ϕ iff M,c bs |=∀ϕ.

(19)

Local model checking of LTL-formulae: example 1

ON OFF

• M,OFF

?

|=_∀F^∞ON No; M,OFF

?

|=_∀F^∞OFF No;

• M,ON

?

|=_∃ ¬F^∞OFF Yes;

• M,OFF

?

|=_∀F^∞ON∨F^∞OFF Yes; M,ON

?

|=_∃ F^∞ON∧F^∞OFF Yes;

• M,ON

?

|=_∃ G(ON→XXOFF) Yes;

• M,ON

?

|=_∃ G(ON→XOFF)∧F^∞ON Yes;

• M,ON

?

|=_∃ G(ON→XXOFF)∧G(OFF→XXXON) No;

• M,ON

?

|=_∃ (ON∧F OFF) U G ON Yes.

(20)

Local model checking of LTL-formulae: example 2

M

s1

{q}

s2

{p,q}

s4

{q}

s3

{p}

s5

{}

s6

{p,q}

Check the following:

M,s1

?

|=∃Gp. N M,s₁

?

|=_∃XGp. Y M,s₁

?

|=∃G(q→Xp) Y M,s1

?

|=∀G(q→Xp) N M,s1

?

|=∀F^∞(p∨q) Y M,s₁

?

|=∀ G^∞(¬p →Xq) N M,s3

?

|=∃¬q U X(q U Gp) Y M

?

|=∀F^∞(p∨q) Y M,s1

?

|=∃X(pU Gq) Y M

?

|=∃ G^∞(p∨q) Y

(21)

Ultimately periodic linear models for LTL

Ultimately periodic sequence, intuitively: like a lasso, consisting of a finite

‘tail’, followed by a finite ‘loop’.

A computation (or, linear LTL-model) σ:N→ P(PROP) isultimately periodic (UP) if there exist natural numbersi andp >0 such that σ(k) =σ(k+p) for everyk ≥i.

The (possibly empty) sequence σ(0), . . . , σ(i−1) is theprefix and σ(i), . . . , σ(i+p−1) is the loopof the model.

We say thatσ hasprefix index i and periodp.

Thus, an UP-modelσ can be equivalently represented by the finite sequence Γ₀, . . . ,Γ_i+p such that each Γ_j =σ(j).

Traces^UL(M,s) is the set of UP-computations in Traces(M,s).

(22)

LTL model-checking as an algorithmic problem

In order to define the algorithmic problemof model-checking, models must be finitely presentable objects.

We say thatM= (S,R,L) is finitewhenever S, the image of L, and each set in that image are finite sets.

We only consider the algorithmic model-checking problem for LTL in finite ITS.

For instance, UP-models over finite sets of variables are finite.

(23)

Path model-checking of LTL formulae

Model-checking forLTL in finite ITS is usually intractable.

If we restrict attention to finite UP-models, we have thepath model-checking problem for LTL:

input: A finite UP-modelσ and anLTLformulaϕ.

question: Doesσ |=ϕ?

Proposition

The path model-checking problem forLTL is decidable in PTime. Proof sketch: The path model-checking device can compute the truth of all subformulae of the given formula at each state of the UP-model simultaneously, by applying certain labelling algorithm.

For that, the device only has to perform a number of steps polynomial in the size of the input formula and of the model.

Open question: Is the path model-checking problem for LTL PTime-hard?

(24)

The full model-checking problems for LTL

Given an ITS M= (S,R,L), denote byPROP(M) the set of atomic propositions occurring in the image of L.

WhenM is finite, its size|M|is defined as the sum card(S) +card(R) +X

s∈S

card(L(s)).

The (universal) local model-checking problem forLTL:

input: anLTL formulaϕ, a finite ITS Mand a states ∈S, question: Is it the case thatM,s |=∀ϕ?.

In the above we can assume that the codomain of Lis restricted to PROP(ϕ).

Existential local model-checking, denoted by MC^∃(LTL), is defined likewise.

(25)

Ultimately periodic model property for LTL-formulae

Theorem (Sistla& Clarke’85)

For every satisfiable LTLformulaϕ, there is an ultimately periodic model σ such thatσ|=ϕ, its period is bounded by|ϕ| ×2^4|ϕ|and its prefix index is bounded by 2^4|ϕ|.

Proof: see lecture notes.

(26)

Complexity of LTL

Theorem (Sistla& Clarke’85) LTL satisfiability is inPSpace.

Proof sketch: Guessing a sequence of length at most 2^4|ϕ|+|ϕ| ×2^4|ϕ|

and checking on-the-fly that it is a small satisfiability witness can be done in nondeterministic polynomial space.

By Savitch’s Theorem this gives a polynomial space upper bound.

Theorem (Sistla& Clarke’85)

The existential and universal model-checking problems for LTL are in PSpace.

Proof sketch:

By a similar argument. The small satisfiability witness can be decorated with states and transitions from the model.

The only essential difference is that the maximal values for the prefix index and the period have an additional factor, viz., the number of states of the transition system.