Model Checking for Branching-Time Temporal Logics
-------------------------------------------------
The thesis considers formal verification of computerized systems.
In formal verification, we verify that a system meets a desired
behavior by checking that a mathematical model of the system
satisfies a formal specification that describes the behavior.
The special method of formal verification that we consider is
branching-time model checking. In this method, formal verification
means determining whether a Kripke structure satisfies a branching
temporal logic formula.
Translating linear temporal logic formulas to automata on
infinite words has proven to be an effective approach for implementing
linear-time model-checking and for obtaining many extensions and
improvements to this verification method. On the other hand, for
branching temporal logics, automata-theoretic techniques have long been
thought to introduce an exponential penalty, making them essentially
useless for model-checking. Efforts to employ the theory of automata
on infinite trees for the benefit of branching-time model checking
started at the 80's, but with no success. In this thesis we show that
alternating tree automata are the key to a comprehensive
automata-theoretic framework for branching temporal logics.
Using the automata-theoretic framework we are able to improved the
space complexity of branching-time model-checking. In particular, we
show that alternating tree automata provide a PSPACE procedure for
CTL* model checking of concurrent programs, and provide an explanation
why this bound can not be achieved for Mu-calculus model checking and
even for its alternation-free fragment. We show that the efficient
bounds hold also for fair model-checking, where a system is checked to
be correct under certain fairness constraints, and for modular
model checking, where a system is checked to be correct by checking
its components.
Improving branching-time model-checking complexity is only one way to
make this method practical. Naturally, there is a trade-off between
the expressive power of a temporal logic and the complexity of its
model-checking problem: the more a logic is expressive, the higher its
model-checking complexity is. A wise model checker should enable the
maximal expressive power and ease of use within the complexity limits
enforced by the user. In the second part of the thesis, we consider
three different ways of extending conventional branching temporal
logics: more liberal syntax, existential quantification over atomic
propositions, and temporal modalities that refer to the past. Each of
the three ways makes branching temporal logic a more convenient
specification language. We examine their both theoretical and
practical~aspects.