PROCESMODELLEREN
S = states, A = actions, → =
transitions, Si = initial state, Ω = final
Labeled transition system, LTS:
states
Formal notation / formalization of LTSs
L = (S,A,→,Si, Ω)
S = {A,B,C,D,E,F,G}
A = {s,q,p,u,t}
→ = {(A,p,B),(A,s,C),(A,q,G),(B,u,D), etc.}
Si = A
Ω = {E}
Information about LTSs
- Allowed behaviour = what a lamp can and may do. For a lamp with states
on/off/broken, on-off-on-off is allowed behaviour, but on-on isn’t.
- Silent actions (notation: ==>) don’t have a label because they’re invisible from
the outside world.
- A subset of states (notation: ) is a livelock if from U only states within U
can be reached. A single state without any outgoing transitions is a deadlock.
- Graphs can have equivalent behaviour. Language equivalence can be a first
notion of this. Graphs can have different equivalence levels:
o Strong bisimulation: checks for isomorphism, which means that there is
a one-to-one correlation between the vertices (states/nodes) and arcs
(relations/edges) of graph A and the vertices and arcs of graph B. See
example below.
o Delay bisimulation: silent steps are allowed
o Weak bisimulation: silent steps on both sides of the graph-relation are
allowed
- Reflexive relation -> a state relates to itself (PS: a silent step is reflexive)
- Symmetric relation -> x relates to y and y also relates to x
- Transitive relation -> x can get to z via a long path, for example via y, but also
via a direct connection between x and z
When asked for the bijective function to prove isomorphism:
Also, all arcs of G can be mapped to the arcs of H.
F
All vertices in graph G can be mapped to the vertices in graph H
(f: VG → VH). The formula:
Conversely, all vertices in H can mapped to the vertices in G
, From text to LTS:
1. Consider what the possible states/places and objects are
2. Identify the initial state [DON’T FORGET THAT LITTLE ARROW!!!!]
3. Ask for each state: ‘what are the possible actions from this state?’ and ‘what
happens when I do this?’
4. Check if certain states and/or actions overlap. In that case, merge them.
5. Put circles on the final states, which are the states in which you’ll be happy if
the process ends there.
Eventually, you should meet all the requirements. Many different models are
possible. You can abstract away from certain things if there are not of big importance.
Below, you see a modeling example.
Example:
“The library has two members and the collection exists of two books. The members can
borrow these books and bring them back later (so those are the two possible actions). Model
this as LTS, assuming that the amount of books and members stays the same.”
- Initial state / Si: all books are still
in the library and nothing is
borrowed yet.
If you say that you have book ‘a’ and
book ‘b’ and that the two members
can borrow the books, you would get a model
looking like the one above. That’s too big, so you
have to abstract something away to make the
model smaller and better. You can do this by only
looking at the amount of books instead of the
individual books, which makes that you get the model on the right.
In this case, the individual books and not knowing who has borrowed what book is not a
big deal in this case, but when it is, you should go with the first model. In case that you
only have to know how many books the library has and how many are borrowed, you can
use an even more simplified model:
Which model you choose depends on what the purpose is / will be of your model. PS: also
define final states, also depending on what the purpose of your model is.
S = states, A = actions, → =
transitions, Si = initial state, Ω = final
Labeled transition system, LTS:
states
Formal notation / formalization of LTSs
L = (S,A,→,Si, Ω)
S = {A,B,C,D,E,F,G}
A = {s,q,p,u,t}
→ = {(A,p,B),(A,s,C),(A,q,G),(B,u,D), etc.}
Si = A
Ω = {E}
Information about LTSs
- Allowed behaviour = what a lamp can and may do. For a lamp with states
on/off/broken, on-off-on-off is allowed behaviour, but on-on isn’t.
- Silent actions (notation: ==>) don’t have a label because they’re invisible from
the outside world.
- A subset of states (notation: ) is a livelock if from U only states within U
can be reached. A single state without any outgoing transitions is a deadlock.
- Graphs can have equivalent behaviour. Language equivalence can be a first
notion of this. Graphs can have different equivalence levels:
o Strong bisimulation: checks for isomorphism, which means that there is
a one-to-one correlation between the vertices (states/nodes) and arcs
(relations/edges) of graph A and the vertices and arcs of graph B. See
example below.
o Delay bisimulation: silent steps are allowed
o Weak bisimulation: silent steps on both sides of the graph-relation are
allowed
- Reflexive relation -> a state relates to itself (PS: a silent step is reflexive)
- Symmetric relation -> x relates to y and y also relates to x
- Transitive relation -> x can get to z via a long path, for example via y, but also
via a direct connection between x and z
When asked for the bijective function to prove isomorphism:
Also, all arcs of G can be mapped to the arcs of H.
F
All vertices in graph G can be mapped to the vertices in graph H
(f: VG → VH). The formula:
Conversely, all vertices in H can mapped to the vertices in G
, From text to LTS:
1. Consider what the possible states/places and objects are
2. Identify the initial state [DON’T FORGET THAT LITTLE ARROW!!!!]
3. Ask for each state: ‘what are the possible actions from this state?’ and ‘what
happens when I do this?’
4. Check if certain states and/or actions overlap. In that case, merge them.
5. Put circles on the final states, which are the states in which you’ll be happy if
the process ends there.
Eventually, you should meet all the requirements. Many different models are
possible. You can abstract away from certain things if there are not of big importance.
Below, you see a modeling example.
Example:
“The library has two members and the collection exists of two books. The members can
borrow these books and bring them back later (so those are the two possible actions). Model
this as LTS, assuming that the amount of books and members stays the same.”
- Initial state / Si: all books are still
in the library and nothing is
borrowed yet.
If you say that you have book ‘a’ and
book ‘b’ and that the two members
can borrow the books, you would get a model
looking like the one above. That’s too big, so you
have to abstract something away to make the
model smaller and better. You can do this by only
looking at the amount of books instead of the
individual books, which makes that you get the model on the right.
In this case, the individual books and not knowing who has borrowed what book is not a
big deal in this case, but when it is, you should go with the first model. In case that you
only have to know how many books the library has and how many are borrowed, you can
use an even more simplified model:
Which model you choose depends on what the purpose is / will be of your model. PS: also
define final states, also depending on what the purpose of your model is.
