Embedded Systems Group (ES)

Checking Simulation and Bisimulation Relations of Kripke Structures

Using this tool, you can check for given Kripke structures whether one simulates the other, and whether both are bisimilar to each other. The syntax can be guessed by the given example (states are integers mentioned with the labels). Further examples taken from previous exams are also available.

The syntax for the state transition systems (the Kripke structures) should be obvious: states are integers 0,...,n as listed in the labels, and the labels are of the form i:x1,...,xm to denote that variables x1,...,xm hold in state i. Transitions are lists of the form i->j denoting a transition from state i to state j.

K1xK2
K1≤K2
K2≤K1
K1≈K2
K1≈K1
K2≈K2
print all simulation diagrams
K1
K2