Introduction to Model Checking

Dr. Falak Sher

Information Technology University, Punjab

Modeling, Verification and Synthesis Group

February 4, 2019

Dr. Falak Sher (ITU Punjab) Introduction to Model Checking September 11, 2017 1/2
Acknowledgement

Prof. Joost-Pieter Katoen Prof. Holger Hermanns

RWTH Aachen University Germany Saarland University Germany

Dr. Falak Sher (ITU Punjab) Introduction to Model Checking September 11, 2017 2/2
Overview overview2.1

Introduction
Modelling parallel systems
Transition systems ←−
Modeling hard- and software systems
Parallelism and communication
Linear Time Properties
Regular Properties
Linear Temporal Logic
Computation-Tree Logic
Equivalences and Abstraction

1 / 628
Transition systems Transsys/ts1.4-1

real system

semantics 
abstraction y
semantic model

2 / 628
Transition systems Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model

3 / 628
Transition systems Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:

4 / 628
Transition systems Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:
• the states of the system
• the stepwise behaviour
• the initial states

5 / 628
Transition systems Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:
• the states of the system
↑
control component + information on “relevant” data
• the stepwise behaviour
• the initial states

6 / 628
Transition systems =
b extended digraphs Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:
• the states of the system ←− nodes
↑
control component + information on “relevant” data
• the stepwise behaviour ←− edges
• the initial states

7 / 628
Transition systems =
b extended digraphs Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:
• the states of the system ←− nodes
↑
control component + information on “relevant” data
• the stepwise behaviour ←− transitions
• the initial states

8 / 628
Transition systems =
b extended digraphs Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:
• the states of the system ←− nodes
• the stepwise behaviour ←− transitions
• the initial states
• additional information on
communication
state properties
9 / 628
Transition systems =
b extended digraphs Transsys/ts1.4-1

real system
 x
semantics   implementation
abstraction y  refinement
semantic model
The semantic model yields a formal representation of:
• the states of the system ←− nodes
• the stepwise behaviour ←− transitions
• the initial states
• additional information on
communication ←− actions
state properties ←− atomic proposition
10 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)

11 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)
• S is the state space, i.e., set of states,

12 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)
• S is the state space, i.e., set of states,
• Act is a set of actions,

13 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)
• S is the state space, i.e., set of states,
• Act is a set of actions,
• −→ ⊆ S × Act × S is the transition relation,

14 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)
• S is the state space, i.e., set of states,
• Act is a set of actions,
• −→ ⊆ S × Act × S is the transition relation,
α
i.e., transitions have the form s −→ s ′
where s, s ′ ∈ S and α ∈ Act

15 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)
• S is the state space, i.e., set of states,
• Act is a set of actions,
• −→ ⊆ S × Act × S is the transition relation,
α
i.e., transitions have the form s −→ s ′
where s, s ′ ∈ S and α ∈ Act
• S0 ⊆ S the set of initial states,

16 / 628
Transition system (TS) ts1.4-TS-def

A transition system is a tuple

T = (S, Act, −→, S0, AP, L)
• S is the state space, i.e., set of states,
• Act is a set of actions,
• −→ ⊆ S × Act × S is the transition relation,
α
i.e., transitions have the form s −→ s ′
where s, s ′ ∈ S and α ∈ Act
• S0 ⊆ S the set of initial states,
• AP a set of atomic propositions,
• L : S → 2AP the labeling function
17 / 628
Transition system for beverage machine ts1.4-2

pay

select

coke sprite

18 / 628
Transition system for beverage machine ts1.4-2

pay

select

coke sprite

state space S = {pay , select, coke, sprite}

set of initial states: S0 = {pay }

19 / 628
Transition system for beverage machine ts1.4-2

pay
get coke get sprite actions:
coin coin
τ
select
τ τ get sprite
sprite get coke
coke
state space S = {pay , select, coke, sprite}
set of initial states: S0 = {pay }

20 / 628
Transition system for beverage machine ts1.4-2

pay
get coke get sprite actions:
coin coin
τ
select
τ τ get sprite
sprite get coke
coke
state space S = {pay , select, coke, sprite}
set of initial states: S0 = {pay }
set of atomic propositions: AP = {pay , drink}
labeling function: L(coke) = L(sprite) = {drink}
L(pay ) = {pay }}, L(select) = ∅
21 / 628
Transition system for beverage machine ts1.4-2

pay
get coke get sprite actions:
coin coin
τ
select
τ τ get sprite
sprite get coke
coke
state space S = {pay , select, coke, sprite}
set of initial states: S0 = {pay }
set of atomic propositions: AP = S
labeling function: L(s) = {s} for each state s

22 / 628
“Behaviour” of transition systems ts1.4-3

possible behaviours of a TS result from:

