Tim Willemse: On quotients for equivalences on 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 quotienting.

Somewhat surprisingly, there does not appear to be a general recipe (yet) for obtaining a quotient for a given equivalence relation. To illustrate, I’ll explore the problem of quotienting for several well-known equivalence relations.