Model Checking Ch.4

Overview

1. Modeling (Ch.3)

graph TB START --> s0 s0 --> s1 s0 --> s2 s1 --> s0 s1 --> s2 s2 --> s2 style START fill:#FFFFFF, stroke:#FFFFFF START(( )) s0((a,b)) s1((b,c)) s2((c))

Kripke structure

2. Specification (Ch.4)

\( \bm{EF}c, \bm{AG}b \)

Temporal Logic

3. Verification

CTL Model Checking (Ch.5)
LTL and CTL* Model Checking (Ch.6)
etc...

Goal: Understanding specification
- Specify properties of the model
Means: Temporal Logic
- Describe properties along time (dynamically)
Flow of this chapter:
- Introduction to Temporal Logic
- Types of Temporal Logic
  - CTL*
  - CTL
  - ACTL*
  - ACTL
  - LTL
- Important Topics
  - Temporal Logic with Set
  - Fairness
  - Counterexamples
  - Safety and Liveness Properties

Introduction to Temporal Logic
4.1 The Computation Tree Logic CTL*
4.2 Syntax and Semantics of CTL*
4.3 Temporal Logics Based on CTL*
4.4 Temporal Logic with Set Atomic Propositions and Set Semantics
4.5 Fairness
4.6 Counterexamples
4.7 Safety and Liveness Properties

Introduction to Temporal Logic

NOTE: This descriptions are informal.

Propositional Logic

Describe the relationship between atomic propositions.

Syntax

\[ \phi := p \mid \lnot \phi \mid \phi \lor \psi \mid \phi \land \psi \, \mid \phi \rightarrow \psi \]

\( \phi, \psi \): Syntax of propositional logic
\( p \in AP \): Atomic proposition

Example

"If I didn't have lunch, I am hungry" is expressed as

\( \lnot \) "I had lunch" \( \Rightarrow \) "I am hungry"

Temporal Logic

Describe atomic propositions along time.

Syntax

\[ \phi := p \mid \lnot \phi \mid \phi \lor \psi \mid \phi \land \psi \mid F \phi \mid G \phi \mid X \phi \mid ... \]

\( \phi \) : Syntax of temporal logic
\( p \in AP \) : Atomic proposition

Example

"I will eventually be hungry in the future" is expressed as

\( F \) "I am hungry"

Propositional Logic vs. Temporal Logic

Propositional Logic: a single point in time (like a picture)

graph LR s(("hungry"))

Temporal Logic: continuous time (like a movie)

graph LR s0(( )) --> s1(( )) --> s2(( )) --> s3((hungry)) --> s4((hungry)) --> dots style dots fill:#FFFFFF, stroke:#FFFFFF dots((...))

4.1 The Computation Tree Logic CTL*

CTL*: Temporal Logic describing properties of computation tree

Computation Tree

Computation Tree \( \Leftrightarrow \) Kripke structure
- Computation Tree is formed by unwinding the Kripke structure from initial state.
All branches are infinite
- \( \because \) Transition relations in Kripke structure is left-total (each state has a successor).

Kripke structure \( M \)

graph TB START --> s0 s0 --> s1 s0 --> s2 s1 --> s0 s1 --> s2 s2 --> s2 style START fill:#FFFFFF, stroke:#FFFFFF START(( )) s0((a,b)) s1((b,c)) s2((c))

\( \Longleftrightarrow \)

Computation Tree of \( M \)

graph TB START --> s0 s0 --> s1 s0 --> s2 s1 --> s3 --> dots0 s3 --> dots1 s1 --> s4 --> dots2 s2 --> s5 --> dots3 style START fill:#FFFFFF, stroke:#FFFFFF style dots0 fill:#FFFFFF, stroke:#FFFFFF style dots1 fill:#FFFFFF, stroke:#FFFFFF style dots2 fill:#FFFFFF, stroke:#FFFFFF style dots3 fill:#FFFFFF, stroke:#FFFFFF START(( )) dots0((...)) dots1((...)) dots2((...)) dots3((...)) s0((a,b)) s1((b,c)) s2((c)) s3((a,b)) s4((c)) s5((c))

CTL*

CTL*: Temporal Logic describing properties of computation tree (\( \Leftrightarrow \) Kripke structure)

CTL* Formulas

CTL* formulas are composed of path quantifiers and temporal operators:

Path quantifiers: \( \bm{A}, \bm{E} \)
- \( \bm{A} \varphi \) : "all computation paths"
  - All paths from a given state have property \( \varphi \)
- \( \bm{E} \varphi \) : "there exists a computation path"
  - At least one path from a given state has property \( \varphi \)

\( \bm{A} \varphi \)

