Tim Willemse: On the minimisation of transition systems

Event Details

There is a wealth of equivalence relations on labelled transition systems; see, e.g., Van Glabbeek’s linear-time branching-time spectrum. Some of these equivalences have found their way in tool sets such as mCRL2, where they are used either to compare two transition systems, or to reduce the size of a transition system. The latter is often referred to as minimisation. Perhaps somewhat surprisingly there seems to be no general recipe for obtaining the minimal transition system for a given equivalence relation. In fact, not all equivalence relations have unique minimal representatives of a transition systems. To illustrate, I’ll explore the problem of minimisation for several well-known, and some lesser-known, equivalence relations.