Transcript From Labeled Transition Systems back to Equational Theory

Process Algebra (2IF45)
Introduction
From Labeled Transition Systems back to
Equational Theory
Dr. Suzana Andova
Reactive systems – general
• Computing systems which are supposed to offer some
(well-defined) services to their users
• These systems are large and usually consist of a number
of components which interact with each other
• Many of them are control crucial and/or safety critical
1
Process Algebra (2IF45)
Reactive systems - Correctness problem
• It is important that a realization of these systems is just
as intended
• Intended behaviour can be validated
• Solution: MODELING
• abstract model of the system
• unambiguous description
• methods and tools for model analysis
2
Process Algebra (2IF45)
Model of Labeled Transition Systems (LTS)
x:= 1;
y:= x+1;
out(y).
in(x);
y:= x+1;
while (true) {
out(y);
}.
?x
?x
!x
y:=x+1
?y
y:=x+1
!y
!y
3
out(x);
in(y).
Process Algebra (2IF45)
Model of Labeled Transition Systems (LTS)
Intermezzo
4
Process Algebra (2IF45)
Model of Labeled Transition Systems
VM2
VM1
VM3
?return
?coin
!coffee
?coin
?return
!tea
?coin
!coffee
!tea
!tea
!coffee
Using VM1
coin
User
!coin
?coffee
coffee
!coffee
5
?coin
error
!tea
Process Algebra (2IF45)
Model of Labeled transition systems
VM2’
VM1
VM3
?return
?return
?coin
!coffee
?coin
!tea
error
?coin
?coffee
?tea
!tea
!coffee
!coffee
!tea
User
!coin
6
!coffee
?coffee
Process Algebra (2IF45)
Observation
• LTSs consist of states and transitions labeled with (action) labels
• Initial state is indicated, final states are indicated
• LTSs can interact according to predefined communications
7
Process Algebra (2IF45)
Questions
• What is a state?
•How do we know drawing a transition from a state s to a state s’ is
right? How do we know which label to assign to it?
• How do we combine LTSs?
• When modeling a system, is an LTS a model to start with or is it
something to be obtained as a final or side product?
• What ingredient do we need to have predefined, to be able to produce
an LTS?
8
Process Algebra (2IF45)
Answers
• What is a state?
A state is an expression in a specification language (signature)
• How do we know whether drawing a transition from a state s to a state s’ is
right? How do we know which label to assign to it?
A transition and its label are determined by a set of rules, defining the behaviour
of any specification given in the language
• How do we combine LTSs?
Any composition (operation) on LTSs must be predefined in the language and
with the rules
9
Process Algebra (2IF45)
Answers
• When modeling a system, is an LTS a model to start with or is it
something to be obtained as a final or side product?
• What ingredient do we need to have predefined, to be able to produce
and work with LTSs?
10
Process Algebra (2IF45)
Answers
• When modeling a system, is an LTS a model to start with or is it
something to be obtained as a final or side product?
In (model checking) tools
manipulating
the state space (LTSs):
UPPAAL, Prism, MRMC
manipulating
the specification (language):
mCRL2, Chi, CADP, FDR, PEPA,
MRMC updated IMC
reduction
on specification
components’ specifications
…
reduction
on specification
the whole system specification
No!
reduction
on LTSs
verification
model checking
11
Yes!
the state space
composition by axiom
SS generation by the SOS rules
property specification
Process Algebra (2IF45)
Equational theory in place
In (model checking) tools
manipulating
the state space (LTSs):
UPPAAL, Prism, MRMC
manipulating
the specification (language):
mCRL2, Chi, CADP, FDR, PEPA,
MRMC updated IMC
reduction
on specification
components’ specifications
…
reduction
on specification
the whole system specification
No!
reduction
on LTSs
verification
model checking
12
Yes!
the state space
composition by axiom
SS generation by the SOS rules
property specification
Process Algebra (2IF45)
Equational theory in place
In (model checking) tools
manipulating
the state space (LTSs):
UPPAAL, Prism, MRMC
manipulating
the specification (language):
mCRL2, Chi, CADP, FDR, PEPA,
MRMC updated IMC
reduction
on specification
components’ specifications
consistent
…
reduction
on specification
the whole system specification
No!
reduction
on LTSs
verification
model checking
13
Yes!
the state space
composition by axiom
SS generation by the SOS rules
property specification
Process Algebra (2IF45)
Equational theory in place
In this course we will learn HOW to build a consistent
Process Algebra
= checking)
specification
In (model
tools language
+ axioms
manipulating
manipulating
+
SOS
rules
the state space (LTSs):
the specification (language):
+ reduction equivalence
relations
UPPAAL, Prism, MRMC
mCRL2, Chi, CADP,
FDR, PEPA,
MRMC
updated
IMC
so that the initial specification and the model checked
LTS,
they both
reduction
describe the same system!
on specification
components’ specifications
consistent
…
reduction
on specification
the whole system specification
No!
reduction
on LTSs
verification
model checking
14
Yes!
the state space
composition by axiom
SS generation by the SOS rules
property specification
Process Algebra (2IF45)
Labeled transition systems – basic notions
15
Process Algebra (2IF45)
Labeled transition systems – basic notions
VM1’
• Given a set of labels L
• An LTS consists of:
• S is a set of states
?coin
•  SxLxS
• S0 S is the initial state
•   S is the set of final states
nondeterministic
choice
successful
termination
16
Process Algebra (2IF45)
!coffee
!tea
deadlock
state
Labeled transition systems - choice
VM1’
VM1’’
?coin
nondetermini
stic choice
!coffee
Using VM1’
!tea
nondeterministic
choice
?coin
?coin
!coffee
!tea
Using VM1’’
coin
coin
coin
coffee
coffee
 or 

17
Process Algebra (2IF45)
Labeled transition systems - relations
VM1’
VM1’’
?coin
!coffee
!tea
?coin
!coffee
?coin
!tea
Similarities of the LTSs:
they both have the same traces, {?coin, ?coin !coffee, ?coin !tea}
Differences of the LTSs:
The moment a choice is made is different.
In VM1’ the choice is made before ?coin is executed.
In VM1’’ the choice is made after ?coin is executed.
18
Process Algebra (2IF45)
LTS Equivalence spectrum
Rob J. van Glabbeek “The Linear
Time-Branching Time Spectrum”,
CONCUR 1990
19
Process Algebra (2IF45)
Bisimulation on LTSs
Bisimilar LTSs
?coin
!coffee
!coffee
?coin
!coffee
Bisimulation relation: A binary relation R on the set of state S of an LTS is
bisimulation relation iff the following transfer conditions hold:
1. for all states s, t, s’  S, whenever (s, t)  R and s –a-> s’ for some a  L, then
there is a state t’  S such that t –a-> t’ and (s’, t’)  R;
2. vice versa, for all states s, t, s’  S, whenever (s, t)  R and t –a-> t’ for some a 
L, then there is a state s’  S such that s –a-> s’ and (s’, t’)  R;
3. whenever (s, t)  R and s  then t ;
4. whenever (s, t)  R and t  then s ;
Two LTSs s and t are bisimilar, s  t, iff there is a bisimulation relation R such that
(s, t)  R
20
Process Algebra (2IF45)
Bisimulation on LTSs
Bisimilar LTSs
?coin
Not bisimilar LTSs
?coin
?coin
?coin
?coin
??
!coffee
!coffee
!coffee
!coffee
!tea
!coffee
!tea
Bisimulation relation: A binary relation R on the set of state S of an LTS is
bisimulation relation iff the following transfer conditions hold:
1. for all states s, t, s’  S, whenever (s, t)  R and s –a-> s’ for some a  L, then
there is a state t’  S such that t –a-> t’ and (s’, t’)  R;
2. vice versa, for all states s, t, s’  S, whenever (s, t)  R and t –a-> t’ for some a 
L, then there is a state s’  S such that s –a-> s’ and (s’, t’)  R;
3. whenever (s, t)  R and s  then t ;
4. whenever (s, t)  R and t  then s ;
Two LTSs s and t are bisimilar, s  t, iff there is a bisimulation relation R such that
(s, t)  R
21
Process Algebra (2IF45)
Structural Operational Semantics –
general introduction
components’ specifications
the whole system specification
the state space
…
22
Process Algebra (2IF45)
Structural Operational Semantics –
general introduction
Ingredients
• A set of labels L
• Language  (signature/ syntax) : consists of symbols denoting
constants, operators, variables, functions, additional symbols
• All expressions (terms) in the language are build from the
symbols in the signature, denoted C()
• An expression corresponds to a state in a state space (LTS)
• Example: Language of Natural numbers
0
“zero”
s(_)
“successor function”
a(_, _)
“addition”
m(_, _)
“multiplication”
Terms in the language: s(s(0)), a(s(0),m(s(0),s(s(s(0))))), 0,
s(x) where x is a variable, …
23
Process Algebra (2IF45)
Structural Operational Semantics –
general introduction
Ingredients (cont.)
• Deduction (SOS) rules
• Rules are in the form


where
•  is a set of formulas called premises; it can be an empty set
•  is a formula called conclusion
• Formula is either a transition s –a-> t or a termination s for some
terms s and t in the language, s, t  C() and a label a  L
• Deduction rules determine transitions in a LTS
• A language and a set of rules defined over the language is
called deduction system
24
Process Algebra (2IF45)
Example: Deduction system for “Counting
down”
• Example: Language of Natural numbers
0
“zero”
s(_)
“successor function”
a(_, _)
“addition”
m(_, _)
“multiplication”
Question: How to define deduction rules that generate the following LTS
s(s(0))
1
s(0)
1
0
25
Process Algebra (2IF45)
Example: Deduction system for “Counting
down”
• Example: Language of Natural numbers
0
“zero”
s(_)
“successor function”
a(_, _)
“addition”
m(_, _)
“multiplication”
Question: How to define deduction rules that generate the following LTS
s(s(0))
1
s(0)
1
0
26
1
s(x) 
x
0 
1
y
y’

1
a(x,y)  a(x, y’)
x, y
a(x,y) 
Process Algebra (2IF45)

1
x
x’ , y
1
a(x,y) 
x’


Example: Deduction system for “Counting
down”
a( s(s(0)), s(s(s(0))) )
1

a( s(s(0)), s(s(0)) )
1

a( s(s(0)), s(0) )
1



0
1
s(x) 
x
1
y
y’

1
a(x,y)  a(x, y’)
x, y
a(x,y) 
27
Process Algebra (2IF45)

1
x
x’ , y
1
a(x,y) 
x’

1
1
0

a( s(s(0)), 0 )


s(0)
Example: Deduction system for “Counting
down” --- Alternative rules
Exercise: Write an alternative rules for the
Counting down deduction system!
28