14:00-15:00 | 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 checking. 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. |