Mark Bouwman: Compositional state space generation

Event Details

In the FormaSig project we translate communicating SysML state machines to mCRL2. Selecting and executing a transition consists of several transitions in the mCRL2 model. These internal state machines can be considered unobservable and are renamed to tau. Since many of these internal transitions can be combined, the bisimulation quotient is orders of magnitude smaller than the original LTS. However, to be able to apply bisimulation reduction you first need to generate the entire LTS, which is often not feasible for our models. In this talk I will present a technique where we 1) compute the LTSs of individual state machines, 2) reduce these LTSs modulo bisimulation and 3) combine the LTSs into the LTS representing the behaviour of the parallel composition of all state machines.