[go: up one dir, main page]
Scribd
Upload
53 views11 pages

EE709 Temporal Logic

The document discusses temporal logic, which is a formal way to express properties over time. It describes linear temporal logic and computation tree logic, defines Kripke structures and paths, and covers state formulas, path formulas, and computation tree logic formulas. Examples of using temporal logic to represent arbitration are also provided.

Uploaded by

Yogesh Katara
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
53 views11 pages

EE709 Temporal Logic

The document discusses temporal logic, which is a formal way to express properties over time. It describes linear temporal logic and computation tree logic, defines Kripke structures and paths, and covers state formulas, path formulas, and computation tree logic formulas. Examples of using temporal logic to represent arbitration are also provided.

Uploaded by

Yogesh Katara
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 11

Temporal logic: a formal way to express

properties

Madhav Desai
Department of Electrical Engineering
IIT Bombay

March 12, 2024


Overview

I Linear temporal logic.


I Computation tree logic.
Kripke structure

I Finite set of states S.


I Transition relation T ⊆ S × S.
I Complete: that is, for every s ∈ S, there is a t ∈ S such that
(s, t) ∈ T.
I L : S → {0, 1} is defined as follows: For s ∈ S, L(s) consists
of propositions which hold in s, for example the state
variables.
Example: viewing a Mealy machine as a Kripke structure

I S = {(x, q, y ) : x, q, y }.
I T = {((x, q, y ), (x 0 , q 0 , y 0 )) : q 0 = δ(x, q).
I L(s) = {x(s), q(s), y (s), (y (s) == λ(x(s), q(s)))}.
State formulas

f : S → {0, 1}
If f holds at state s then we denote this by

sf

I s  f if and only if f ⊆ L.
I s  ¬f if and only if s 
f .
I s  (f + g ) if and only (s  f ) + (s  g ).
I s  (f .g ) if and only (s  f ).(s  g ).
Paths

π = s(0), s(1), s(2), . . . , where s(i) ∈ S.


Path formulas

I If f is a state formula, then f is also a path formula and


f (π) = f (s(0)).
I s  E (g ) means that there is a path π starting from s such
that g holds on that path.
I Linear time formulas:
I Next f holds on the path: Xf (π) = f (s(1).
I Finally, f holds on the path π: Ff (π) = f (s(k))forsomek ≥ 0.
I Globally, f holds on the path π: Gf (π) = f (s(k))forallk ≥ 0.
I f holds until g on the path π: fUg(π) = 1 if and only if there
exists k ≥ 0 such that g (s(k) = 1, and f (s(i)) = 1 for i < k.
I Tree formulas:
I Always (on every path) the path formula f holds: Af
I There exists a path on which the path formula f holds: Ef .
Computation Tree Logic formulas

I AXp, EXp
I AGp, EGp
I AFp, EFp
I A(f U g), E(f U g)
Equivalences

A f = ~ E (~f)
E f = ~ A (~f)
EF f = E(1 U f)
AX f = ~EX (~f)
AG f = ~EF (~f)
EF f = ~AG (~f)
.. etc...
Example: arbitration

T1, T2 requests
C1, C2 critical region access

~EF (C1.C2)
AG (T1 => F C1)
AG (T2 => F C2)
Encoding of a run

Runk = R(s(0), s(1)).R(s(1).s(2))....R(s(k − 1), s(k))


Constraintk = C 0(s(0))C 1(s(1))C 2(s(2))...Ck(s(k))

Check if Runk .Constraintk is satisfiable

You might also like