select nondeterministically an initial state s ∈ S0
WHILE s is non-terminal DO
α
select nondeterministically a transition s −→ s ′
execute the action α and put s := s ′
OD

23 / 628
“Behaviour” of transition systems ts1.4-3

possible behaviours of a TS result from:

select nondeterministically an initial state s ∈ S0
WHILE s is non-terminal DO
α
select nondeterministically a transition s −→ s ′
execute the action α and put s := s ′
OD
executions: maximal “transition sequences”
α1 α2 α3
s0 −→ s1 −→ s2 −→ . . . with s0 ∈ S0

24 / 628
“Behaviour” of transition systems ts1.4-3

possible behaviours of a TS result from:

select nondeterministically an initial state s ∈ S0
WHILE s is non-terminal DO
α
select nondeterministically a transition s −→ s ′
execute the action α and put s := s ′
OD
executions: maximal “transition sequences”
α1 α2 α3
s0 −→ s1 −→ s2 −→ . . . with s0 ∈ S0
reachable fragment:
Reach(T ) = set of all states that are reachable from
an initial state through some execution
25 / 628
Possible meanings of nondeterminism in TS ts1.4-3a

26 / 628
Possible meanings of nondeterminism in TS ts1.4-3a

• (true) concurrency modeled by interleaving

• competition of parallel dependent actions
• implementational freedom, underspecification
• incomplete information on system environment

27 / 628
Transition system for parallel actions ts1.4-4

parallel execution of independent actions

parallel execution of dependent actions

28 / 628
Transition system for parallel actions ts1.4-4

parallel execution of independent actions

e.g. x| :={zx+1} ||| y := y −3 α , β independent
| {z }
action α action β

parallel execution of dependent actions

29 / 628
Transition system for parallel actions ts1.4-4

parallel execution of independent actions

e.g. x| :={zx+1} ||| y := y −3 α , β independent
| {z }
action α action β

parallel execution of dependent actions

e.g. x| :={zx+1} ||| y := 2∗x α , β dependent
| {z }
action α action β

30 / 628
Transition system for parallel actions ts1.4-4

parallel execution of independent actions ← interleaving

e.g. x| :={zx+1} ||| y := y −3 α , β independent
| {z }
action α action β

parallel execution of dependent actions ← competition

e.g. x| :={zx+1} ||| y := 2∗x α , β dependent
| {z }
action α action β

31 / 628
parallel execution of independent actions ← interleaving
x =0
α y =5 β
x =1 x = 0 x := x+1 ||| y := y −3
y =5 y = 2 | {z } | {z }
β x =1 α action α action β
y =2

32 / 628
parallel execution of independent actions ← interleaving
x =0
α y =5 β
x =1 x = 0 x := x+1 ||| y := y −3
y =5 y = 2 | {z } | {z }
β x =1 α action α action β
y =2
parallel execution of dependent actions ← competition

33 / 628
parallel execution of independent actions ← interleaving
x =0
α y =5 β
x =1 x = 0 x := x+1 ||| y := y −3
y =5 y = 2 | {z } | {z }
β x =1 α action α action β
y =2
parallel execution of dependent actions ← competition
x =0
α y =0 β
x =1 x =0 x| :={zx+1} ||| y := 2∗x
y =0 y =0 | {z }
action α action β
β α
x =1 x =1
y =2 y =0
34 / 628
Possible meanings of nondeterminism in TS ts1.4-4a

• (true) concurrency modeled by interleaving

• competition of parallel dependent actions
• implementational freedom, underspecification
• incomplete information on system environment

35 / 628
Implementation freedom ts1.4-5

... modelled by nondeterminism

36 / 628
Implementation freedom ts1.4-5

fax
unknown
sender receiver
email

37 / 628
Implementation freedom ts1.4-5

fax
unknown
sender receiver
email
realization by a TS:

generate message
... ...

send fax send email

38 / 628
Implementation freedom ts1.4-5

fax
unknown
sender receiver
email
realization by a TS:

generate message
... ...

send fax send email

at a future refinement step the nondeterminism

is replaced with one of the alternatives
39 / 628
Implementation freedom ts1.4-5

fax
known without
sender HH   receiver email access

email
H
 HH

realization by a TS:

generate message
... ...

send fax send email

at a future refinement step the nondeterminism

is replaced with one of the alternatives
40 / 628
Implementation freedom ts1.4-5

fax
known without
sender HH   receiver email access

email
H
 HH

realization by a TS: refined TS:

generate message generate message

... ... ...

send fax send email send fax

at a future refinement step the nondeterminism

is replaced with one of the alternatives
41 / 628
Underspecification ts1.4-6

42 / 628
Underspecification ts1.4-6

produce message

try to send

lost delivered

43 / 628
Underspecification ts1.4-6

produce message

try to send

lost 10−8 delivered

1 − 10−8

