KEMBAR78
LTL for Computer Science Students | PDF | Metalogic | Mathematics Of Computing
Scribd
Upload
80 views44 pages

LTL for Computer Science Students

The document discusses the semantics of linear temporal logic (LTL). It defines LTL formulas over a set of atomic propositions AP and the set of infinite words over the power set of AP (AP-INF). It provides examples of LTL properties, such as "p1 is always true". It explains that an LTL formula defines a subset of AP-INF consisting of words that satisfy the formula. The semantics of LTL operators like conjunction, negation, next, and until are defined in terms of how they affect word satisfaction.

Uploaded by

John Doe
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
80 views44 pages

LTL for Computer Science Students

The document discusses the semantics of linear temporal logic (LTL). It defines LTL formulas over a set of atomic propositions AP and the set of infinite words over the power set of AP (AP-INF). It provides examples of LTL properties, such as "p1 is always true". It explains that an LTL formula defines a subset of AP-INF consisting of words that satisfy the formula. The semantics of LTL operators like conjunction, negation, next, and until are defined in terms of how they affect word satisfaction.

Uploaded by

John Doe
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/ 44

Unit-7: Linear Temporal Logic

B. Srivathsan

Chennai Mathematical Institute

NPTEL-course

July - November 2015

1/13
Module 2:
Semantics of LTL

2/13
AP-INF = set of infinite words over PowerSet(AP)

3/13
AP-INF = set of infinite words over PowerSet(AP)

Property 1: p1 is always true

3/13
AP-INF = set of infinite words over PowerSet(AP)

Property 1: p1 is always true

{ A0 A1 A2 · · · ∈ AP-INF | each Ai contains p1 }

{ p1 } { p1 } { p1 } { p1 } { p1 } { p1 } { p1 } . . .
{ p1 } { p1 , p2 } { p1 } { p1 , p2 } { p1 } { p1 , p2 } . . .
..
.

3/13
AP-INF = set of infinite words over PowerSet(AP)

Property 1: p1 is always true

{ A0 A1 A2 · · · ∈ AP-INF | each Ai contains p1 }

{ p1 } { p1 } { p1 } { p1 } { p1 } { p1 } { p1 } . . .
{ p1 } { p1 , p2 } { p1 } { p1 , p2 } { p1 } { p1 , p2 } . . .
..
.
Property 2: p1 is true at least once and p2 is always true

3/13
AP-INF = set of infinite words over PowerSet(AP)

Property 1: p1 is always true

{ A0 A1 A2 · · · ∈ AP-INF | each Ai contains p1 }

{ p1 } { p1 } { p1 } { p1 } { p1 } { p1 } { p1 } . . .
{ p1 } { p1 , p2 } { p1 } { p1 , p2 } { p1 } { p1 , p2 } . . .
..
.
Property 2: p1 is true at least once and p2 is always true

{ A0 A1 A2 · · · ∈ AP-INF | exists Ai containing p1 and every Aj contains p2 }

{ p2 } { p1 , p2 } { p2 } { p2 } { p2 } { p1 , p2 } { p2 } . . .
{ p1 , p2 } { p2 } { p2 } { p2 } { p2 } { p2 } . . .
.
..

3/13
AP-INF = set of infinite words over PowerSet(AP)

A property over AP is a subset of AP-INF

4/13
AP-INF = set of infinite words over PowerSet(AP)

A property over AP is a subset of AP-INF

LTL can be used to specify properties

4/13
AP-INF = set of infinite words over PowerSet(AP)

A property over AP is a subset of AP-INF

LTL can be used to specify properties

LTL can be used to describe subsets of AP-INF

4/13
{p1 } {p1 } {p1 } {p2 } {p1 }
p1 U p2 ...

:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP 1, 2 : LTL formulas

6/6

LTL formula φ −
→ Words(φ)

5/13
{p1 } {p1 } {p1 } {p2 } {p1 }
p1 U p2 ...

:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP 1, 2 : LTL formulas

6/6

LTL formula φ −
→ Words(φ) ⊆ AP-INF

5/13
{p1 } {p1 } {p1 } {p2 } {p1 }
p1 U p2 ...

:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP 1, 2 : LTL formulas

