Logical Characterization• Linear Temporal Logic

Speciﬁcation for the computation path
Property description for a sequence of transitions

୪⾜ศᩓィ⟬≉ㄽ (14)• Branching Temporal Logic

Speciﬁcation for the computation tree
Property description for all possible tree of transitions

Shoji Yuen

LTL states the properties about a path:
A state that satisﬁes p is always followed by a states that satisﬁes q

2012/01/17

BTL sates the properties about branches:
All transitions from a state that satisﬁes p lead to the states thatsatisfy q

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

1/14

Propositional Temporal LogicFH23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

2/14

PTL speciﬁcation♦φ ≡ true U φφ ≡ ¬(true U ¬φ)(p → ♦q) : state p is always followed by state q.

::= p | ¬F | F ∧ F |  F | F U F

Temporal operators

Satisﬁability of PTL-formulas is checked in PSPACE-complete.

φ : φ holds after the next transition.

Model: Kripke structure M = S, S0 , μ, E

φ1 U φ2 : φ1 holds until φ2 holds.
σ |= p iﬀ

p ∈ σ0σ |= ¬φ iﬀ

σ |= φσ |= φ1 ∧ φ2 iﬀ
σ |= φ iﬀσ |= φ1 U φ2 iﬀ

S: States

S0 ⊆ S: Initial states

E ⊆S ×S: Transitions

μ : S → 2APσ |= φ1 and σ |= φ2σ 1 |= φFor some j ≥ 0.σ j |= φ2

Check: Check if path(s) of M satisfy property φ.
Usually the paths beginning from an initial state.

and σ k |= φ1 for all 0 ≤ k < j
H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

3/14

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

4/14

Timed PTL

MITL(metric interval temporal logic)[Alur90]

With speciﬁcation when a transition may occurs0MITL formulas1Fρ:(S0 , I0 ) → (S1 , I1 ) → (S2 , I2 ) →Ii : interval Ii is adjacent to Ii +1
s2::= p | ¬F | F ∧ F | F UI FMITL semantics ρ = (σ, I ):timed state sequence.

s3

ρ |= p iﬀ p ∈ σ 0Interval:[a, b],[a, b),[a, ∞),(a, b],(a, b),(a, ∞)[,] for closed intervals, (,) for open intervals

ρ |= ¬φ iﬀ p |= φ
ρ |= φ1 ∧ φ2 iﬀ ρ |= φ1 and ρ |= φ2
ρ |= φ1 UI φ2 iﬀ for some t ∈ I .σ t |= φ2notation: ρt : State sequence after time t.

σ t |= for all t  ∈ (0, t)t ∈ Ii , ρt = (σi , Ii − t) → (σi +1,Ii +1−t ) → · · ·H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

5/14

H23 ୪⾜ศᩓィ⟬≉ㄽ

Derived operators

2012/01/17

6/14

Rational time satisﬁability♦I φ ≡ true UI φ
I φ ≡ ¬♦I ¬φ
φ1 I U φ2 ≡ ¬((¬φ2 ) UI (¬φ1 )) φ1 unless φ2Deﬁnition(σ, I ) is rational if the end-points of all intervals in I are rational.

What do these formulas mean?

ρ Q-satiﬁes φ iﬀ ρ |=Q φ where all time variables range over only Qp ∧ ≥0 (p → (¬) U(0,∞) p).

A MITL formula φ is Q-satisﬁable iﬀ it is satisﬁable.

(0,∞) (p → ♦[0,3) q).

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

7/14

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

8/14

Undecidability[Alur90]

Satisﬁability

Theorem

Proposition

The satisﬁability of MITL (with no singlular interval) isEXPSPACE-complete.

If singular intervals are allowed as subscripts for temporal operators
in MITL, then the satisﬁability problem is undecidable.
Singular interval:[a, a]

Alur’s algorithm:O(2N·K ·log (N·K ) )If no singular interval is allowed,

K:N:

(p → ♦=5 q) is not in MITL
(p → (¬q) U=5 q) is in MITL

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

9/14

Model checking TA with MITL

largest integer constant in φ+1
number of propositions, boolean connectives
and temporal operators in φ.

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

10/14

More on Timed Automata
Timed Safety Automata[Henzinger94]
Timed automata with state invariants.
State invariants:time constraints on states
All states are Büchi accepting.
Eﬀective in checking safety properties. All safety properties can bechecked in the ﬁnite preﬁx.

For a timed automaton A, check if LT (A) ⊆ L(φ)
Construct a TA that accepts L(A) ∩ L(B¬φ ) and check itsemptiness.
Construction of A × B¬φ is exponential for |φ|. Checking
emptiness is PSPACE-complete.

Zone construction[BengtssonYi04]
More eﬃcient than regions Symbolic timed model checking.
Regions ⇒ Zones (diﬀerence constrains)
Bounded Diﬀerence Matrix(BDM):Eﬃcient data structure

A minor extension for timed automata to deal with intervals.

Uppaal incorporates these eﬀective verﬁcation
method.[BengtssonYi04]
H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

11/14

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

12/14

Other timed model

SummaryTimed I/O automata [Kaynar, Lynch, Segara, Vaandrager05]• Concurrent computation model

Process calculi with time

A set of automata with synchronization• Realtime ACP [Baeten91]• Process calculus(CCS)• Timed CCS [Yi90]

Algebraic characterization based on bisimulations• Timed CSP [Schneider00]• Timed extension• ATP [Nicolin, Sifaxis90]

Time as a synchronization measure
A thoery of timed automaton and its extension• TPL [Regan, Hennessy95]

SOS characterization with time

Await for time-aware application.

OSOS with time tick [UlidowskiYuen04]

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

13/14

H23 ୪⾜ศᩓィ⟬≉ㄽ

2012/01/17

14/14