at a future refinement step the nondeterminism

is replaced with probabilism

44 / 628
Possible meanings of nondeterminism in TS ts1.4-6a

• (true) concurrency modeled by interleaving

• competition of parallel dependent actions
• implementational freedom, underspecification
• incomplete information on system environment

45 / 628
Possible meanings of nondeterminism in TS ts1.4-6a

• (true) concurrency modeled by interleaving

• competition of parallel dependent actions
• implementational freedom, underspecification
• incomplete information on system environment, e.g.,
interfaces with other programs, human users, sensors

46 / 628
Incomplete information on the environment ts1.4-7

off

on

0 1 ... 9 menu

... ... ... ...

mobile phone

47 / 628
Incomplete information on the environment ts1.4-7

off

on

0 1 ... 9 menu

... ... ... ...

mobile phone

resolution of the nondeterministic choices

by a human user

48 / 628
Possible meanings of nondeterminism in TS ts1.4-8

concurrency (interleaving) α β
α ||| β is represented by
β α
competitions x=0

to be resolved by a scheduler x=1 x=0

e.g. x:=x+1 k x:=3x
x=3 x=1
underspecification, implementational freedom
incomplete information on system environment, e.g.,
interfaces with other programs, human users, sensors
49 / 628
Overview overview2.2

Introduction
Modelling parallel systems
Transition systems
Modeling hard- and software systems ←−
Parallelism and communication
Linear Time Properties
Regular Properties
Linear Temporal Logic
Computation-Tree Logic
Equivalences and Abstraction

50 / 628
Model checking ts1.4-9

system P1k. . .kPn requirements

transition
specification spec
system T

model checker
does T satisfy spec ?

yes no + error indication

51 / 628
Model checking ts1.4-9

system P1k. . .kPn requirements

specification spec

transition
system T

model checker
does T satisfy spec ?

yes no + error indication

52 / 628
Model checking ts1.4-9

syntactic description requirements

of P1 k. . .kPn
specification spec
semantics

transition
system T

model checker
does T satisfy spec ?

yes no + error indication

53 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym
input bits circuit output bits

register r1, . . . , rk

54 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

55 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

b switching functions {0, 1}n × {0, 1}k −→ {0, 1}

δj , λi =

56 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

b switching functions {0, 1}n × {0, 1}k −→ {0, 1}

δj , λi =
input values a1 , . . . , an output value λi (. . .)
for the input variables for output variable yi
7→
+ current values c1 , . . . , ck next value δj (. . .)
of the registers for register rj

57 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

initial register evaluation [r1=c01, . . ., rk =c0k ]

58 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

initial register evaluation [r1=c01, . . ., rk =c0k ]

transition system:
• states: evaluations of x1, . . . , xn , r1, . . . , rk

59 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

initial register evaluation [r1=c01, . . ., rk =c0k ]

transition system:
• states: evaluations of x1, . . . , xn , r1, . . . , rk
• transitions represent the stepwise behavior

60 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

initial register evaluation [r1=c01, . . ., rk =c0k ]

transition system:
• states: evaluations of x1, . . . , xn , r1, . . . , rk
• transitions represent the stepwise behavior
• values of input bits change nondeterministically

61 / 628
Modelling of sequential circuits by TS ts1.4-10

x1 , . . . , xn y1 , . . . , ym output
input bits circuit functions
λ1 , . . . , λm
transition
functions
δ1 , . . . , δk
register r1, . . . , rk

initial register evaluation [r1=c01, . . ., rk =c0k ]

transition system:
• states: evaluations of x1, . . . , xn , r1, . . . , rk
• transitions represent the stepwise behavior
• values of input bits change nondeterministically
• atomic propositions: x1, . . . , xn , y1, . . . , ym , r1, . . . , rk
62 / 628
Example: sequential circuit ts1.4-11a

63 / 628
Example: sequential circuit ts1.4-11a

output function: λy = ¬(x ⊕ r )

transition function: δr = x ∨ r

64 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r

65 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system

66 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system

x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

67 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system

x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

initial register evaluation: r =0

68 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system

x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

initial register evaluation: r =0

69 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system

x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

initial register evaluation: r =0

70 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system

x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

initial register evaluation: r =0

71 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system
{y }
x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

initial register evaluation: r =0

72 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system
{y } {x}
x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1

initial register evaluation: r =0

73 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system
{y } {x}
x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1
{r }
initial register evaluation: r =0
74 / 628
Example: TS for sequential circuit ts1.4-11

output function
λy = ¬(x ⊕ r )
transition function
δr = x ∨ r
transition system
{y } {x}
x=0 r =0 x=1 r =0

x=0 r =1 x=1 r =1
{r } {x, r , y }
initial register evaluation: r =0
75 / 628
How many states . . . ts1.4-12