graph TB s0(( )) --> s1(( )) s0 --> s2(( )) s1 --> s3(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6(( )) classDef node fill:#bbb

\( \bm{E} \varphi \)

graph TB s0(( )) --> s1(( )) s0 --> s2(( )) s1 --> s3(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6(( )) style s0 fill:#bbb style s2 fill:#bbb style s5 fill:#bbb

Temporal operators: \( \bm{X}, \bm{F}, \bm{G}, \bm{U}, \bm{R} \)
- \( \bm{X} p \) : "next time \( p \)"
  - Proposition \( p \) holds on the second state of the path
- \( \bm{F} p \) : "eventually \( p \)" or "in the future \( p \)"
  - Proposition \( p \) holds at some state on the path
- \( \bm{G} p \) : "always \( p \)" or "globally \( p \)"
  - Proposition \( p \) holds at every state on the path
- \( p \bm{U} q \) : "\( p \) until \( q \)"
  - It holds if:
    - there is a state on the path where the second property \( q \) holds and
    - at every preceding state on the path, the first property \( p \) holds.
- \( p \bm{R} q \) : "\( p \) release \( q \)"
  - It holds if \( q \) holds along the path up to and including the first state where \( p \) holds.
    - \( p \) is not required to eventually hold.
  - Logical dual of the \( \bm{U} \)

Example

\( \pi_0 \models \bm{G} b \)
- On \( \pi_0 \), property \( b \) holds in every state.
\( \pi_1 \not\models \bm{G} b \)
- On \( \pi_1 \), property \( b \) does not hold in every state.
\( s_0 \models \bm{EG} b \)
- One path (but not all paths) from the initial state \( s_0 \) satisfy \( \bm{G} b \)
\( s_0 \not\models \bm{AG} b \)
- All paths from the initial state \( s_0 \) do not satisfy \( \bm{G} b \)

graph TB START --> s0 s0 --> s1 s0 --> s2 s1 --> s3 --> dots0 s3 --> dots1 s1 --> s4 --> dots2 s2 --> s5 --> dots3 style START fill:#FFFFFF, stroke:#FFFFFF style dots0 fill:#FFFFFF, stroke:#FFFFFF style dots1 fill:#FFFFFF, stroke:#FFFFFF style dots2 fill:#FFFFFF, stroke:#FFFFFF style dots3 fill:#FFFFFF, stroke:#FFFFFF START(( )) dots0((π0)) dots1((...)) dots2((...)) dots3((π1)) s0(("s0
{a,b}")) s1(("s1
{b,c}")) s2(("s2
{c}")) s3(("s3
{a,b}")) s4(("s4
{c}")) s5(("s5
{c}"))

This example shows that:

Path quantifiers describe properties of a state.
- "Does a certain path start in this state?"
Temporal operators describe properties of a path.
- "Can a certain state be reached along this path?"

Path quantifier: \( \bm{A} \varphi \)

graph TB s0(( )) --> s1(( )) s0 --> s2(( )) s1 --> s3(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6(( )) classDef node fill:#bbb

Temporal operator: \( \bm{F} p \)

graph LR x0 --> x1 --> x2 --> x3 --> x4 x0(( )) x1((p)) x2(( )) x3(( )) x4(( ))

4.2 Syntax and Semantics of CTL*

In this section, we formally define the syntax and semantics of CTL*.

4.2.1 Syntax of CTL*

Two types of formulas:

State formulas specify the properties of a specific state
Path formulas specify the properties of a specific path

State formulas:

If \( p \in AP \), then \( p \) is a state formula. (\( AP \) is the set of atomic propositions)

If \( f \) and \( g \) are state formulas, then \( \lnot f, f \lor g \) and \( f \land g \) are state formulas.

If \( f \) is a path formula, then \( \bm{E} f \) and \( \bm{A} f \) are state formulas.

Path formulas:

If \( f \) is a state formula, then \( f \) is also a path formula.

If \( f \) and \( g \) are path formulas, then \( \lnot f, f \lor g, f \land g, \bm{X} f, \bm{F} f, \bm{G} f, f \bm{U} g \) and \( f \bm{R} g \) are path formulas.

Example of A.4

\( s_0 \models p \)

graph LR s0((p))

\( \pi_0 \models p \)

graph LR s0((p)) --> s1(( )) --> s2(( )) --> s3(( )) --> s4(( ))

\( \pi_0 \models \bm{X} p \)

graph LR x0 --> x1 --> x2 --> x3 --> x4 x0(( )) x1((p)) x2(( )) x3(( )) x4(( ))

CTL* is the set of state formulas permitted by the above rules:

Boolean propositions (labels)
- ex) \( p \)
Path formulas with path quantifier
- ex) \( \bm{AX} p , \bm{EAG} q\)
Boolean combinations
- ex) \( p \land \bm{AX} q \)

Examples of formulas

A.1

\( s_0 \models a \)

A.2

\( s_0 \models a \land b \)

A.4

\( \pi_0 \models a \)

because \( \pi_0 \) have the initial state \( s_0 \)

A.5

\( \pi_0 \models \bm{G} b \)

Temporal operators specify paths \( \pi \)

A.3

\( s_0 \models \bm{EG} b \)

Path quantifiers specify states \( s \)

Q. Is \( \pi_0 \models \bm{EG} b \) correct?

Correct because of:

A.3 ( \( \bm{EG} b \) is state formula )
A.4 ( state formula is path formula )

graph TB START --> s0 s0 --> s1 s0 --> s2 s1 --> s3 --> dots0 s3 --> dots1 s1 --> s4 --> dots2 s2 --> s5 --> dots3 style START fill:#FFFFFF, stroke:#FFFFFF style dots0 fill:#FFFFFF, stroke:#FFFFFF style dots1 fill:#FFFFFF, stroke:#FFFFFF style dots2 fill:#FFFFFF, stroke:#FFFFFF style dots3 fill:#FFFFFF, stroke:#FFFFFF START(( )) dots0((π0)) dots1((...)) dots2((...)) dots3((π1)) s0(("s0
{a,b}")) s1(("s1
{b,c}")) s2(("s2
{c}")) s3(("s3
{a,b}")) s4(("s4
{c}")) s5(("s5
{c}"))

\[ \pi_0 = \{ s_0, s_1, s_3, ... \} \text{ (leftmost path)} \]

4.2.2 Semantics of CTL*

Preparation for semantic definitions

Review: Kripke structure \( M \)

\( M = (S, S_0, R, AP, L) \)

\( S \)

the set of states

\( S_0 \subseteq S \)

the set of initial states

\( R \in S \times S \)

the transition relation, left total

\( \bm{AP} \)

the set of atomic propositions

\( \bm{L} : S \rightarrow 2^{AP} \)

a function that labels each state with a set of atomic propositions

Path \( \pi \) in \( M \)

\( \pi = s_0, s_1, ... \)

\( s_k \in S \), and \( (s_i, s_{i+1}) \in R \)

\( \pi^i = s_i, s_{i+1}, ... \)

the suffix of \( \pi \) starting at \( s_i \)

The modeling relation \( \models \) and Equivalence \( \equiv \)

\( M, s \models f \)

\( f \) holds at state \( s \) in a kripke structure \( M \)

\( M, \pi \models f \)

\( f \) holds at path \( \pi \) in a kripke structure \( M \)

\( f \equiv g \)

\( M, s \models f \) if and only if \( M, s \models g \) for all \( M, s \)

\( M, \pi \models f \) if and only if \( M, \pi \models g \) for all \( M, \pi \)

Definition: Semantics of CTL*

Assumptions:

