Dec 17, 2013: Prof. Dr. Martin Lange: Model Checking Equivalence Relations

December 17, 2013Model Checking Equivalence Relations
Room: HalB 2BProf. Dr. Martin Lange

The polyadic mu-calculus is a variant of the modal mu-calculus whose formulas are
interpreted in tuples of states of a transition systems. The classic example of a polyadic
- in fact binary - formula is the one defining bisimilarity. In fact, the polyadic mu-calculus
can define practically all simulation-based process equivalences in the sense of fixed
formulas phi which are true on a pair (P,Q) of processes iff P and Q are equivalent according
to these notions.
In this talk I will present an extension of the polyadic mu-calculus with first-order functions
that is capable of expressing trace-based process equivalence notions which are usually
harder than simulation-based ones (PSPACE-hard vs. included in P). This lifts model checking
technology to equivalence checking: a generic model checker for this logic can be instantiated
with these fixed formulas and partially evaluated to yield algorithms for process equivalence
Other equivalences can be expressed in this logic as well; there are examples from the areas
of automata theory, circuit design, string problems, etc. The aim of this approach is to tackle
(hard) computation problems with the model checking toolkit in order to possibly arrive at
practical algorithms for these problems.
This is joint work with Etienne Lozes and Manuel Vargas Guzman.