. . . has the transition system for a circuit of the form?

1000 gates y
1 output bit
r1, . . . , r100 no input
100 registers

76 / 628
How many states . . . ts1.4-12

. . . has the transition system for a circuit of the form?

1000 gates y
1 output bit
r1, . . . , r100 no input
100 registers
answer: 2100

77 / 628
How many states . . . ts1.4-12

. . . has the transition system for a circuit of the form?

1000 gates y
1 output bit
r1, . . . , r100 no input
100 registers
answer: 2100
x ...
no output
1 input bit
r1 , . . . , r100 100 registers

78 / 628
How many states . . . ts1.4-12

. . . has the transition system for a circuit of the form?

1000 gates y
1 output bit
r1, . . . , r100 no input
100 registers
answer: 2100
x ...
no output
1 input bit
r1 , . . . , r100 100 registers
answer: 2100 ∗ 21 = 2101
79 / 628
Data-dependent systems ts1.4-13

problem: TS-representation of conditional branchings ?

if x > 0 if x ≤ 0
... ...

80 / 628
Data-dependent systems ts1.4-13

problem: TS-representation of conditional branchings ?

if x > 0 if x ≤ 0
... ...
example: sequential program
WHILE x > 0 DO
x := x−1
x−1;
y := y +1
OD
...

81 / 628
Data-dependent systems ts1.4-13

problem: TS-representation of conditional branchings ?

if x > 0 if x ≤ 0
... ...
example: sequential program
if x ≤ 0
WHILE x > 0 DO y :=y +1 ℓ1
x := x−1
x−1; ℓ3
y := y +1
OD ℓ2 if x > 0 then
... x := x−1

82 / 628
Data-dependent systems ts1.4-13

problem: TS-representation of conditional branchings ?

if x > 0 if x ≤ 0
... ... program graph
example: sequential program ↓
if x ≤ 0
WHILE x > 0 DO y :=y +1 ℓ1
x := x−1
x−1; ℓ3
y := y +1
OD ℓ2 if x > 0 then
... x := x−1

83 / 628
Data-dependent systems ts1.4-13

problem: TS-representation of conditional branchings ?

if x > 0 if x ≤ 0
... ... program graph
example: sequential program ↓
if x ≤ 0
ℓ1 → WHILE x > 0 DO y :=y +1 ℓ1
x := x−1
x−1; ℓ3
ℓ2 → y := y +1
OD ℓ2 if x > 0 then
ℓ3 → . . . x := x−1
ℓ1 , ℓ2, ℓ3 are locations,
i.e., control states
84 / 628
Data-dependent systems ts1.4-13

problem: TS-representation of conditional branchings ?

if x > 0 if x ≤ 0
... ... program graph
example: sequential program ↓
if x ≤ 0
ℓ1 → WHILE x > 0 DO y :=y +1 ℓ1
x := x−1
x−1; ℓ3
ℓ2 → y := y +1
OD ℓ2 if x > 0 then
ℓ3 → . . . x := x−1
states of the transition system:
locations + relevant data (here: values for x and y )
85 / 628
Example: TS for sequential program ts1.4-14

initially: x = 22, y = 0
ℓ1→ WHILE x > 0 DO
x := x−1
ℓ2→ y := y +1
OD
ℓ3→ . . .
program graph
y :=y +1 if x ≤ 0
ℓ1

ℓ3
ℓ2 if x > 0 then
x := x−1
86 / 628
Example: TS for sequential program ts1.4-14

initially: x = 22, y = 0 ℓ1 x = 2 y = 0
ℓ1→ WHILE x > 0 DO
x := x−1 ℓ2 x = 1 y = 0
ℓ2→ y := y +1
OD
ℓ3→ . . . ℓ1 x = 1 y = 1

program graph
ℓ2 x = 0 y = 1
y :=y +1 if x ≤ 0
ℓ1
ℓ1 x = 0 y = 2
ℓ3
ℓ2 if x > 0 then
x := x−1 ℓ3 x = 0 y = 2
87 / 628
Example: TS for sequential program ts1.4-14

initially: x = 22, y = 0 ℓ1 x = 2 y = 0
ℓ1→ WHILE x > 0 DO α
x := x−1 ← action α ℓ2 x = 1 y = 0
ℓ2→ y := y +1 ← action β β
OD
ℓ3→ . . . ℓ1 x = 1 y = 1
α
program graph
ℓ2 x = 0 y = 1
ℓ1 if x ≤ 0 then β
β loop exit
ℓ1 x = 0 y = 2
ℓ2 ℓ3 loop exit
if x > 0
then α ℓ3 x = 0 y = 2
88 / 628
Typed variables Transsys/pc2.2-typed-variables

typed variable: variable x + data domain Dom(x)

89 / 628
Typed variables Transsys/pc2.2-typed-variables