\( f_1, f_2 \): State formulas
\( g_1, g_2 \): Path formulas
\( p \in AP \): Atomic propositions

Semantics of CTL*:

\( M, s \models p \)

\( \Leftrightarrow \)

\( p \in L(s), \) for \( p \in AP \)

\( M, s \models \lnot f_1 \)

\( \Leftrightarrow \)

\( M, s \not\models f_1 \)

\( M, s \models f_1 \lor f_2 \)

\( \Leftrightarrow \)

\( M, s \models f_1 \) or \( M, s \models f_2 \)

\( M, s \models f_1 \land f_2 \)

\( \Leftrightarrow \)

\( M, s \models f_1 \) and \( M, s \models f_2 \)

\( M, s \models \bm{E} g_1 \)

\( \Leftrightarrow \)

there is an infinite path \( \pi \) starting from \( s \) such that \( M, \pi \models g_1 \)

graph TB s0(( )) --> s1(( )) s0 --> s2(( )) s1 --> s3(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6(( )) style s0 fill:#bbb style s2 fill:#bbb style s5 fill:#bbb

\( M, s \models \bm{A} g_1 \)

\( \Leftrightarrow \)

for every infinite path \( \pi \) starting from \( s \) we have \( M, \pi \models g_1 \)

graph TB s0(( )) --> s1(( )) s0 --> s2(( )) s1 --> s3(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6(( )) classDef node fill:#bbb

\( M, \pi \models f_1 \)

\( \Leftrightarrow \)

\( s \) is the first state of \( \pi \), and \( M, s \models f_1 \)

graph LR s0(("f1")) --> s1(( )) --> s2(( )) --> s3(( )) --> s4(( ))

\( M, \pi \models \lnot g_1 \)

\( \Leftrightarrow \)

\( M, \pi \not\models g_1 \)

\( M, \pi \models g_1 \lor g_2 \)

\( \Leftrightarrow \)

\( M, \pi \models g_1 \) or \( M, \pi \models g_2 \)

10.

\( M, \pi \models g_1 \land g_2 \)

\( \Leftrightarrow \)

\( M, \pi \models g_1 \) and \( M, \pi \models g_2 \)

11.

\( M, \pi \models \bm{X} g_1 \)

\( \Leftrightarrow \)

\( M, \pi^{1} \models g_1 \)

graph LR x0 --> x1 subgraph g1 x1 --> x2 --> x3 --> x4 end x0(( )) x1(( )) x2(( )) x3(( )) x4(( ))

12.

\( M, \pi \models \bm{F} g_1 \)

\( \Leftrightarrow \)

there exists a \( k \geq 0 \) such that \( M, \pi^{k} \models g_1 \)

graph LR f0 --> f1 --> f2 --> f3 subgraph g1 f3 --> f4 end f0(( )) f1(( )) f2(( )) f3(( )) f4(( ))

13.

\( M, \pi \models \bm{G} g_1 \)

\( \Leftrightarrow \)

for all \( i \geq 0 \), \( M, \pi^{i} \models g_1 \)

graph LR subgraph g1-0 [g1] s0 --> s1 subgraph g1-1 [g1] s1 --> s2 subgraph g1-2 [g1] s2 --> s3 subgraph g1-3 [g1] s3 --> s4 subgraph g1-4 [g1] s4 end end end end end s0(( )) s1(( )) s2(( )) s3(( )) s4(( ))

14.

\( M, \pi \models g_1 \bm{U} g_2 \)

\( \Leftrightarrow \)

there exists a \( k \geq 0 \) such that \( M, \pi^{k} \models g_2 \) and
for all \( 0 \leq j < k, M, \pi^{i} \models g_1 \)

graph LR subgraph g1-0 [g1] u0 --> u1 subgraph g1-1 [g1] u1 --> u2 subgraph g1-2 [g1] u2 --> u3 subgraph g2 u3 --> u4 end end end end u0(( )) u1(( )) u2(( )) u3[ ] u4(( )) style g2 fill:#ccff99

15.

\( M, \pi \models g_1 \bm{R} g_2 \)

\( \Leftrightarrow \)

for all \( j \geq 0 \), if for every \( i < j, M, \pi^{i} \not\models g_1 \), then
\( M, \pi^{j} \models g_2 \)

graph LR subgraph g2-0 ["g2 (¬g1)"] r0 --> r1 subgraph g2-1 ["g2 (¬ g1)"] r1 --> r2 subgraph g2-2 ["g2 (¬ g1)"] r2 --> r3 subgraph g1 ["g1 ∧ g2"] r3 --> r4 end end end end r0[ ] r1[ ] r2[ ] r3( ) r4(( )) style g1 fill:#ccff99

graph LR subgraph g2-0 ["g2 (¬g1)"] r0 --> r1 subgraph g2-1 ["g2 (¬ g1)"] r1 --> r2 subgraph g2-2 ["g2 (¬ g1)"] r2 --> r3 subgraph g1 ["g2 (¬ g1)"] r3 --> r4 end end end end style r4 fill:#FFFFFF, stroke:#FFFFFF r0[ ] r1[ ] r2[ ] r3[ ] r4[...]

16.

\( M \models f_1 \)

\( \Leftrightarrow \)

for all \( s \in S_0, M, s \models f_1 \)

Go to CTL* Complex Semantics.

Some properties

\( \lor, \lnot, \bm{X}, \bm{U} \) and \( \bm{E} \) are sufficient to express any CTL* formula:
\[ \begin{array}\\ f \land g &\equiv& \lnot ( \lnot f \lor \lnot g ) \\ f \bm{R} g &\equiv& \lnot ( \lnot f \bm{U} \lnot g) \\ \bm{F} f &\equiv& true \bm{U} f \\ \bm{G} f &\equiv& \lnot \bm{F} \lnot f \\ \bm{A}(f) &\equiv& \lnot \bm{E} (\lnot f) \end{array} \]
Clause 16 has an unexpected effect if \( M \) has multiple initial states:
- \( S_0 = \{ s_0, s_1 \} \)
- \( M, s_0 \models \bm{EX} p \) and \( M, s_1 \not\models \bm{EX} p \)
- \( M \not\models \bm{EX} p \) because \( M, s_1 \not\models \bm{EX} p \)
- \( M \not\models \lnot \bm{EX} p \) because \( M, s_0 \models \bm{EX} p \)
- Consequently, neither \( \bm{EX} p \) nor \( \lnot \bm{EX} p \) holds in \( M \)

graph TB start0 --> s0 start1 --> s1 s0 --> s2 s0 --> s3 s1 --> s3 s2 --> s2 s3 --> s3 style start0 fill:#FFFFFF, stroke:#FFFFFF style start1 fill:#FFFFFF, stroke:#FFFFFF start0(( )) start1(( )) s0((s0)) s1((s1)) s2(("s2
{p}")) s3(("s3
{¬p}"))

4.2.3 Negation Normal Form(NNF)

Negation normal form (NNF):

A syntactic form of logical formulas
Negations are applied only to atomic propositions
- ex) \( \bm{AG} ( \lnot p \bm{R} \lnot q ) \)
NNF of CTL* is useful for model checking.

CTL* \( \Leftrightarrow \) NNF of CTL*: \[ \begin{array} \\ \lnot \bm{A} \phi &\equiv& \bm{E} \lnot \phi \\ \lnot \bm{E} \phi &\equiv& \bm{A} \lnot \phi \\ \lnot \bm{G} \phi &\equiv& \bm{F} \lnot \phi \\ \lnot \bm{F} \phi &\equiv& \bm{G} \lnot \phi \\ \lnot \bm{X} \phi &\equiv& \bm{X} \lnot \phi \\ \lnot ( \phi \bm{U} \psi ) &\equiv& ( \lnot \phi \bm{R} \lnot \psi ) \\ \lnot ( \phi \bm{R} \psi ) &\equiv& ( \lnot \phi \bm{U} \lnot \psi ) \\ \lnot ( \phi \land \psi ) &\equiv& ( \lnot \phi \lor \lnot \psi ) \\ \lnot ( \phi \lor \psi ) &\equiv& ( \lnot \phi \land \lnot \psi ) \\ \end{array} \]

\( \lnot ( p \bm{U} q ) \equiv ( \lnot p \bm{R} \lnot q ) \):

\( p \bm{U} q \)
- \( q \) will hold at some point and
- \( p \) hold anytime at every preceding state which holds \( q \)
\( \lnot ( p \bm{U} q ) \)
- \( q \) won't hold forever or
- \( \lnot p \) hold at a preceding state which holds \( q \)
\( \lnot p \bm{R} \lnot q \)
- \( \lnot q \) will hold globally or
- \( \lnot p \) release \( \lnot q \)

\( p \bm{U} q \)

graph LR u0 --> u1 --> u2 --> u3 --> u4 style u4 fill:#FFFFFF, stroke:#FFFFFF u0(("p, ¬ q")) u1(("p, ¬ q")) u2(("p, ¬ q")) u3[q] u4((...))

\( \lnot ( p \bm{U} q ) \)

graph LR u0 --> u1 --> u2 --> u3 --> u4 style u4 fill:#FFFFFF, stroke:#FFFFFF u0(("p, ¬ q")) u1("¬ p, ¬ q") u2(("p, ¬ q")) u3[q] u4((...))

\( \lnot p \bm{R} \lnot q \)

graph LR r0 --> r1 --> r2 --> r3 --> r4 --> r5 style r4 fill:#FFFFFF, stroke:#FFFFFF r0(("p, ¬ q")) r1(("p, ¬ q")) r2(("p, ¬ q")) r3("¬ p, ¬ q") r4((...)) r5["q"]

Example

\[ \lnot(( A \bm{U} B) \lor \bm{F} C) \equiv ( \lnot (A \bm{U} B) \land \lnot \bm{F} C) \equiv (\lnot A \bm{R} \lnot B) \land \bm{G} \lnot C \]

Some properties

The conversion of a CTL* formula to NNF is linear in the size of the formula.
- This is true for many fragments of CTL*.
\( \land, \lor, \bm{E}, \bm{A}, \bm{X}, \bm{U}, \bm {R} \) are sufficient to express any NNF of CTL* formula:
- A reduction to \( \bm{E}, \bm{X}, \bm{U} \) is not possible.

4.3 Temporal Logics Based on CTL*

In this section, we consider several sublogics of CTL*.

We can divide the sublogics into two groups:

Branching-time logics (CTL, ACTL*, ACTL)
- Describe properties about sub-trees (states)
- Multiple \( \bm{A}, \bm{E} \)
  - ex) \( \bm{AGEF} p \)
