What is the definition of a transition system?
A transition system is defined by a tuple
<S, A, ->, L, AP, I>
where
- S is the set of states
- A is a set of actions
- -> subset S x A x S is a set of transitions
- L: S -> 2^(AP) is a labelling function
- AP is a finite set of atomic propositions
- I subset S is the set of initial states
How is the labelling function defined?
2^AP means “the set of all subsets of AP”
for example AP = {ON, OFF}
2^AP = {Γ, {ON}, {OFF}, {ON, OFF}}
since |AP| = 2 then 2^AP = 2^2 = 4
What are Atomic Propositions?
Atomic propositions are statements that are evaluated as either true or false. In model checking, we evaluate such a statement as true if a state contains the atomic proposition and false if it does not contain it
What is the cartesian product of two sets?
All possible pairs of states from the two sets gathered in one set
What kind of compositions of two transition systems does there exist?
There two ways of composing transition systems. Either there is interleaving semantics or synchronous semantics.
What is the formal definition of forward and backwards reachability?
(the alpha at the arrow is above the arrow)
πππ π‘(π ) = {π ’ β£ βπΌ. π πΌβ π β²}
πππ(π ) = {π ’ β£ βπΌ. π β² πΌβ π }
What is non-determinism?
It may represent internal decisions of the system that are intentionally underspecified. Specifically, it is when there are multiple options of actions from a state using the same labelled action.
When is a transition system action-deterministic?
If there is no more than 1 initial state
|πΌ| β€ 1
For every state s and every action a, there is only one outgoing transition from s
labelled with a.
|{π β² β£ π πβ π β²}| β€ 1
Definition of a terminal state
A state is a terminal state if it has no outgoing transition.
Formally:
Β¬βπ β² . π β π β²
or
πππ π‘(π ) = β
What does Ο mean in the following context: (s0ββs1ββ)^Ο
Infinite amount of executions
What is a trace?
Replacing every state in an execution by its atomic properties
yields a trace.
π 0 β π 1 β π 0 β β―
ππ β ππΉπΉ β ππ β
What is a computation tree?
A computation tree is the unfolding of the transition system.
When interleaving two transition systems. How does that work?
We have the cartesian product of S1 and S2, along with I1 and I2 and the union of both transition systems actions and atomic propositions.
Interleaving means that if there previously was a transition between s1 and s1’, then there is still a transition of the composed states, (s1, s2) -> (s1’,s2)…
When synchronizing two transition systems. How does that work?
Here you have T1 |B| T2, where B is a set of actions. If there previously was a transition between s1 and s1’ labelled with an action a that is not in B, then we still have the transition of the composed states (s1, s2) -> (s1’, s2). But if the action a is in B, then we only create one transition for that action for both composed states: (s1, s2) -> (s1’, s2’).
How can state explosion occur in model checking?
If we have n transition systems with m states each and we interleave them all, how many states do we have?
m = 3 and we have n = 2. The cartesian product will give us n * m states. If we now make n = 3 we have 27, so it is actually m^n.
Synchonization may reduce the size composition, but the worst case is still exponential.
compose a transition system as follows:
T1: a1,b1
T2: a2, b2
Synchronous composition gives 4 states in total
add a transition system
T1: a1, b1
T2: a2, b2
T3: a3, b3
synchronous composition gives us 8 states in total
m^n states