typed variable: variable x + data domain Dom(x)

• Boolean variable: variable x with Dom(x) = {0, 1}
• integer variable: variable y with Dom(y ) = N
• variable z with Dom(z) = {yellow, red, blue}

90 / 628
Typed variables Transsys/pc2.2-typed-variables

typed variable: variable x + data domain Dom(x)

• Boolean variable: variable x with Dom(x) = {0, 1}
• integer variable: variable y with Dom(y ) = N
• variable z with Dom(z) = {yellow, red, blue}

evaluation for a set Var of typed variables:

type-consistent function η : Var → Values

91 / 628
Typed variables Transsys/pc2.2-typed-variables

typed variable: variable x + data domain Dom(x)

• Boolean variable: variable x with Dom(x) = {0, 1}
• integer variable: variable y with Dom(y ) = N
• variable z with Dom(z) = {yellow, red, blue}

evaluation for a set Var of typed variables:

type-consistent function η : Var → Values
↑ ↑ S
η(x) ∈ Dom(x) Values = Dom(x)
x∈Var
for all x ∈ Var

92 / 628
Typed variables Transsys/pc2.2-typed-variables

typed variable: variable x + data domain Dom(x)

• Boolean variable: variable x with Dom(x) = {0, 1}
• integer variable: variable y with Dom(y ) = N
• variable z with Dom(z) = {yellow, red, blue}

evaluation for a set Var of typed variables:

type-consistent function η : Var → Values
↑ ↑ S
η(x) ∈ Dom(x) Values = Dom(x)
x∈Var
for all x ∈ Var

Notation: Eval(Var ) = set of evaluations for Var

93 / 628
Conditions on typed variables pc2.2-typed-cond

If Var is a set of typed variables then

Cond(Var)) = set of Boolean conditions
Cond(Var
on the variables in Var

94 / 628
Conditions on typed variables pc2.2-typed-cond

If Var is a set of typed variables then

Cond(Var)) = set of Boolean conditions
Cond(Var
on the variables in Var


Example: ¬x ∧ y <z+3 ∨ w =red
1}, Dom(y ) = Dom(z) = N
where Dom(x) = {0, 1} N,
Dom(w ) = {yellow, red, blue}

95 / 628
Conditions on typed variables pc2.2-typed-cond

If Var is a set of typed variables then

Cond(Var)) = set of Boolean conditions
Cond(Var
on the variables in Var


Example: ¬x ∧ y <z+3 ∨ w =red
1}, Dom(y ) = Dom(z) = N
where Dom(x) = {0, 1} N,
Dom(w ) = {yellow, red, blue}

|= for evaluations and conditions

satisfaction relation |=

96 / 628
Conditions on typed variables pc2.2-typed-cond

If Var is a set of typed variables then

Cond(Var)) = set of Boolean conditions
Cond(Var
on the variables in Var


Example: ¬x ∧ y <z+3 ∨ w =red
1}, Dom(y ) = Dom(z) = N
where Dom(x) = {0, 1} N,
Dom(w ) = {yellow, red, blue}

|= for evaluations and conditions

satisfaction relation |=
Example:
[ x=0, y =3, z=6 ] |= ¬x ∧ y <z
[ x=0, y =3, z=6 ] |6 = x ∨ y =z
97 / 628
Effect-function for actions pc2.2-typed-effect

Given a set Act of actions that operate on the variables

in Var , the effect of the actions is formalized by:

98 / 628
Effect-function for actions pc2.2-typed-effect

Given a set Act of actions that operate on the variables

in Var , the effect of the actions is formalized by:
Effect : Act×Eval (Var) → Eval (Var)

99 / 628
Effect-function for actions pc2.2-typed-effect

Given a set Act of actions that operate on the variables

in Var , the effect of the actions is formalized by:
Effect : Act×Eval (Var) → Eval (Var)

x:=2x+y ” then:
if α is “x:=2x+y
Effect(α, [x=1, yy=3,
=3, . . . ]) = [x=5, yy=3,
=3, . . . ]

100 / 628
Effect-function for actions pc2.2-typed-effect

Given a set Act of actions that operate on the variables

in Var , the effect of the actions is formalized by:
Effect : Act×Eval (Var) → Eval (Var)

x:=2x+y ” then:
if α is “x:=2x+y
Effect(α, [x=1, yy=3,
=3, . . . ]) = [x=5, yy=3,
=3, . . . ]
x:=2x+y ; y :=1−x
if β is “x:=2x+y :=1−x” then:
Effect(β, [x=1, y =3, . . . ]) = [x=5, y =−4, . . . ]

101 / 628
Effect-function for actions pc2.2-typed-effect

Given a set Act of actions that operate on the variables

in Var , the effect of the actions is formalized by:
Effect : Act×Eval (Var) → Eval (Var)