Linear-time logics (LTL)
- Describe properties about a single path
- Single \( \bm{A} \)
  - ex) \( \bm{AFG} p \)

Branching-time logics

graph TB s0(( )) --> s1(( )) s0(( )) --> s2(( )) s2 --> s5(( )) s2 --> s6(( )) s5 --> s11(( )) s5 --> s12(( )) s6 --> s13(( )) s6 --> s14(( )) subgraph subtree s1 --> s3(( )) s1 --> s4(( )) s3 --> s7(( )) s3 --> s8(( )) s4 --> s9(( )) s4 --> s10(( )) end style s0 fill:#aaa style s1 fill:#aaa style s3 fill:#aaa style s4 fill:#aaa style s7 fill:#aaa style s8 fill:#aaa style s9 fill:#aaa style s10 fill:#aaa

Linear-time logics

graph TB s0(( )) --> s1(( )) s0(( )) --> s2(( )) s1 --> s3(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6(( )) s3 --> s7(( )) s3 --> s8(( )) s4 --> s9(( )) s4 --> s10(( )) s5 --> s11(( )) s5 --> s12(( )) s6 --> s13(( )) s6 --> s14(( )) style s0 fill:#aaa style s1 fill:#aaa style s4 fill:#aaa style s9 fill:#aaa

All four logics have:

syntactic restriction of CTL*.
the same semantics of CTL*.

4.3.1 The Branching-Time Logic CTL

CTL is CTL* with one restriction:

Path quantifier and temporal operator always occur in pairs.
- ex) \( \bm{AX} \phi, \bm{EG} \phi, \bm{AXEG} \phi \)
We can assume that CTL have ten temporal operators:
- \( \{ \bm{A}, \bm{E} \} \times \{ \bm{X}, \bm{F}, \bm{G}, \bm{U}, \bm{R} \} \)
Ten temporal operators are state formulas.
- Specifying a state \( s \) means specifying the paths starting from \( s \).