6/6

LTL formula φ −
→ Words(φ) ⊆ AP-INF

Words(φ): set of words in AP-INF that satisfy φ

5/13
When does a word satisfy LTL formula φ?

6/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6

7/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6
Every word satisfies true

7/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6
Every word satisfies true

σ satisfies pi if pi ∈ A0

7/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6
Every word satisfies true

σ satisfies pi if pi ∈ A0

σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

7/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6
Every word satisfies true

σ satisfies pi if pi ∈ A0

σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

σ satisfies ¬φ if σ does not satisfy φ

7/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6
Every word satisfies true

σ satisfies pi if pi ∈ A0

σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

σ satisfies ¬φ if σ does not satisfy φ

σ satisfies X φ if A1 A2 A3 . . . satisfies φ

7/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

pi 2 AP , 2 : LTL formulas
Word σ : A01A1 A 2 . . . ∈ AP- INF

6/6
Every word satisfies true

σ satisfies pi if pi ∈ A0

σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

σ satisfies ¬φ if σ does not satisfy φ

σ satisfies X φ if A1 A2 A3 . . . satisfies φ

σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and


for all 0 ≤ i < j Ai Ai+1 . . . satisfies φ1

7/13
Words(φ) = { σ ∈ AP-INF | σ satisfies φ }

8/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas

6/6
σ satisfies pi if pi ∈ A0

σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

σ satisfies ¬φ if σ does not satisfy φ

σ satisfies X φ if A1 A2 A3 . . . satisfies φ

σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and


for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1

9/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas
Words(true) = AP-INF
6/6
σ satisfies pi if pi ∈ A0

σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

σ satisfies ¬φ if σ does not satisfy φ

σ satisfies X φ if A1 A2 A3 . . . satisfies φ

σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and


for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1

9/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas
Words(true) = AP-INF
6/6
σ satisfies pi if pi ∈ A0
Words(pi ) = { A0 A1 A2 . . . | pi ∈ A0 }
σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2

σ satisfies ¬φ if σ does not satisfy φ

σ satisfies X φ if A1 A2 A3 . . . satisfies φ

σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and


for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1

9/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas
Words(true) = AP-INF
6/6
σ satisfies pi if pi ∈ A0
Words(pi ) = { A0 A1 A2 . . . | pi ∈ A0 }
σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2
Words(φ1 ∧ φ2 ) = Words(φ1 ) ∩ Words(φ2 )
σ satisfies ¬φ if σ does not satisfy φ

σ satisfies X φ if A1 A2 A3 . . . satisfies φ

σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and


for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1

9/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas
Words(true) = AP-INF
6/6
σ satisfies pi if pi ∈ A0
Words(pi ) = { A0 A1 A2 . . . | pi ∈ A0 }
σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2
Words(φ1 ∧ φ2 ) = Words(φ1 ) ∩ Words(φ2 )
σ satisfies ¬φ if σ does not satisfy φ
Words(¬φ) = (Words(φ))c
σ satisfies X φ if A1 A2 A3 . . . satisfies φ

σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and


for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1

9/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas
Words(true) = AP-INF
6/6
σ satisfies pi if pi ∈ A0
Words(pi ) = { A0 A1 A2 . . . | pi ∈ A0 }
σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2
Words(φ1 ∧ φ2 ) = Words(φ1 ) ∩ Words(φ2 )
σ satisfies ¬φ if σ does not satisfy φ
Words(¬φ) = (Words(φ))c
σ satisfies X φ if A1 A2 A3 . . . satisfies φ
Words(X φ) = { A0 A1 A2 . . . | A1 A2 · · · ∈ Words(φ) }
σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and
for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1

9/13
:= true | pi | 1 ^ 2 |¬ 1 | X | 1 U 2