x:=2x+y ” then:
if α is “x:=2x+y
Effect(α, [x=1, yy=3,
=3, . . . ]) = [x=5, yy=3,
=3, . . . ]
x:=2x+y ; y :=1−x
if β is “x:=2x+y :=1−x” then:
Effect(β, [x=1, y =3, . . . ]) = [x=5, y =−4, . . . ]
(x, yy)) := (2x+y , 1−x)
if γ is “(x, 1−x)” then:
Effect(γ, [x=1, yy=3,
=3, . . . ]) = [x=5, yy=0,
=0, . . . ]
102 / 628
Program graph (PG) Transsys/ts-program-graph-def-1

103 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where

104 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,

105 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,

106 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)

107 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)
↑
function that formalizes the effect of the actions

108 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)
↑
function that formalizes the effect of the actions
example: if α is the assignment x:=x+y then
Effect(α, [x=1, y =7]) = [x=8, yy=7]
=7]
109 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)
• ֒→ ⊆ Loc × Cond(Var) × Act × Loc

110 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)
• ֒→ ⊆ Loc × Cond(Var) × Act × Loc
g :α
specifies conditional transitions of the form ℓ ֒→ ℓ′

ℓ , ℓ′ are locations, g ∈ Cond(Var

Cond(Var)) α ∈ Act
Cond(Var),
111 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)
• ֒→ ⊆ Loc × Cond(Var) × Act × Loc
g :α
specifies conditional transitions of the form ℓ ֒→ ℓ′
• Loc0 ⊆ Loc is the set of initial locations,