\( s_0 \models \bm{EF} ( \bm{AX} p ) \)

graph TB subgraph all ["EF(AXp)"] s0 --> s1 s0 --> s2 s1 --> s3 s1 --> s4 s2 --> s5 s2 --> s6 s3 --> s7 s3 --> s8 s4 --> s9 s4 --> s10 s5 --> s11 s5 --> s12 s6 --> s13 s6 --> s14 end style s0 fill:#bbb style s3 fill:#bbb style s7 fill:#bbb style s8 fill:#bbb s0(( )) s1(( )) s2(( )) s3(( )) s4(( )) s5(( )) s6(( )) s7((p)) s8((p)) s9(( )) s10(( )) s11(( )) s12(( )) s13(( )) s14(( ))

\( s_4 \models \bm{AX} p \)

graph TB s0 --> s1 s0 --> s2 s1 --> s3 s1 --> s4 s2 --> s5 s2 --> s6 s3 --> s7 s3 --> s8 subgraph subtree ["AXp"] s4 --> s9 s4 --> s10 end s5 --> s11 s5 --> s12 s6 --> s13 s6 --> s14 style s4 fill:#bbb style s9 fill:#bbb style s10 fill:#bbb s0(( )) s1(( )) s2(( )) s3(( )) s4(( )) s5(( )) s6(( )) s7(( )) s8(( )) s9((p)) s10((p)) s11(( )) s12(( )) s13(( )) s14(( ))

Syntax

If \( p \in AP \), then \( p \) is a CTL formula.

If \( f \) is a CTL formula, then \( \lnot f, \bm{AX} f, \bm{EX} f, \bm{AF} f, \bm{EF} f, \bm{AG} f, \) and \( \bm{EG} f \) are CTL formulas.

If \( f \) and \( g \) are CTL formulas, then \( f \land g, f \lor g, \bm{A}(f \bm{U} g), \bm{E}(f \bm{U} g), \bm{A}(f \bm{R} g), \) and \( \bm{E}(f \bm{R} g) \) are CTL formulas.

Some Properties

CTL operators can be expressed using three operators \( \bm{EX}, \bm{EG} \) and \( \bm{EU} \): \[ \begin{array} \\ \bm{AX} f &\equiv& \lnot \bm{EX} (\lnot f) \\ \bm{EF} f &\equiv& \bm{E} (true \bm{U} f) \\ \bm{AG} f &\equiv& \lnot \bm{EF} (\lnot f) \\ \bm{AF} f &\equiv& \lnot \bm{EG} (\lnot f) \\ \bm{A} (f \bm{U} g) &\equiv& \lnot \bm{E} (\lnot g \bm{U} (\lnot f \land \lnot g)) \land \lnot \bm{EG} \lnot g \\ \bm{A} (f \bm{R} g) &\equiv& \lnot \bm{E} (\lnot f \bm{U} \lnot g) \\ \bm{E} (f \bm{R} g) &\equiv& \lnot \bm{A} (\lnot f \bm{U} \lnot g) \end{array} \]

\( \bm{A} (f \bm{U} g) = \bm{AF} g \land \bm{A} (g \bm{R} (f \lor g)) \)

\( f \bm{U} g \)
- \( \bm{F} g \): \( g \) will hold
- \( g \bm{R} ( f \lor g ) \): \( f \) hold at every preceding state

\( g \bm{R} (f \lor g) \)

graph LR u0 --> u1 --> u2 --> u3 --> u4 u0((f)) u1((f)) u2((f)) u3[g] u4(( ))

Semantics

We define CTL using \( \bm{EX}, \bm{EG} \) and \( \bm{EU} \).

\( M, s \models p \) for \( p \in AP \)

\( \Leftrightarrow \)

\( p \in L(s) \)

\( M, s \models \lnot f\)

\( \Leftrightarrow \)

\( M, s \not\models f \)

\( M, s \models f_1 \lor f_2 \)

\( \Leftrightarrow \)

\( M, s \models f_1 \) or \( M, s \models f_2 \)

\( M, s \models f_1 \land f_2 \)

\( \Leftrightarrow \)

\( M, s \models f_1 \) and \( M, s \models f_2 \)

\( M, s \models \bm{EX} f \)

\( \Leftrightarrow \)

there exists a state t such that \( R(s, t) \) and \( M, t \models f \)

\( M, s \models \bm{EG} f \)

\( \Leftrightarrow \)

there exists an infinite path \( \pi \) starting at \( s \) such that for all \( i \geq 0, M, s_i \models f \)

\( M, s \models \bm{E} (f_1 \bm{U} f_2) \)

\( \Leftrightarrow \)

there exists an infinite path \( \pi \) starting at \( s \) and there exists a \( k \geq 0 \) such that \( M, s_k \models f_2 \) and for all \( 0 \leq j < k, M, s_j \models f_1 \)

\( M \models f\)

\( \Leftrightarrow \)

for all \( s \in S_0, M, s \models f \)

The remaining seven CTL operators can be introduced.

Basic CTL operators

\( M, s_0 \models \bm{EF} g \)

graph TB s0(( )) --> s1(( )) --> s3(( )) s0 --> s2(( )) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6((g))

\( M, s_0 \models \bm{EG} g \)

graph TB s0((g)) --> s1(( )) --> s3(( )) s0 --> s2((g)) s1 --> s4(( )) s2 --> s5(( )) s2 --> s6((g))

\( M, s_0 \models \bm{AF} g \)

graph TB s0(( )) --> s1((g)) --> s3(( )) s0 --> s2(( )) s1 --> s4(( )) s2 --> s5((g)) s2 --> s6((g))

\( M, s_0 \models \bm{AG} g \)

graph TB s0((g)) --> s1((g)) --> s3((g)) s0 --> s2((g)) s1 --> s4((g)) s2 --> s5((g)) s2 --> s6((g))