Every word
pi 2 AP 1, 2satisfies true
: LTL formulas
Words(true) = AP-INF
6/6
σ satisfies pi if pi ∈ A0
Words(pi ) = { A0 A1 A2 . . . | pi ∈ A0 }
σ satisfies φ1 ∧ φ2 if σ satisfies φ1 and σ satisfies φ2
Words(φ1 ∧ φ2 ) = Words(φ1 ) ∩ Words(φ2 )
σ satisfies ¬φ if σ does not satisfy φ
Words(¬φ) = (Words(φ))c
σ satisfies X φ if A1 A2 A3 . . . satisfies φ
Words(X φ) = { A0 A1 A2 . . . | A1 A2 · · · ∈ Words(φ) }
σ satisfies φ1 U φ2 if there exists j s.t. Aj Aj+1 . . . satisfies φ2 and
for all 1 ≤ i < j Ai Ai+1 . . . satisfies φ1
Words(φ1 Uφ2 ) = { A0 A1 A2 . . . | ∃ j.Aj Aj+1 · · · ∈ Words(φ2 ) and
∀ 0 ≤ i < j. Ai Ai+1 · · · ∈ Words(φ1 ) }

9/13
F φ: true U φ

10/13
F φ: true U φ

σ satisfies true U φ if there exists j s.t. Aj Aj+1 . . . satisfies φ


and for all 0 ≤ i < j Ai Ai+1 . . . satisfies true

10/13
F φ: true U φ

σ satisfies true U φ if there exists j s.t. Aj Aj+1 . . . satisfies φ

10/13
F φ: true U φ

σ satisfies true U φ if there exists j s.t. Aj Aj+1 . . . satisfies φ

G φ: ¬F ¬φ

10/13
F φ: true U φ

σ satisfies true U φ if there exists j s.t. Aj Aj+1 . . . satisfies φ

G φ: ¬F ¬φ

σ satisfies F ¬ φ if there exists j s.t. Aj Aj+1 . . . satisfies ¬ φ

10/13
F φ: true U φ

σ satisfies true U φ if there exists j s.t. Aj Aj+1 . . . satisfies φ

G φ: ¬F ¬φ

σ satisfies F ¬ φ if there exists j s.t. Aj Aj+1 . . . satisfies ¬ φ

σ satisfies ¬ F ¬ φ if σ does not satisfy F ¬ φ

10/13
F φ: true U φ

σ satisfies true U φ if there exists j s.t. Aj Aj+1 . . . satisfies φ

G φ: ¬F ¬φ

σ satisfies F ¬ φ if there exists j s.t. Aj Aj+1 . . . satisfies ¬ φ

σ satisfies ¬ F ¬ φ if σ does not satisfy F ¬ φ

σ satisfies ¬ F ¬ φ if for all j Aj Aj+1 . . . satisfies φ

10/13
AP = { p1 , p2 }

Transition System Property

{ p1 } { p1 , p2 }
MODULE main
request=1 request=1
VAR
ready busy
request: boolean;
status: LTL formula φ
{ready, busy}
ASSIGN
init(status) := ready;
next(status) := case
request=0 request=0
request : busy;
ready busy
TRUE : {ready,busy};
{} { p2 } esac;

Atomic propositions
p1 : (request=1) p2 : (status=busy)

4/7

11/13
AP = { p1 , p2 }

Transition System Property

{ p1 } { p1 , p2 }
MODULE main
request=1 request=1
VAR
ready busy
request: boolean;
status: LTL formula φ
{ready, busy}
ASSIGN
init(status) := ready;
next(status) := case
request=0 request=0
request : busy;
ready busy
TRUE : {ready,busy};
{} { p2 } esac;

Atomic
Transition propositions
system TS satisfies formula φ if
p1 : (request=1) p2 : (status=busy)

Traces(TS) ⊆ Words(φ)
4/7

11/13
(Words(φ))c

Words(φ)

12/13
(Words(φ))c

Traces(TS)

Words(φ)

12/13
(Words(φ))c

Traces(TS)

Words(φ)

TS does not satisfy φ TS does not satisfy ¬φ

12/13
(Words(φ))c

Traces(TS)

Words(φ)

TS does not satisfy φ TS does not satisfy ¬φ

{ p1 } { p2 } { p2 }

12/13
(Words(φ))c

Traces(TS)

Words(φ)

TS does not satisfy φ TS does not satisfy ¬φ

{ p1 } { p2 } { p2 }

Above TS does not satisfy F p1 Above TS does not satisfy ¬F p1

12/13
Semantics of LTL

13/13

You might also like