IAB201 Lecture Notes - Lecture 8: Transition System, Petri Net, Isomorphism
Document Summary
Behavioural equivalence of process models: given two transition systems, a natural question is whether they describe the same behaviour, this can mean many different things. For example, are we satisfied if both transition systems can perform the same sequence of actions: when can we consider two transition systems to be equivalent. Isomorphism: two isomorphic transition systems describe the same collection of traces (sequences of possible actions) If one transition system can perform action x then the other transition system must also be able to perform action x in such a way that the resulting states are again related. Intuition: two transition systems are bisimilar if and only if there is no winner in the bisimilarity game. Two bisimilar transition system preserve all moments of choice. Is a pair s = (n, m), where n is a petri net and m is the initial marking. Transition enablement rule: transitions may change a marking by firing (occurring, only enabled transitions may fire.
