Fixpoint Logic, Games, and Relations of Consequence

Maciej Gazda

promotors: prof.dr.ir J.F. Groote (TU/e) and prof.dr. J.C. van de Pol (UT)
copromotor: dr.ir. T.A.C. Willemse (TU/e)
Technische Universiteit Eindhoven
Date: 15 March, 2016, 16:00
Thesis: PDF

Summary

Fixpoint logic is a powerful mathematical vehicle that allows one to express and subsequently verify virtually all interesting properties of software (models). Its expressive strength lies in the ability of defining both inductive and coinductive types of properties, as well as their combinations. Fixpoint logic comes in various guises, notably the modal mu-calculus and fixpoint equations systems.

In the first part, we explore the game-based view on fixpoint logic. When reasoning about the algorithmic aspects of the logic, specifically efficiency of deciding the satisfaction problem, it is often convenient to resort to the framework of parity games. They form a simple and intuitive alternative to working directly with the logic syntax, and have been an extensively studied research area in the last twenty years. The main contributions are:

  • we analyse one of the classical parity game solving algorithms, namely the Recursive algorithm. Even though its theoretical bounds on running time are not optimal, it has been known to be one of the best algorithms in practice. We study the algorithm’s behaviour on certain special classes of games, and show that when using the optimised version with SCC decomposition, all the classes are solved in polynomial time. We also provide a tighter bound on the global running time.
  • another classical algorithm is studied, namely the Small Progress Measures algorithm. We first provide a clearer, intuitive interpretation of progress measures, by using notions close to the strategy improvement algorithm family. Next, we propose a modification of the algorithm so that it can compute the strategies for both players in one pass, thus slightly improving the global running time on providing the full solution.
  • in recent years, several preorders on parity games have been suggested as useful tools for their analysis and providing more efficient algorithms. Every preorder in question has been defined in an ad-hoc way, and yet all of them seem to be a result of lifting a standard LTS/Kripke structure preorder to a two-player game setting. We propose a uniform way of lifting preorders on Kripke structures to parity games. In our framework, we are not only able to recover all the existing preorders, but also provide several new ones, notably the parity game variant of stuttering simulation.

In the second part of the thesis we look at another guise of fixpoint logic, namely fixpoint equation systems. They provide a very general framework that allows to express and solve a wide range of problems, notably model checking and equivalence of models. Their first-order variant, the so-called Parameterised Boolean Equation Systems, are of special practical importance as they enable us to use symbolic techniques in order to solve them. Here, our contributions are as follows:

  • we introduce and study a novel relation on Boolean equation systems, called consistent consequence. We show that it can be used as an approximation of the solution to an equation system. For the closed, simple and recursive fragment of equation systems we prove that it coincides with direct simulation for parity games. In addition, we show that deciding both consistent consequence and consistent correlations are coNP-complete problems.
  • using the notion of consistent consequence, we develop an abstraction framework for the first order variant of fixpoint equation systems. We study the capabilities of the abstraction theory by comparing it to the framework of generalised Kripke modal transition systems. We show that for model checking the modal mu-calculus, our abstractions can be exponentially more succinct than GTSs and our theory is as complete as the GTS framework for abstraction. Furthermore, we investigate the completeness of our theory irrespective of the encoded decision problem. We illustrate the potential of our theory through case studies using the first-order modal mu-calculus, and a real-time extension thereof, conducted using a prototype implementation of a new syntactic transformation for parameterised Boolean equation systems.