Marcin Jurdzi{\'n}ski
``Games for Verification: Algorithmic Issues''

Abstract:

  This dissertation deals with a number of algorithmic problems
  motivated by computer aided formal verification of finite state
  systems.
  The goal of formal verification is to enhance the design and
  development of complex systems by providing methods and tools for
  specifying and verifying correctness of designs. 
  The success of formal methods in practice depends heavily on the
  degree of automation of development and verification process.
  This motivates development of efficient algorithms for problems
  underlying many verification tasks.
  
  Two paradigmatic algorithmic problems motivated by formal verification
  that are in the focus of this thesis are model checking and
  bisimilarity checking.   
  In the thesis game theoretic formulations of the problems are used to 
  abstract away from syntactic and semantic peculiarities of formal
  models and specification formalisms studied.
  This facilitates a detailed algorithmic analysis, leading to two novel 
  model checking algorithms with better theoretical or practical
  performance, and to an undecidability result for a notion of
  bisimilarity. 
  
  The original technical contributions of this thesis are collected in
  three research articles whose revised and extended versions are
  included in the dissertation.
  
  In the first two papers the computational complexity of deciding the
  winner in parity games is studied.
  The problem of solving parity games is polynomial time equivalent to
  the modal mu-calculus model checking.
  The modal mu-calculus plays a central role in the study of logics
  for specification and verification of programs.
  The model checking problem is extensively studied in literature on
  computer aided verification. 
  The question whether there is a polynomial time algorithm for the
  modal mu-calculus model checking is one of the most challenging and
  fascinating open questions in the area.
  
  In the first paper a new algorithm is developed for solving
  parity games, and hence for the modal mu-calculus model checking. 
  The design and analysis of the algorithm are based on a semantic
  notion of a progress measure. 
  The worst-case running time of the resulting algorithm matches the
  best worst-case running time bounds known so far for the problem,
  achieved by the algorithms due to Browne at al., and Seidl.
  Our algorithm has better space complexity:
  it works in small polynomial space;
  the other two algorithms have exponential worst-case space
  complexity. 
  
  In the second paper a novel approach to model checking is pursued,
  based on a link between parity games and discounted payoff and
  stochastic games, established and advocated by Puri.
  A discrete strategy improvement algorithm is given for solving parity
  games, thereby proving a new procedure for the modal mu-calculus
  model checking.  
  Known strategy improvement algorithms, as proposed for stochastic
  games by Hoffman and Karp, and for discounted payoff games and parity
  games by Puri, work with real numbers and require solving linear
  programming instances involving high precision arithmetic.
  The present algorithm for parity games avoids these difficulties by
  efficient manipulation of carefully designed discrete valuations. 
  A fast implementation is given for a strategy improvement step. 
  Another advantage of the approach is that it provides a better
  conceptual understanding of the underlying discrete structure and
  gives hope for easier analysis of strategy improvement algorithms for
  parity games. 
  However, so far it is not known whether the algorithm works in
  polynomial time.
  The long standing problem whether parity games can be solved in
  polynomial time remains open.
  
  In the study of concurrent systems it is common to model concurrency
  by non-determinism.
  There are, however, some models of computation in which concurrency is
  represented explicitly; 
  elementary net systems and asynchronous transition systems are
  well-known examples.
  History preserving and hereditary history preserving bisimilarities
  are behavioural equivalence notions taking into account causal
  relationships between events of concurrent systems. 
  Checking history preserving bisimilarity is known to be decidable for
  finite labelled elementary nets systems and asynchronous transition
  systems. 
  Its hereditary version appears to be only a slight strengthening and
  it was conjectured to be decidable too.
  In the third paper it is proved that checking hereditary history
  preserving bisimilarity is undecidable for finite labelled
  asynchronous transition systems and elementary net systems.
  This solves a problem open for several years.
  The proof is done in two steps.
  First an intermediate problem of deciding the winner in domino
  bisimulation games for origin constrained tiling systems is introduced
  and its undecidability is shown by a reduction from the halting
  problem for 2-counter machines. 
  Then undecidability of hereditary history preserving bisimilarity is
  shown by a reduction from the problem of domino bisimulation games.