Subformulas

Subformulas of a CTL formula are inner CTL formulas.

Subformulas of \( \bm{AXEX} p \) about CTL syntax
- \( \bm{AXEX} p \)
- \( \bm{EX} p \)
- \( p \)

Note that subformulas of a CTL* formula are inner CTL* formulas.

Subformulas of \( \bm{AXEX} p \) about CTL* syntax
- \( \bm{AXEX} p \)
- \( \bm{XEX} p \)
- \( \bm{EX} p \)
- \( \bm{X} p \)
- \( p \)

4.3.2 The Universal Computation Tree Logics ACTL* and ACTL

ACTL*

ACTL* have two restrictions compared to CTL*:

Only the universal path quantification \( \bm{A} \) is allowed (\( \bm{E} \) is not allowed).
NNF (Negation Normal Form): negation are applied only to atomic propositions.
- \( \because \) We can express \( \bm{E} \) using \( \lnot \bm{A} \)
  - ex) \( \lnot \bm{A}p = \bm{E} \lnot p \)
ex) \( \bm{AX} \lnot p, \bm{AXAFG} (p \lor \lnot q) \)

Syntax of ACTL*

State formulas:

If \( p \in AP \), then \( p \) and \( \lnot p \) are ACTL* state formulas.

If \( f \) and \( g \) are ACTL* state formulas, then \( f \lor g \) and \( f \land g \) are ACTL* state formulas.

If \( f \) is an ACTL* path formula, then \( \bm{A} f \) is an ACTL* state formula.

Path formulas:

If \( f \) is an ACTL* state formula, then \( f \) is also an ACTL* path formula.

If \( f \) and \( g \) are ACTL* path formulas, then \( f \lor g, f \land g, \bm{X} f, \bm{F} f, \bm{G} f, f \bm{U} g \), and \( f \bm{R} g \) are ACTL* path formulas.

Some topics

ECTL* is defined analogously with \( \bm{E} \) instead of \( \bm{A} \).
\( \bm{X}, \bm{U}, \bm{R} \) are sufficient to express ACTL* and ECTL*.
- See Some properties of CTL*

ACTL

ACTL have one more restriction of ACTL*:

Path quantifier and Temporal operators always occur in pairs.
- \( \{ \bm{A} \} \times \{ \bm{X}, \bm{F}, \bm{G}, \bm{U}, \bm{R} \} \)

Syntax of ACTL

If \( p \in AP \), then \( p \) and \( \lnot p \) are ACTL formulas.

If \( f \) is an ACTL formula, then \( \bm{AX} f, \bm{AF} f \), and \( \bm{AG} f \) are ACTL formulas.

If \( f \) and \( g \) are ACTL formulas, then \( f \land g, f \lor g, \bm{A} (f \bm{U} g), \bm{A} (f \bm{R} g) \) are ACTL formulas.

Some topics

\( \bm{AX}, \bm{AU}, \bm{AR} \) are sufficient to express ACTL.
- See Some properties of CTL

4.3.3 Linear Temporal Logic LTL

LTL formulas describe properties of a single path.

Syntax: \( \bm{A} f \)
- \( f \): path formula
Semantics: Satisfies \( f \) for all paths
ex) \( \bm{AFGX} p, \bm{AG} (p \bm{R} q) \)

\( s_0 \models \bm{A} ( \bm{FG} p ) \)

graph TB s0 --> s1 s0 --> s2 s1 --> s3 s1 --> s4 s2 --> s5 s2 --> s6 s3 --> s7 s3 --> s8 s4 --> s9 s4 --> s10 s5 --> s11 s5 --> s12 s6 --> s13 s6 --> s14 classDef node fill:#bbb s0(( )) s1(( )) s2((p)) s3((p)) s4(( )) s5((p)) s6(( )) s7((p)) s8(( )) s9(( )) s10(( )) s11((p)) s12((p)) s13(( )) s14(( ))

\( \{ \pi_0, \pi_1, ... \} \models \bm{FG} p \)

graph TB s0 --> s1 s0 --> s2 s1 --> s3 s1 --> s4 s2 --> s5 s2 --> s6 s3 --> s7 s3 --> s8 s4 --> s9 s4 --> s10 s5 --> s11 s5 --> s12 s6 --> s13 s6 --> s14 style s0 fill:#bbb style s1 fill:#bbb style s3 fill:#bbb style s7 fill:#bbb s0(( )) s1(( )) s2((p)) s3((p)) s4(( )) s5((p)) s6(( )) s7((p)) s8(( )) s9(( )) s10(( )) s11((p)) s12((p)) s13(( )) s14(( ))

Syntax of LTL

LTL formulas:

If \( f \) is a LTL path formula, then \( \bm{A} f \) is a LTL formula.

LTL path formulas:

If \( p \in AP \), then \( p \) is an LTL path formula.

If \( f \) is an LTL path formula, then \( \lnot f, \bm{X} f, \bm{F} f \) and \( \bm{G} f \) are LTL path formulas.

If \( f \) and \( g \) are LTL path formulas, then \( f \land g, f \lor g, f \bm{U} g \) and \( f \bm{R} g \) are LTL path formulas.

Some topics

\( \bm{X} \) and \( \bm{U} \) are sufficient to express other operators.
- See Some properties of CTL*
We can omit \( \bm{A} \) because LTL formulas must have \( \bm{A} \).
- \( M \models f \) means \( M \models \bm{A} f \).

4.3.4 Relationships between Fragments of CTL*

Five logics have different expressive powers.

CTL*: most powerful
- OK: \( \bm{AFG} p, \bm{AG}(\bm{EF}p), \bm{AFG}p \lor \bm{AG}(\bm{EF}p) \)
CTL: path quantifier + temporal operator
- OK: \( \bm{AG}(\bm{EF}p) \)
- NG: \( \bm{AFG}p, \bm{AFG}p \lor \bm{AG}(\bm{EF}p)\)
LTL: \( \bm{A} f \)
- OK: \( \bm{AFG} p \)
- NG: \( \bm{AG}(\bm{EF}p), \bm{AFG}p \lor \bm{AG}(\bm{EF}p) \)

Question: Classify the following formulas

