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.