112 / 628
Program graph (PG) Transsys/ts-program-graph-def

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var) → Eval (Var)
• ֒→ ⊆ Loc × Cond(Var) × Act × Loc
g :α
specifies conditional transitions of the form ℓ ֒→ ℓ′
• Loc0 ⊆ Loc is the set of initial locations,
Cond(Var)) initial condition on the variables
• g0 ∈ Cond(Var
113 / 628
Program graph (PG) ts-program-graph-def-ohne-overlay

Let Var be a set of typed variables.

A program graph over Var is a tuple
P = (Loc, Act, Effect, ֒→, Loc0, g0) where
• Loc is a (finite) set of locations, i.e., control states,
• Act a set of actions,
• Effect : Act × Eval (Var ) → Eval (Var )
• ֒→ ⊆ Loc × Cond(Var)
Cond(Var ) × Act × Loc
g :α
specifies conditional transitions of the form ℓ ֒→ ℓ′
• Loc0 ⊆ Loc is the set of initial locations,
• g0 ∈ Cond(Var) initial condition on the variables.
114 / 628
TS-semantics of a program graph ts-PG-sem

115 / 628
TS-semantics of a program graph ts-PG-sem

program graph P over Var

⇓
transition system TP

116 / 628
TS-semantics of a program graph ts-PG-sem

program graph P over Var

⇓
transition system TP

states in TP have the form

hℓ, ηi
ր տ
location variable evaluation

117 / 628
TS-semantics of a program graph ts-program-graph-sem

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

The transition system of P is:
TP = (S, Act, −→, S0, AP, L)

118 / 628
TS-semantics of a program graph ts-program-graph-sem

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

The transition system of P is:
TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

119 / 628
TS-semantics of a program graph ts-program-graph-sem

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

The transition system of P is:
TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

• initial states: S0 = hℓ, ηi : ℓ ∈ Loc0 , η |= g0

120 / 628
TS-semantics of a program graph ts-program-graph-sem

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

The transition system of P is:
TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

• initial states: S0 = hℓ, ηi : ℓ ∈ Loc0 , η |= g0
The transition relation −→ is given by the following rule:
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(α, η)i

121 / 628
Structured operational semantics (SOS) ts-PG-SOS

The transition system of a program graph P is

TP = (S, Act, −→, S0, AP, L) where
the transition relation −→ is given by the following rule
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(α, η)i

is a shortform notation in SOS-style.

premise
conclusion

122 / 628
Structured operational semantics (SOS) ts-PG-SOS

The transition system of a program graph P is

TP = (S, Act, −→, S0, AP, L) where
the transition relation −→ is given by the following rule
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(α, η)i

is a shortform notation in SOS-style.

It means that −→ is the smallest relation such that:
g :α α
if ℓ ֒→ ℓ′ ∧ η |= g then hℓ, ηi −→ hℓ′, Effect(α, η)i
123 / 628
TS-semantics of a program graph ts-PG-lab

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

transition system TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

• initial states: S0 = hℓ, ηi : ℓ ∈ Loc0 , η |= g0
• −→ is given by the following rule:
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(α, η)i

124 / 628
Labeling of the states ts-PG-lab

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

transition system TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

• initial states: S0 = hℓ, ηi : ℓ ∈ Loc0 , η |= g0
• −→ is given by the following rule:
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(α, η)i
• atomic propositions: AP = Loc ∪ Cond(Var)
Cond(Var )

125 / 628
Labeling of the states ts-PG-lab

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

transition system TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

• initial states: S0 = hℓ, ηi : ℓ ∈ Loc0 , η |= g0
• −→ is given by the following rule:
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(α, η)i
• atomic propositions: AP = Loc ∪ Cond(Var)
Cond(Var )
• labeling function:

Cond(Var ) : η |= g
L(hℓ, ηi) = {ℓ} ∪ g ∈ Cond(Var)
126 / 628
TS-semantics of a program graph ts-program-graph-sem-ohne-overlay

Let P = (Loc, Act, Effect, ֒→, Loc0, g0) be a PG.

transition system TP = (S, Act, −→, S0, AP, L)
• state space: S = Loc × Eval (Var)

• initial states: S0 = hℓ, ηi : ℓ ∈ Loc0 , η |= g0
• −→ is given by the following rule:
g :α
ℓ ֒→ ℓ′ ∧ η |= g
α
hℓ, ηi −→ hℓ′ , Effect(η, α)i
• atomic propositions: AP = Loc ∪ Cond(Var)
Cond(Var )
• labeling function:

Cond(Var ) : η |= g
L(hℓ, ηi) = {ℓ} ∪ g ∈ Cond(Var)
127 / 628
Guarded Command Language (GCL) ts1.4-15

by Dijkstra

128 / 628
Guarded Command Language (GCL) ts1.4-15

by Dijkstra

• high-level modeling language that contains features

of imperative languages and nondeterministic choice

129 / 628
Guarded Command Language (GCL) ts1.4-15

by Dijkstra

• high-level modeling language that contains features

of imperative languages and nondeterministic choice
• semantics:
GCL-program
↓
program graph
↓
transition system

130 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt

g : guard, i.e., Boolean condition

on the program variables
stmt : statement

131 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt ← enabled if g is true

g : guard, i.e., Boolean condition

on the program variables
stmt : statement

132 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt ← enabled if g is true

g : guard, i.e., Boolean condition

on the program variables
stmt : statement

repetitive command/loop:
DO :: g ⇒ stmt OD

133 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt ← enabled if g is true

g : guard, i.e., Boolean condition

on the program variables
stmt : statement

repetitive command/loop:
DO :: g ⇒ stmt OD ← WHILE g DO stmt OD

134 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt ← enabled if g is true

g : guard, i.e., Boolean condition

on the program variables
stmt : statement

repetitive command/loop:
DO :: g ⇒ stmt OD ← WHILE g DO stmt OD
conditional command:
IF :: g ⇒ stmt1
:: ¬g ⇒ stmt2
FI
135 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt ← enabled if g is true

g : guard, i.e., Boolean condition

on the program variables
stmt : statement

repetitive command/loop:
DO :: g ⇒ stmt OD ← WHILE g DO stmt OD
conditional command:
IF :: g ⇒ stmt1 IF g THEN stmt1
:: ¬g ⇒ stmt2 ← ELSE stmt2
FI FI
136 / 628
Guarded Command Language (GCL) ts1.4-15

guarded command g ⇒ stmt ← enabled if g is true

repetitive command/loop:
DO :: g ⇒ stmt OD ← WHILE g DO stmt OD
conditional command:
IF :: g ⇒ stmt1 IF g THEN stmt1
:: ¬g ⇒ stmt2 ← ELSE stmt2
FI FI

symbol :: stands for the nondeterministic choice

between enabled guarded commands

137 / 628
Guarded Command Language (GCL) ts1.4-16

modeling language with nondeterministic choice

def  
stmt = x := expr  stmt1; stmt2 
::g1 ⇒ stmt1 . . . ::
DO :: ::gn ⇒ stmtn OD
::g1 ⇒ stmt1 . . . ::
IF :: ::gn ⇒ stmtn FI
..
.

where x is a typed variable and expr an expression of

the same type

138 / 628
Guarded Command Language (GCL) ts1.4-16

modeling language with nondeterministic choice

def  
stmt = x := expr  stmt1; stmt2 
::g1 ⇒ stmt1 . . . ::
DO :: ::gn ⇒ stmtn OD
::g1 ⇒ stmt1 . . . ::
IF :: ::gn ⇒ stmtn FI
..
.

where x is a typed variable and expr an expression of

the same type

semantics of a GCL-program: program graph

139 / 628
GCL-program for beverage machine pc2.1-GCL-getraenkeautomat

140 / 628
GCL-program for beverage machine pc2.1-GCL-getraenkeautomat

uses two variables #sprite, #coke ∈ {0, 1, . . . , max}

for the number of available drinks (sprite or coke)

141 / 628
GCL-program for beverage machine pc2.1-GCL-getraenkeautomat

uses two variables #sprite, #coke ∈ {0, 1, . . . , max}

for the number of available drinks (sprite or coke)
uses the following actions:
enabled effect
get coke if #coke > 0 #coke := #coke −1
get sprite if #sprite > 0 #sprite := #sprite−1

142 / 628
GCL-program for beverage machine pc2.1-GCL-getraenkeautomat

uses two variables #sprite, #coke ∈ {0, 1, . . . , max}

for the number of available drinks (sprite or coke)
uses the following actions:
enabled effect
get coke if #coke > 0 #coke := #coke −1
get sprite if #sprite > 0 #sprite := #sprite−1
#sprite := max
refill any time
#coke := max

143 / 628
GCL-program for beverage machine pc2.1-GCL-getraenkeautomat

uses two variables #sprite, #coke ∈ {0, 1, . . . , max}

for the number of available drinks (sprite or coke)
uses the following actions:
enabled effect
get coke if #coke > 0 #coke := #coke −1
get sprite if #sprite > 0 #sprite := #sprite−1
#sprite := max
refill any time
#coke := max
insert coin any time no effect on variables

144 / 628
GCL-program for beverage machine pc2.1-GCL-getraenkeautomat

uses two variables #sprite, #coke ∈ {0, 1, . . . , max}

for the number of available drinks (sprite or coke)
uses the following actions:
enabled effect
get coke if #coke > 0 #coke := #coke −1
get sprite if #sprite > 0 #sprite := #sprite−1
#sprite := max
refill any time
#coke := max
insert coin any time no effect on variables
if machine is empty and user has
return coin
entered a coin (no effect on variables)
145 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin;

IF :: #sprite = #coke = 0 ⇒ return coin

:: #coke > 0 ⇒ #coke := #coke − 1

:: #sprite > 0 ⇒ #sprite := #sprite−1

FI
:: true ⇒ #sprite := max; #coke := max

OD

146 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin; (* user inserts a coin *)

IF :: #sprite = #coke = 0 ⇒ return coin

:: #coke > 0 ⇒ #coke := #coke − 1

:: #sprite > 0 ⇒ #sprite := #sprite−1

FI
:: true ⇒ #sprite := max; #coke := max

OD

147 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin; (* user inserts a coin *)

IF :: #sprite = #coke = 0 ⇒ return coin
(* no beverage available *)
:: #coke > 0 ⇒ #coke := #coke − 1

:: #sprite > 0 ⇒ #sprite := #sprite−1

FI
:: true ⇒ #sprite := max; #coke := max

OD

148 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin; (* user inserts a coin *)

IF :: #sprite = #coke = 0 ⇒ return coin
(* no beverage available *)
:: #coke > 0 ⇒ #coke := #coke − 1
(* user selects coke *)
:: #sprite > 0 ⇒ #sprite := #sprite−1
(* user selects sprite *)
FI
:: true ⇒ #sprite := max; #coke := max
(* refilling of the machine *)
OD

149 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin; (* user inserts a coin *)

IF :: #sprite = #coke = 0 ⇒ return coin
(* no beverage available *)
:: #coke > 0 ⇒ get coke
(* user selects coke *)
:: #sprite > 0 ⇒ get sprite
(* user selects sprite *)
FI
:: true ⇒ refill
(* refilling of the machine *)
OD

150 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin;

IF :: #sprite = #coke = 0 ⇒ return coin

:: #coke > 0 ⇒ get coke

:: #sprite > 0 ⇒ get sprite

FI
:: true ⇒ refill

OD

151 / 628
GCL-program for beverage machine pc2.1-GCL-2

DO :: true ⇒ insert coin;

IF :: #sprite = #coke = 0
⇒ return coin
:: #coke > 0 ⇒ get coke
:: #sprite > 0 ⇒ get sprite
FI
:: true ⇒ refill
OD
... yields a program graph with
• two variables #sprite, #coke ∈ {0, 1, . . . , max}

152 / 628
GCL-program for beverage machine pc2.1-GCL-2

start → DO :: true ⇒ insert coin;

select
select→→ IF :: #sprite = #coke = 0
⇒ return coin
:: #coke > 0 ⇒ get coke
:: #sprite > 0 ⇒ get sprite
FI
:: true ⇒ refill
OD
... yields a program graph with
• two variables #sprite, #coke ∈ {0, 1, . . . , max}
• two locations start and select
153 / 628
 refill start refill

refill insert coin

get coke get sprite
select

start start
insert coin insert get
coinsprite
selectget coke select
get coke startget sprite
start start
insert coin insert coin insert coin
select get sprite selectget sprite select

start get coke start get coke

insert coin insert coin
selectget sprite select
154 / 628