\( \bm{AXG}p, \bm{EG}p, \bm{AGAXF}p \)

Q1. CTL

\( \bm{EG}p \)

Q2. LTL

\( \bm{AXG}p \)

Q3. ACTL*

\( \bm{AXG}p, \bm{AGAXF}p \)

4.4 Temporal Logic with Set Atomic Propositions and Set Semantics

In logics, a formula can be expressed by sets.
\[ 0 < \phi < 3 = \{ \phi = 1, \phi = 2 \} \]

In temporal logics, a formula can be express by sets of states.
\[ [\![ \bm{EX} (b \land c) ]\!]_{M} = \{ s_0, s_3, ... \} \]

graph TB START --> s0 s0 --> s1 s0 --> s2 s1 --> s3 --> dots0 s3 --> dots1 s1 --> s4 --> dots2 s2 --> s5 --> dots3 style START fill:#FFFFFF, stroke:#FFFFFF style dots0 fill:#FFFFFF, stroke:#FFFFFF style dots1 fill:#FFFFFF, stroke:#FFFFFF style dots2 fill:#FFFFFF, stroke:#FFFFFF style dots3 fill:#FFFFFF, stroke:#FFFFFF START(( )) dots0((π0)) dots1((...)) dots2((...)) dots3((π1)) s0(("s0
{a,b}")) s1(("s1
{b,c}")) s2(("s2
{c}")) s3(("s3
{a,b}")) s4(("s4
{c}")) s5(("s5
{c}"))

Formal Definition

\[ [\![ f ]\!]_{M} := \{ s \in S \mid M, s \models f \} \]

Set Atomic Proposition

Syntax

Extension of CTL* with set atomic proposition

If \( \{ s_0, ..., s_n \} \in S \), then \( \{ s_0, ..., s_n \} \) is a CTL* state formula called set atomic proposition.

Semantics

1a.

\( M, s \models \{ s_0, s_1, ..., s_n \} \)

\( \Leftrightarrow \)

\( s \in \{ s_0, s_1, ..., s_n \} \)

Example

\( M,s_1 \models \bm{EX} \{ s_3, s_5 \} \)
\( M,s_2 \models \bm{EX} \{ s_3, s_5 \} \)

4.5 Fairness

Please see the Kripke structure.
Do you think \( \pi_0 = \{ s_0, s_0, ..., s_0, ... \}, \pi_1 = \{ s_0, s_1, s_1, ..., s_1, ... \} \) is realistic?

graph LR start --> s0 --> s1 --> s0 s0 --> s0 s1 --> s1 style start fill:#FFFFFF, stroke:#FFFFFF start(( )) s0(("s0
{a}")) s1(("s1
{b}"))

NO!!
We want to remove \( \pi_0, \pi_1 \) → fairness constraints

Fairness constraints

Fairness constraints define the set of states that we want the system to visit fairly.

\( F = \{ P_1, ..., P_k \} \subseteq 2^S \)

In example, \( F = \{ \{ s_0 \}, \{ s_1 \} \} \).

Fair Path

In example, we want to define that the path \( \pi \) is fair if:

\( \pi \) visit \( s_0 \) many times and
\( \pi \) visit \( s_1 \) many times.

Formal Definition

\[ \textit{inf}(\pi) = \{ s \mid s = s_i \text{ for infinitely many } i \} \] We define that \( \pi \) is fair if and only if \[ \text{for every } P \in F, \textit{inf}(\pi) \cap P \neq \{\} \]

Example

Fairness Constraints: \( F = \{ \{ s_0 \}, \{ s_1 \} \} \)

graph LR start --> s0 --> s1 --> s0 s0 --> s0 s1 --> s1 style start fill:#FFFFFF, stroke:#FFFFFF start(( )) s0(("s0
{a}")) s1(("s1
{b}"))

Check whether \( \pi_0 = \{ s_0, s_0, ..., s_0, ... \} \) is fair:

\( \textit{inf} (\pi_0) = \{ s_0 \} \)
\( \text{for every } P \in F, \textit{inf}(\pi) \cap P \neq \{\} \)
- \( \textit{inf}(\pi_0) \cap P_1 = \{ s_0 \} \cap \{ s_0 \} = \{ s_0 \} \neq \{\} \)
- \( \textit{inf}(\pi_0) \cap P_2 = \{ s_0 \} \cap \{ s_1 \} = \{\} \)

Check whether \( \pi_2 = \{ s_0, s_1, s_0, s_1, ..., s_0, s_1, ... \} \) is fair:

\( \textit{inf} (\pi_2) = \{ s_0, s_1 \} \)
\( \text{for every } P \in F, \textit{inf}(\pi) \cap P \neq \{\} \)
- \( \textit{inf}(\pi_2) \cap P_1 = \{ s_0, s_1 \} \cap \{ s_0 \} = \{ s_0 \} \neq \{\} \)
- \( \textit{inf}(\pi_2) \cap P_2 = \{ s_0, s_1 \} \cap \{ s_1 \} = \{ s_1 \} \neq \{\} \)

Fairness in CTL*

\[ fpath := \bigwedge_{P \in F} \bigvee_{s \in P} \bm{GF} \{s\} \] \( \bm{GF} \{s\} \) means \( s \) appears infinitely.

graph LR s0(( )) --> s1((s)) --> s2(( )) --> s3((s)) --> s4((s)) --> s5(( )) --> s6(( )) --> s7((s))

In example, \( fpath = \bm{GF} \{ s_0 \} \land \bm{GF} \{ s_1 \} \).

Fairness can be added into CTL* syntax:

\( \bm{E} ( fpath \land \phi ) \)
- There exists a path that is fair and satisfies \( \phi \).
\( \bm{A} ( fpath \rightarrow \phi ) \)
- For every path, if it is fair, then it must satisfies \( \phi \).
  - We focus on fair paths.
  - We can ignore no-fair paths. (e.g, \( \pi_0, \pi_1 \) )
- If we define \( \bm{A} ( fpath \land \phi ) \), we cannot check the properties of \( s_0 \).
  - \( \bm{A} (fpath \land \phi) = \bm{A} (fpath) \land \bm{A} \phi = \{\} \)

graph LR start --> s0 --> s1 --> s0 s0 --> s0 s1 --> s1 style start fill:#FFFFFF, stroke:#FFFFFF start(( )) s0(("s0
{a}")) s1(("s1
{b}"))

Fairness in CTL

In CTL, we cannot express \( \bm{GF} \) because of its syntax rules.
In order to deal with fairness in CTL, we use a fair Kripke structure \( M \) and modify its semantics.

Fair Kripke structure \( M = \{ S, S_0, R, AP, L, F \} \)

\( M, s \models_{F} \bm{E} g_1 \)

\( \Leftrightarrow \)

there exists a fair path \( \pi \) starting from \( s \) such that \( \pi \models_{F} g_1 \).

\( M, s \models_{F} \bm{A} g_1 \)

\( \Leftrightarrow \)

for all fair paths \( \pi \) starting from \( s \), \( \pi \models_{F} g_1 \).

4.6 Counterexamples

Counterexamples are paths that demonstrate the violation of specifications.

How to get:
1. Modeling programs
2. Specification of some properties
3. Model Checking!
4. Get counterexamples if the programs don't satisfy the properties.
Requirement:
- Easy-to-understand description
- A finite representation

Simple Specification \( \bm{AX} p \)

Counterexample of \( \bm{AX} p \) is a path that holds \( \bm{X} \lnot p \).

graph TB s0 --> s1 s0 --> s2 style s0 fill:#bbb style s1 fill:#bbb s0(( )) s1(("¬p")) s2((p))

Specification \( \bm{AG} p \)

Counterexample of \( \bm{AG} p \) is a finite path that holds \( \bm{F} \lnot p \).
(The counterexample is a witness for \( \lnot \bm{AG} p = \bm{EF} \lnot p \).)

graph LR s0((p)) --> s1((p)) --> s2((p)) --> dots --> s3(("¬p")) style dots fill:#FFFFFF, stroke:#FFFFFF dots(("..."))

Specification \( \bm{AF} p \)

Counterexample of \( \bm{AF} p \) is an infinite path, all of its states satisfying \( \lnot p \).
(The counterexample is a witness for \( \lnot \bm{AF} p = \bm{EG} \lnot p \).)
For finite Kripke structures, a counterexample \( \pi \) exists: \[ \pi = \pi_0 ( \pi_1 )^\omega = \pi_0 \pi_1 \pi_1 \pi_1 ...\] A path of that form is called lasso.

graph LR s0(("¬p")) --> s1(("¬p")) --> s2(("¬p")) --> dots --> s3(("¬p")) --> s4(("¬p")) --> dots2 --> s5(("¬p")) s5 --> s3 style dots fill:#FFFFFF, stroke:#FFFFFF style dots2 fill:#FFFFFF, stroke:#FFFFFF dots(("...")) dots2(("..."))

Prove the existence of a lasso-shape counterexample

Assumptions:

The number of states are finite. (from Kripke structure)
Paths are infinite. (from left-total)

Proof:

Let the path \( \pi = s_0, s_1, ... \) be a counterexample for \( \bm{AF} p \).
- for all \( s_i \) we have \( M, s_i \models \lnot p \).
There must be two indices \( 1 \leq n < m \) such that \( s_n = s_m \)
- because of Assumption-1 and 2.
We can form \( \pi = \pi_0 (\pi_1^{\omega}) \) such that:
- \( \pi_0 = s_0, ... s_{n-1} \)
- \( \pi_1 = s_n, ..., s_{m-1} \)

This can prove that every LTL formula has a lasso-shaped counterexample.

4.7 Safety and Liveness Properties

Safety Property

A safety property guarantees that something wrong will never happen.

ex) An error state is never reached.

A safety property is expressed as \( \bm{AG} p \).
If a safety property is violated, there is a finite execution that a "bad" event occurs.
- Counterexample is a path that holds \( \bm{F} \lnot p \). (See \( \bm{AG} p \))

Liveness Property

A liveness property guarantees that something good will eventually happen.

ex) The program eventually finish.

A liveness property is expressed as \( \bm{AF} p \) or \( \bm{A}(p \bm{U} q) \).
If a liveness property is violated, there is a lasso-shaped counterexample.
- Counterexample is an infinite path that holds \( \bm{G} \lnot p \). (See \( \bm{AF} p \))

Overview

Contents

Introduction to Temporal Logic

Propositional Logic

Syntax

Example

Temporal Logic

Syntax

Example

Propositional Logic vs. Temporal Logic

4.1 The Computation Tree Logic CTL*

Computation Tree

CTL*

CTL* Formulas

Example

4.2 Syntax and Semantics of CTL*

4.2.1 Syntax of CTL*

Example of A.4

Examples of formulas

4.2.2 Semantics of CTL*

Preparation for semantic definitions

Review: Kripke structure \( M \)

Path \( \pi \) in \( M \)

The modeling relation \( \models \) and Equivalence \( \equiv \)

Definition: Semantics of CTL*

Some properties

4.2.3 Negation Normal Form(NNF)

Example

Some properties

4.3 Temporal Logics Based on CTL*

4.3.1 The Branching-Time Logic CTL

Syntax

Some Properties

Semantics

Basic CTL operators

Subformulas

4.3.2 The Universal Computation Tree Logics ACTL* and ACTL

ACTL*

Syntax of ACTL*

Some topics

ACTL

Syntax of ACTL

Some topics

4.3.3 Linear Temporal Logic LTL

Syntax of LTL

Some topics

4.3.4 Relationships between Fragments of CTL*

Question: Classify the following formulas

4.4 Temporal Logic with Set Atomic Propositions and Set Semantics

Formal Definition

Set Atomic Proposition

Syntax

Semantics

Example

4.5 Fairness

Fairness constraints

Fair Path

Formal Definition

Example

Fairness in CTL*

Fairness in CTL

4.6 Counterexamples

Simple Specification \( \bm{AX} p \)

Specification \( \bm{AG} p \)

Specification \( \bm{AF} p \)

Prove the existence of a lasso-shape counterexample

4.7 Safety and Liveness Properties

Safety Property

Liveness Property