On the Expressive Power of Hybrid Branching-Time Logics
Hybrid branching-time logics are a powerful extension of branching-time logics like CTL, CTL*, or even the
modal μ-calculus through the addition of binders, jumps and variable tests. Their expressiveness is not
restricted by bisimulation-invariance anymore. Hence, they do not retain the tree model property, and the
finite model property is equally lost. Their satisfiability problems are typically undecidable, their model
checking problems (on finite models) are decidable with complexities ranging from polynomial to non-elementary
In this paper we study the expressive power of such hybrid branching-time logics beyond some earlier results
about their invariance under hybrid bisimulations. In particular, we aim to extend the hierarchy of non-hybrid
branching-time logics CTL, CTL+, CTL* and the modal μ-calculus to their hybrid extensions. We show that
most separation results can be transferred to the hybrid world, even though the required techniques become a
bit more involved. We also present some collapse results for restricted classes of models that are especially
worth investigating, namely linear, tree-shaped and finite models.
Model Checkign Hybrid Branching-Time Logics
We consider hybridisations of the full branching time logic CTL* and its prominent fragments CTL, CTL+ and FCTL+
through the addition of nominals, binders and jumps. We formally define three types of hybridisations by restricting
the interplay between hybrid operators and path formulae contrary to previous proposals in the literature which ignored
potential problems with a formal semantics. We then investigate the model checking problem for these logics obtaining
expression complexities from PSPACE-completeness to non-elementary decidability and data complexities ranging from
NLOGSPACE to PSPACE. Lastly, we identify a family of fragments of these hybrid logics, called the bounded fragments,
that (in some cases) have the same model checking complexity as their non-hybrid counterparts.
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic.
It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent
calculus are finite trees obtained by successively applying proof rules to formulas, thus simplifying
Students often struggle with the mathematical formalities and the level of abstraction that topics
like formal logic and formal proofs involve. The difficulties can be categorised as syntactic or
semantic. On the syntactic level, students need to understand what a correctly formed proof is, how
rules can be applied (on paper for instance) without leaving the mathematical framework of the sequent
calculus, and so on. Beyond this, on the semantic level, students need to acquire strategies that let
them find the right proof.
The Sequent Calculus Trainer is a tool that is designed to aid students in learning the techniques of
proving given statements formally. In this paper we describe the didactical motivation behind the tool
and the techniques used to address issues on the syntactic as well as on the semantic level.
Multi-Buffer Simulations: Decidability and Complexity
Multi-buffer simulation is a refinement of fair simulation between two nondeterministic
Büchi automata (NBA). It is characterised by a game in which letters get pushed to
and taken from FIFO buffers of bounded or unbounded capacity.
Games with a single buffer approximate the PSPACE-complete language inclusion problem for
NBA. With multiple buffers and a fixed mapping of letters to buffers these games approximate
the undecidable inclusion problem between Mazurkiewicz trace languages.
We study the decidability and complexity of multi-buffer simulations and obtain the following
results: P-completeness for fixed bounded buffers, EXPTIME-completeness in case of a single
unbounded buffer and high undecidability (in the analytic hierarchy) with two buffers of
which at least one is unbounded. We also consider a variant in which the buffers are kept
untouched or flushed and show PSPACE-completeness for the single-buffer case.
A Canonical Model Construction for Iteration-Free PDL with Intersection
We study the axiomatisability of the iteration-free fragment of Propositional Dynamic Logic with
Intersection and Tests. The combination of program composition, intersection and tests makes its
proof-theory rather difficult. We develop a normal form for formulae which minimises the interaction
between these operators, as well as a refined canonical model construction. From these we derive an
axiom system and a proof of its strong completeness.
Model Checking for the Full Hybrid Computation Tree Logic
We consider the hybridisations of the full branching time logic CTL* through the addition of nominals,
binders and jumps. We formally define three fragments restricting the interplay between hybrid operators
and path formulae contrary to previous proposals in the literature which ignored potential problems
with a formal semantics. We then investigate the model checking problem for these logics obtaining
complexities from PSPACE-completeness to non-elementary decidability.
Multi-Buffer Simulations for Trace Language Inclusion
We consider simulation games played between Spoiler and Duplicator
on two Büchi automata in which the choices made by Spoiler can be
buffered by Duplicator in several buffers before she executes them
on her structure. We show that they are useful to approximate the
inclusion of trace closures of languages accepted by finite-state
automata, which is known to be undecidable. We study the
decidability and complexity and show that the game with bounded
buffers can be decided in polynomial time, whereas the game with one
unbounded and one bounded buffer is highly undecidable. We also show
some sufficient conditions on the automata for Duplicator to win the
game (with unbounded buffers).
Two-Buffer Simulation Games
We consider simulation games played between Spoiler and Duplicator on two Büchi automata
in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she
executes them on her structure.
Previous work on such games using a single buffer has shown that they are useful to approximate
language inclusion problems. We study the decidability and complexity and show that games with
two buffers can be used to approximate corresponding problems on finite transducers, i.e. the
inclusion problem for rational relations over infinite words.
The Arity Hierarchy in the Polyadic μ-Calculus
The polyadic &mu-calculus is a modal fixpoint logic whose formulas define relations
of nodes rather than just sets in labelled transition systems. It can express
exactly the polynomial-time computable and bisimulation-invariant queries on
finite graphs. In this paper we show a hierarchy result with respect to expressive
power inside the polyadic &mu-calculus: for every level of fixpoint alternation, greater
arity of relations gives rise to higher expressive power. The proof uses a diagonalisation
Conjunctive Visibly-Pushdown Path Queries
Conjunctive regular path queries are a well-established querying formalism for graph-structured data.
In this formalism it is possible to ask whether a path between two nodes satisfies some regular property.
Several extensions of conjunctive path queries have been investigated in the recent year. Extended
conjunctive regular path queries allow to express queries where several paths are compared and asked to
belong to some regular relation.
In this paper, we investigate another extension of conjunctive regular path queries, where path properties
and path relations are defined by visibly pushdown automata. We study the problem of query evaluation for
extended conjunctive visibly pushdown path queries and their subclasses, and give a complete picture of
their combined and data complexity. In particular, we introduce a weaker notion of extended conjunctive
path queries, called extended conjunctive reachability queries for which query evaluation is polynomial
time in data complexity. We also show that query containment is decidable in 2-EXPTIME for (non-extended)
conjunctive visibly pushdown path queries.
Ramsey-Based Inclusion Checking for Visibly Pushdown Automata
Checking whether one formal language is included in another is
important in many verification tasks. In this article, we provide
solutions for checking the inclusion of languages given by visibly
pushdown automata over both finite and infinite words. Visibly
pushdown automata are a richer automaton model than the classical
finite-state automata, which allows one, for example, to reason
about the nesting of procedure calls in the executions of recursive
imperative programs. As a highlight, the presented solutions do not
rely on explicit automaton constructions for determinization and
complementation. Instead, they are more direct and generalize the
so-called Ramsey-based inclusion-checking algorithms, which apply to
classical finite-state automata and proved to be effective there, to
visibly pushdown automata. We also experimentally evaluate these
algorithms, thereby demonstrating the virtues of avoiding explicit
determinization and complementation constructions.
The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
We present the Sequent Calculus Trainer, a tool that aims at supporting students in learning how to correctly
construct proofs in the sequent calculus for first-order logic with equality. It is a proof assistant supporting
the understanding of all the syntactic principles that need to be obeyed in constructing correct proofs. It
does not provide any help in finding good proof strategies. Instead it aims at understanding the sequent calculus
on lower level that needs to be mastered before one can consider proof strategies. Its main feature is a proper
feedback system embedded in a graphical user interface.
We also report on some empirical findings that indicate how the Sequent Calculus Trainer can improve the students'
success in learning sequent calculus for full first-order logic.
On Guarded Transformation in the Modal μ-Calculus
This paper concerns the problem of transforming a formula of the modal μ-calculus into an equivalent guarded formula. Guarded
form requires every occurrence of a bound fixpoint variable to occur under a modal operator in its defining fixpoint subformula.
Guardedness often makes the design of procedures for the μ-calculus, e.g. satisfiability checking, easier; and many procedures
that can be found in existing literature therefore explicitly require their inputs to be guarded.
Kozen (1983) as well as Banieqbal and Kuiper (1989) already noted that every formula can equivalently be rewritten as a guarded one. Walukiewicz (2000)
presented such a guarded transformation procedure that obviously produces formulas which are exponentially larger in the best case because it requires
Boolean subformulas to be transformed into disjunctive or conjunctive normal form. Kupferman, Vardi and Wolper (2000) as well as Mateescu (2001)
noticed that these subtransformations are unnecessary and presented an optimised guarded transformation which they independently claimed to produce
formulas of linear, respectively quadratic size when measured as the number of distinct subformulas or, equivalently, as the size of its syntax-DAG.
In this paper we first show that these claims about the possibility to do guarded transformation with only a polynomial blowup are flawed; we show
that even the optimised guarded transformations can produce formulas of exponential DAG-size. We then study different forms of syntax for the
modal μ-calculus (vectorial form and hierarchical modal equation systems) and related size measures because they are tightly linked to the question
of whether or not a polynomial guarded transformation is possible. We show that the problem for formulas in vectorial form is as hard as solving
parity games, thus unlikely to admit a simple polynomial solution. We also show that the blowup in the optimised guarded transformation due to
Kupferman, Vardi and Wolper is only quadratic when measured in terms of the Fischer-Ladner closure of a formula, thus revealing that the Fischer-Ladner
closure is not an equivalent measure to DAG-size but can be exponentially smaller. We also investigate the guarded transformation procedure suggested
by Seidl and Neumann (1999) which was also claimed to be polynomial for the modal μ-calculus. This claim is correct regarding the blowup; however,
it heavily relies on the fact that the procedure takes formulas in its usual form and produces hierarchical equation systems. Transforming these into plain
formulas again is what introduces an exponential blowup.
Thus, the question of whether or not a polynomial guarded transformation for formulas of the modal μ-calculus is possible must be considered
as still open. There is some evidence that this problem is reasonably hard.
The Fixpoint-Iteration Algorithm for Parity Games
It is known that the model checking problem for the modal mu-calculus reduces to the problem of solving
a parity game and vice-versa. The latter is realised by the Walukiewicz formulas which are satisfied by a node
in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any
model checking algorithm for the modal mu-calculus, suitably specialised to the Walukiewicz formulas, yields
an algorithm for solving parity games. In this paper we study the effect of employing the most straight-forward
mu-calculus model checking algorithm: fixpoint iteration. It is also one of the few algorithms, let alone
only one, that were not originally devised for parity game solving already. While an empirical study quickly
shows that this does not yield an algorithm that works well in practice, it is interesting from a theoretical
point for two reasons: first, it is exponential on virtually all families of games that were designed as
lower bounds for very particular algorithms suggesting that fixpoint iteration is connected to all those. Second,
fixpoint iteration does not compute positional winning strategies. Note that the Walukiewicz formulas only define
winning regions; some additional work is needed in order to make this algorithm compute winning strategies. We
show that these are particular exponential-space strategies which we call eventually-positional, and we show how
positional ones can be extracted from them.
Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
We consider Polyadic Higher-Order Fixpoint Logic (PHFL), a modal fixpoint logic that is obtained as
the merger of Higher-Order Fixpoint Logic and the Polyadic
mu-Calculus, two formalisms which were originally introduced as expressive languages for
program specification purposes. Polyadicity enables formulas to make assertions about tuples of
states rather than states only. From Higher-Order Fixpoint Logic, PHFL inherits the ability to formalise
properties using higher-order functions.
We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of
higher-order is exactly the Polyadic $\mu$-Calculus, and it is known from Otto's Theorem that it
captures the bisimulation-invariant fragment of the complexity class P. We extend this result by showing
that certain other fragments of PHFL capture the bisimulation-invariant fragments of other important
complexity classes. We first show that EXPTIME in this sense is captured by the fragment using at most
functions of order 1. We also give characterisations of PSPACE and NLOGSPACE by certain formulas of
these two fragments which can be regarded as having tail-recursive functions only.
While many characterisations of complexity classes in descriptive complexity theory have been obtained
as extensions of logics with low expressive power, the work we present here introduces a logic of very
high expressive power and characterises complexity classes by fragments of this generic framework.
An Incremental Approximation to the Finite Satisfiability Problem for Full Interval Temporal Logic
Interval Temporal Logic (ITL) is a powerful formalism to reason about sequences of
events that can occur simultaneously and in an overlapping fashion. Despite its
importance for various application domains, little tool support for automated ITL
reasoning is available, possibly also owed to ITL's undecidability.
We consider bounded satisfiability which approximates finite satisfiability and is
only NP-complete. We provide an encoding into SAT that makes use of the power of
modern incremental SAT solvers and present a tool that tests an ITL specification for
Ramsey-based Inclusion Checking for Visibly Pushdown Automata
Checking whether one formal language is included in another is vital
to many verification tasks. In this article, we provide solutions
for checking the inclusion of languages given by visibly pushdown
automata over both finite and infinite words. Visibly pushdown
automata are a richer automaton model than the classical
finite-state automata, which allows one, for example, to reason
about the nesting of procedure calls in the executions of recursive
imperative programs. As a highlight, the presented solutions do not
comprise automaton constructions for determinization and
complementation. Instead, they are more direct and generalize the
so-called Ramsey-based inclusion-checking algorithms, which apply to
classical finite-state automata and proved to be effective there, to
visibly pushdown automata. We also experimentally evaluate these
algorithms, thereby demonstrating the virtues of avoiding
determinization and complementation constructions.
Buffered Simulation games for Büchi Automata
We introduce buffered simulations,
a family of simulation relations that better approximate language inclusion
than standard simulations. Buffered simulations are
based on a two-player game in which the second player, called here Duplicator,
may skip his turn and respond to a given move in a later round of the game.
We consider various variants of these buffered simulations and establish their
decidability and exact complexity.
Model Checking String Problems
Model checking is a successful technique for automatic program verification. We show that
it also has the power to yield competitive solutions for other problems. We consider three
computation problems on strings and show how the polyadic modal μ-calculus can define
their solutions. We use partial evaluation on a model checking algorithm in order to obtain
an efficient algorithm for the longest common substring problem. It shows comparable good
performance in practice as the well-known suffix tree algorithm. Moreover, it has the conceptual
advantage that it can be interrupted at any time and still deliver long common substrings.
Deciding the Unguarded Model μ-Calculus
The modal μ-calculus extends basic modal logic with second-order quantification in
terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete.
Decision procedures for the modal μ-calculus are not easy to obtain
though since the arbitrary nesting of fixpoint constructs requires some combinatorial
arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision
procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g.
explicitly require formulas to be in guarded normal form. In this paper we present a tableau
calculus for deciding satisfiability of arbitrary, i.e. not necessarily guarded μ-calculus
formulas. It is based on a new unfolding rule for greatest fixpoint formulas which allows
unguarded formulas to be handled without an explicit transformation into guarded form, thus
avoiding a (seemingly) exponential blow-up in formula size. We prove soundness and completeness
of the calculus, and compare it empirically to using guarded transformation instead. The new
unfolding rule can also be used to handle nested star operators in PDL formulas correctly.
Polynomial Guarded Transformation for the Modal μ-Calculus is Still Open
Guarded normal form requires occurrences of fixpoint variables in a mu-calculus-formula
to occur under the scope of a modal operator. The literature contains guarded transformations
that effectively transform a mu-calculus-formula into guarded normal form. We show that the known
guarded transformations can cause an exponential blowup in formula size, contrary to existing
claims of polynomial behaviour. We also show that any polynomial guarded transformation for
mu-calculus-formulas in the more relaxed vectorial form gives rise to a polynomial solution
algorithm for parity games, the existence of which is an open problem.
A Decision Procedure for CTL* Based on Tableaux and Automata
We present a decision procedure for the full branching-time logic CTL* which
is based on tableaux which global conditions on infinite branches. These conditions
can be checked using automata-theoretic machinery. The decision procedure then
consists of a doubly exponential reduction to the problem of solving a parity game.
This has advantages over existing decision procedures for CTL$^*$, in particular
the automata-theoretic ones: the underlying tableaux only work on subformulas of
the input formula. The relationship between the structure of such tableaux and
the input formula is given by very intuitive tableau rules. Furthermore, runtime
experiments with an implementation of this procedure in the MLSolver tool
show the practicality of this approach within the limits of the problem's
computational complexity of being 2EXPTIME-complete.
Extended Computation Tree Logic
We introduce a generic extension of the popular branching-time logic CTL which
refines the temporal until and release operators with formal languages. For
instance, a language may determine the moments along a path that an until
property may be fulfilled. We consider several classes of languages,
represented by automata on finite words, which lead to a range of logics with
different expressive power and complexity. The importance of such logics is
motivated by their use in model checking, program synthesis, abstract
We show that the addition of context-free
languages to the until operator does not have an adverse effect on the model
checking complexity: the logic still allows for polynomial time
model-checking despite the significant increase in expressive power.
This makes this logic a promising candidate for applications in verification.
However, great care has to be taken with adding languages to the
release-operator since, with the
introduction of nondeterminism, the complexity can range from PSPACE to
In addition to these results, we perform an analysis of the expressive power of
these logics with respect to \CTLStar and extensions of PDL, and obtain a
range of results on the complexity of satisfiability.
Local Strategy Improvement for Parity Game Solving
The problem of solving a parity game is at the core of many problems in model checking,
satisfiability checking and program synthesis. Some of the best algorithms for solving parity game
are strategy improvement algorithms. These are global in nature since they require the entire parity
game to be present at the beginning. This is a distinct disadvantage because in many applications one
only needs to know which winning region a particular node belongs to, and a witnessing winning
strategy may cover only a fractional part of the entire game graph.
We present a local strategy improvement algorithms which explores the game graph on-the-fly
whilst performing the improvement steps. We also compare it empirically with
global ones on some benchmarks from the verification domain showing that local strategy
improvement can be very beneficial over the global counterpart.
Alternating Context-Free Grammars Are Conjunctive Grammars And Vice-Versa
Alternating context-free and conjunctive grammars are two formalisms that extend context-free grammars
with an operator for universal choice. The classes of languages derived by such grammars lie
in between CFL and CSL. Here we show that not only the two classes coincide but that the language of
a grammar is invariant under these two semantics. Furthermore, we suggest a third equivalent semantics
which allows words to have exponentially shorter derivations and which is therefore much more suited for
parsing in these grammars.
A Solver for Modal Fixpoint Logics
We present MLSolver, a tool for solving the satisfiability and validity problems
for modal fixpoint logics. The underlying technique is based on characterisations
of satisfiability through infinite (cyclic) tableaux in which branches have an
inner thread structure mirroring the regeneration of least and greatest fixpoint
constructs in the infinite. Well-foundedness for unfoldings of least fixpoints is
checked using deterministic parity automata. This reduces the satisfiability and
validity problems to the problem of solving a parity game. MLSolver then uses
a parity game solver in order to decide satisfiability and derives example models
from the winning strategies in the parity game. Currently supported logics are the
modal and linear-time μ-calculi, CTL*, and PDL (and therefore also CTL
and LTL). MLSolver is designed to allow easy extensions in the form of further
modal fixpoint logics.
On regular Temporal Logics with Past
The IEEE standardized Property Specification Language, PSL
for short, extends the well-known linear-time temporal logic LTL
with so-called semi-extended regular expressions. PSL and the
closely related System-Verilog Assertions, SVA for short,
are increasingly used in many phases of the hardware design cycle,
from specification to verification.
In this article, we extend the common core of these specification
languages with past operators. We name this extension RTL.
Although all ω-regular properties are expressible in PSL,
SVA, and RTL, past operators often allow one to specify properties
more naturally and concisely. In fact, we show that RTL is
exponentially more succinct than the cores of PSL and SVA. On the
star-free properties, RTL is double exponentially more succinct than
LTL, even when LTL is extended with the classical past operators.
Furthermore, we present a translation of RTL into
language-equivalent nondeterministic Büchi automata, which is
based on novel constructions for 2-way alternating automata. Our
translation has almost the same worst-case complexity in terms of
the size of the resulting nondeterministic Büchi automata as the
existing translations for PSL and SVA. Consequently, the
satisfiability and the model-checking problem for RTL fall into the
same complexity classes as the corresponding problems for PSL and
SVA. From the translation it also follows that the blowup of
translating RTL formulas into initially equivalent PSL/SVA formulas
is at most triply exponential.
Digraph Reachability, Model Checking PDL, and an Intersection Problem for Classes of Formal Languages
We show interreducibility under linear-time (Turing) reductions between three families of problems
parametrised by classes of formal languages: the problem of reachability in a directed graph constrained
by a formal language, the model checking problem for Propositional Dynamic Logic over some class of
formal languages, and the problem of deciding whether or not the intersection of a language of some
class with a regular language is empty. This allows several decidability and complexity results to be
transferred, mainly from the area of formal languages to the areas of graph algorithms and modal logics.
A Note on the Relation between Inflationary Fixpoints and Least Fixpoints of Higher-Order
Least fixpoints of monotone functions are an important concept in computer science which
can be generalised to inflationary fixpoints of arbitrary functions. This raises questions
after the expressive power of these two concepts, in particular whether the latter can
be expressed as the former in certain circumstances. We show that the inflationary fixpoint
of an arbitrary function on a lattice of finite height can be expressed as the least fixpoint
of a monotone function on an associated function lattice.
The Model Checking Problem for Propositional Dynamic Logics over Indexed Languages
Propositional Dynamic Logic (PDL) is Modal Logic over structures with accessibility relations represented
by (possibly infinite) languages from a class L of formal languages. We consider IL, the
class of indexed languages. It forms a genuine superclass of the Context-Free Languages whilst being a
genuine subclass of the Context-Sensitive Languages. We present an explicit model checking procedure for
PDL over IL that runs in deterministic exponential time. This matches the complexity-theoretic lower bound
for this problem which is easily obtained from the exponential-time hardness of the emptiness problem for
indexed languagues. This result extends the scope of language classes L for which model checking PDL over
L is known to be decidable.
On the Hybrid Extensions of CTL and CTL+
The paper studies the expressivity, relative succinctness and complexity of satisfiability for hybrid
extensions of the branching-time logics CTL and CTL+ by variables. Previous complexity results
show that only fragments with one variable do have elementary complexity. It is shown that
HCTL+ and HCTL are expressively equivalent but HCTL+ is exponentially more succinct than
HCTL. On the other hand, HCTL+ does not capture CTL*, even with arbitrarily many variables,
as it cannot express the simple CTL* property EGFp. The satisfiability problem for
HCTL+ is complete for triply exponential time, this remains true for quite weak fragments and
quite strong extensions of the logic.
On PSL with Past Operators
The IEEE standardized Property Specification Language, PSL
for short, allows one to express ω-regular properties by
extending the well-known linear-time temporal logic LTL with
semi-extended regular expressions. PSL is increasingly used in many
phases of the hardware design cycle, from specification to
In this paper, we extend PSL with past operators. We name this
extension PPSL. Although PPSL and PSL have the same expressive
power, past operators often allow one to specify properties more
naturally and concisely. In fact, we show that PPSL is exponentially
more succinct than PSL. Furthermore, we present a translation of
PPSL into language-equivalent nondeterministic Büchi automata,
which has almost the same worst-case complexity in terms of the size
of the resulting automata as the existing translations for PSL.
From the presented translation, it follows that PPSL formulas can be
translated into initially equivalent PSL formulas with a triple
exponential blow-up, and that the satisfiability problem and the
model-checking problem for PPSL have the same computational
worst-case complexities as the corresponding problems for PSL.
Solving Parity Games in Practice
Parity games are 2-player games of perfect information and infinite duration that have
important applications in automata theory and decision procedures for temporal logics.
In this paper we investigate practical aspects of solving parity games. We describe
universal optimisations on parity games that aim at reducing their difficulty for any
solver and introduce a generic solver that intertwines these optimisations with a
``real'' solver which is only called on parts of a game that cannot be solved by the
simpler methods. We evaluate this approach empirically.
To CNF or not to CNF? An Efficient Yet Presentable Version of the CYK Algorithm
The most familiar algorithm to decide the membership problem for
context-free grammars is the one by Cocke, Younger and Kasami (CYK) using
grammars in Chomsky normal form (CNF). We propose to teach a simple
modification of the CYK algorithm that uses grammars in a less restrictive
binary normal form (2NF) and two precomputations: the set of nullable
nonterminals and the inverse of the unit relation between symbols.
The modified algorithm is equally simple as the original one, but
highlights that the at most binary branching rules alone are responsible
for the O(n3) time complexity. Moreover, the simple transformation
to 2NF comes with a linear increase in grammar size, whereas some
transformations to CNF found in most prominent textbooks on formal
languages may lead to an exponential increase.
Model Checking for Hybrid Logic
We consider the model checking problem for Hybrid Logic. Known algorithms so far
are global in the sense that they compute, inductively, in every step the set of
all worlds of a Kripke structure that satisfy a subformula of the input. Hence,
they always exploit the entire structure. Local model checking tries to avoid this
by only traversing necessary parts of the input in order to establish or refute
the satisfaction relation between a given world and a formula.
We present a framework for local model checking of Hybrid Logic based on games. We
show that these games are simple reachability games for ordinary Hybrid Logic and
weak Büchi games for Hybrid Logic with operators interpreted over the transitive
closure of the accessibility relation of the underlying Kripke frame, and show how
to solve these games thus solving the local model checking problem.
Since the first-order part of Hybrid Logic is inherently hard to localise in model
checking, we give examples, in the end, of how global model checkers can be optimised
in certain special cases using well-established techniques like fixpoint approximations
and divide-and-conquer algorithms.
A Purely Model-Theoretic Proof of the Exponential Succinctness Gap between CTL+ and CTL
We present a proof of the exponential succinctness gap between the branching time
temporal logics CTL+ and CTL. The lower bound on formule size presented
here is non-optimal, but the proof is simple and avoids automata-theory and
Polyadic Dynamic Logics for HPSG Parsing
Non-Regular Fixed-Point Logics and Games
Analyzing Context-Free Grammars Using an Incremental SAT Solver
We consider bounded versions of undecidable problems about context-free languages
which restrict the domain of words to some finite length: inclusion, intersection, universality,
equivalence, and ambiguity. These are in NP and thus solvable by a reduction to the
satisfiability problem for propositional logic. We present such encodings - fully utilizing
the power of incrementat SAT solvers - prove correctness and validate this approach with some
Temporal Logics Beyond Regularity
Non-regular program correctness properties play an important role in the specification of unbounded
buffers, recursive procedures, etc. This thesis surveys results about the relative expressive power
and complexity of temporal logics which are capable of defining non-regular properties. In particular,
it features Propositional Dynamic Logic of Context-Free Programs, Fixpoint Logic with Chop, the Modal
Iteration Calculus, and Higher-Order Fixpoint Logic.
Regarding expressive power we consider two classes of structures: arbitrary transition systems as
well as finite words as a subclass of the former. The latter is meant to give an intuitive account
of the logics' expressive powers by relating them to known language classes defined in terms of
grammars or Turing Machines.
Regarding the computational complexity of temporal logics beyond regularity we focus on their
model checking problems since their satisfiability problems are all highly undecidable. Their
model checking complexities range between polynomial time and non-elementary.
Linear Time Logics around PSL: Complexity, Expressiveness, and a little bit of Succinctness
We consider linear time temporal logic enriched with semi-extended regular expressions through
various operators that have been proposed in the literature, in particular in Accelera's Property
Specification Language. We obtain results about the expressive power of fragments of this logic
when restricted to certain operators only: basically, all operators alone suffice for expressive
completeness w.r.t.\ omega-regular expressions, just the closure operator is too weak.
We also obtain complexity results. Again, almost all operators alone suffice for EXPSPACE-completeness,
just the closure operator needs some help.
Cut-Free Sequent Systems for Temporal Logic
Currently known sequent systems for temporal logics such as linear time temporal
logic and computation tree logic either rely on a cut rule, an invariant rule, or an
infinitary rule. The first and second violate the subformula property and the third
has infinitely many premises. We present finitary cut-free invariant-free weakeningfree
and contraction-free sequent systems for both logics mentioned. In the case of
linear time all rules are invertible. The systems are based on annotating fixpoint
formulas with a history, an approach which has also been used in game-theoretic
characterisations of these logics.
Semantical Expansion of Two-Level Boolean Formulas for Minimisation
Semantical expansion aims at boosting minimisation heuristics for Boolean formulas. It provides
an easy way of deciding whether or not a given minterm, resp. clause, can be added safely to
a formula in DNF, resp. CNF. We suggest to use incremental and complete SAT solvers and instances
of UNSAT for these decisions, and report on some preliminary empirical results.
Polyadic Dynamic Logics for Deep Parsing
Head-driven phrase structure grammar (HPSG) is one of the most prominent theories employed
in deep parsing of natural language. Many linguistic theories are arguably best formalized
in extensions of modal or dynamic logic, and HPSG seems to be no exception. The adequate
extension of dynamic logic has not been studied in detail, however; its most important aspect
is its reference to sets of substructures. In this paper, the proper extension is identified,
and some important results are established: Satisfiability on unrestricted structures is
undecidable, and model checking is shown to be PSPACE-hard. The complexity of parsing in the
set-free fragment of HPSG has been shown to be NP-complete under a few linguistically motivated
restrictions; in this paper, similar restrictions are identified that turn model checking
tractable and parsing NP-complete, while the effects of set values are restored.
The Complexity of Model Checking Higher-Order Fixpoint Logic
Higher Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the
modal μ-calculus. This makes it a highly expressive temporal logic that is capable
of expressing various interesting correctness properties of programs that are not
expressible in the modal μ-calculus.
This paper provides complexity results for its model checking problem. In particular
we consider its fragments HFLk,m which are formed using types of bounded order k
and arity m only. We establish k-ExpTime-completeness for model checking each HFLk,m
fragment. For the upper bound we reduce the problem to the problem of solving rather large
parity games of small index. As a consequence of this we obtain an ExpTime upper bound on the
expression complexity of each HFLk,m.
The lower bound is established by a reduction from the word problem for alternating
(k-1)-fold exponential space bounded Turing Machines. As a corollary we obtain
k-ExpTime-completeness for the data complexity of HFLk,m already when m ≥ 4.
Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
We present a model checking algorithm for HFL1, the first-order fragment
of Higher-Order Fixpoint Logic. This logic is capable of expressing many interesting properties
which are not regular and, hence, not expressible in the modal
mu-calculus. The algorithm avoids best-case exponential behaviour by localising
the computation of functions and can be implemented symbolically using BDDs.
We show how insight into the behaviour of this procedure, when run on a fixed formula,
can be used to obtain specialised algorithms for particular problems. This yields, for example,
the competitive antichain algorithm for NFA universality but also a new algorithm for
a string matching problem.
A Proof System for the Linear Time μ-Calculus
The linear time μ-calculus extends LTL with arbitrary least and greatest fixpoint operators. This
gives it the power to express all ω-regular languages, hence, it is more expressive than LTL.
The validity problem is PSPACE-complete for both LTL and the linear time μ-calculus. However, in
practice it is more difficult for the latter because of nestings of fixpoint operators and the fact
that variables can have several occurrences in a formula.
We present a simple proof system for the linear time μ-calculus with a high-level specification on
infinite branches in these proofs. We prove it sound and complete, and present two different methods
for finding proofs, i.e. for checking these specifications. One uses nondeterministic Büchi automata,
the other morphisms in a finite category which can also be used to check termination of certain
recursive functional programs.
Specifying Non-Regular Properties of Runs
We consider the problem of specifying non-regular properties of finite
and infinite words as abstractions of system runs. We prove an equi-expressibility
result between LFLC, the Linear Time μ-Calculus enriched with sequential composition,
and alternating ω-context-free grammars with a weak parity acceptance condition.
This correspondence is used to obtain some (un-)decidability results regarding
satisfiability and model checking for this logic. A side-effect of this correspondence
is the collapse of the alternation-hierarchy in LFLC.
When Not Losing Is Better than Winning: Abstraction and Refinement for the Full μ-Calculus
This work presents a novel game-based approach to abstraction-refinement for the full μ-calculus,
interpreted over 3-valued semantics.
A novel notion of non-losing strategy is introduced and exploited for refinement. Previous
works on refinement in the context of 3-valued semantics require a direct algorithm for
solving a 3-valued model checking game. This was necessary in
order to have the information needed for refinement available on
one game board. In contrast, while still considering a 3-valued
model checking game, here we reduce the problem of solving the
game to solving two 2-valued model checking (parity) games.
In case the result is indefinite (don't know), the corresponding
non-losing strategies, when combined, hold all the information
needed for refinement. This approach is beneficial since it can
use any solver for 2-valued parity games. Thus, it can take
advantage of newly developed such algorithms with improved
Bounded Model Checking for Weak Alternating Büchi Automata
We present an incremental bounded model checking encoding
into propositional satisfiability where the property
specification is expressed as a weak alternating Büchi automaton (WABA).
The encoding is linear in the specification, or, more exactly
O(|I| + k*|T| + k*|δ|), where |I| is the size of the initial state
predicate, k is the bound, |T| is the size of the transition relation,
and |δ| is the size of the WABA transition relation.
Minimal length counterexamples can also be provided by the approach
by increasing the encoding size to be quadratic in the number of
states in the largest component of the WABA.
The proposed encoding can be used to implement more efficient bounded
model checking algorithms for $\omega$-regular industrial specification
languages such as Accellera's Property Specification Language (PSL).
Encouraging experimental results on a prototype implementation are reported.
Temporal Logics for Non-Regular Properties: Model Checking
The modal μ-calculus captures exactly the bisimulation-invariant
regular tree languages. Hence, properties expressed in formulas of
its fragments like LTL or CTL for instance are only regular.
We present temporal logics whose expressive power reaches beyond that
of the modal $\mu$-calculus and survey known result
about these with a focus on their model checking problems --- due to
the undecidability of satisfiability.
Solving Parity Games by a Reduction to SAT
This paper presents a reduction from the problem of solving parity games
to the satisfiability problem in propositional logic (SAT). The reduction
is done in two stages, first into difference logic, i.e. SAT combined
with the theory of integer differences, an instance of the SAT modulo
theories (SMT) framework. In the second stage the integer variables and
constraints of the difference logic encoding are replaced with a set of
Boolean variables and constraints on them, giving rise to a pure SAT
encoding of the problem. The reduction uses Jurdzinski's characterisation
of winning strategies via progress measures. The reduction is motivated by
the success of SAT solvers in symbolic verification, bounded model checking
in particular. The paper reports on prototype implementations of the reductions
and presents some experimental results.
Improved Bounded Model Checking for the Linear Time μ-Calculus
The linear time μ-calculus - resp. its alternation-free fragment - is
an extension of LTL that is capable of expressing all ω-regular
properties. Two optimised encodings of the bounded model checking problem for
this logic into propositional logic are being presented. They improve over an
earlier encoding by implicitly quantifying over loops, by employing a bounded
semantics that yields better approximative results, by handling greatest fixpoint
formulas in a simpler and least fixpoint formulas in a possibly smaller way, and
by building the propositional formulas locally. The two encodings are evaluated
empirically and compared to each other.
Three Notes on the Complexity of Model Checking Fixpoint Logic with Chop
This paper provides lower complexity bounds of deterministic exponential time
for the combined, data and expression complexity of Fixpoint Logic with
Chop. This matches the previously known upper bound showing that its model
checking problem is EXPTIME-complete, even when the transition system or
the formula is fixed. All results already hold for the alternation-free
fragment of Fixpoint Logic with Chop.
Bounded Model Checking for All Regular Properties
The technique of bounded model checking is extended to the linear
time μ-calculus, a temporal logic that can express all monadic
second-order properties of ω-words, in other words, all
ω-regular languages. Experimental evidence is presented
showing that the method can be successfully employed for properties
that are hard or impossible to express in the weaker logic LTL that
is traditionally used in bounded model checking.
Solving Parity Games by a Reduction to SAT
This paper presents a reduction from the problem of solving parity
games to the satisfiability problem for formulas of propositional
logic in conjunctive normal form. It uses Jurdzinski's characterisation
of winning strategies via progress measures. The reduction is motivated
by the apparent success that using SAT solvers has had in symbolic
verification. The paper reports on a prototype implementation of the
reduction and presents some runtime results.
Bounded Model Checking for All Regular Properties Using Weak Alternating Parity Automata
An encoding for bounded model checking omega-regular
properties is presented. It uses weak alternating parity automata
as the specification model for such properties.
The Complexity of Model Checking Higher Order Fixpoint Logic
This paper analyzes the computational complexity of the model checking problem
for Higher Order Fixpoint Logic -- the modal μ-calculus enriched with a
typed λ-calculus. It is hard for every level of the elementary
time/space hierarchy and in elementary time/space when restricted to formulas
of bounded type order.
2-ExpTime Lower Bounds for Propositional Dynamic Logics with Intersection
In 1984, Danecki proved that satisfiability in IPDL, i.e.,
Propositional Dynamic Logic (PDL) extended with an intersection
operator on programs, is decidable in deterministic double
exponential time. Since then, the exact complexity of IPDL has
remained an open problem: the best known lower bound was the
ExpTime one stemming from plain PDL until, in 2004, the first
author established ExpSpace-hardness. In this paper, we finally
close the gap and prove that IPDL is hard for 2-ExpTime, thus
2-ExpTime-complete. We then sharpen our lower bound, showing that
it even applies to IPDL without the test operator interpreted
on tree structures.
Propositional Dynamic Logic of Context-Free Programs and Fixpoint Logic with Chop
This paper compares Propositional Dynamic Logic of Non-Regular Programs and Fixpoint Logic with
Chop. It identifies a fragment of the latter which is equi-expressive to the former. This
relationship transfers several decidability and complexity results between the two logics.
Model Checking Propositional Dynamic Logic with All Extras
This paper presents a model checking algorithm for Propositional Dynamic
Logic (PDL) with looping, repeat, test, intersection, converse, program complementation
as well as context-free programs. The algorithm shows that the model checking
problem for PDL remains PTIME-complete in the presence of all these operators,
in contrast to the high increase in complexity that they cause for the
The Alternation Hierarchy in Fixpoint Logic with Chop Is Strict Too
Fixpoint Logic with Chop extends the modal mu-calculus with a sequential
composition operator which results in an increase in expressive power. We
develop a game-theoretic characterisation of its model checking problem
and use these games to show that the alternation hierarchy in this logic
is strict. The structure of this result follows the lines of Arnold's
proof showing that the alternation hierarchy in the modal mu-calculus
is strict over the class of binary trees.
Weak Automata for the Linear Time μ-Calculus
This paper presents translations forth and back between formulas of the linear
time μ-calculus and parity automata with a weak acceptance condition. This
yields a normal form for these formulas, in fact showing that the linear time
alternation hierarchy collapses at level 0 and not just at level 1 as known so
far. The translation from formulas to automata can be optimised yielding automata
whose size is only exponential in the alternation depth of the formula.
Parallel and Symbolic Model Checking for Fixpoint Logic with Chop
We consider the model checking problem for FLC, a modal fixpoint logic
capable of defining non-regular properties. This paper presents a refinement
of a symbolic model checker and discusses how to parallelise this algorithm.
It reports on a prototype implementation of the algorithm in Glasgow
Parallel Haskell and its performance on a cluster of workstations.
Game Over: The Foci Approach to LTL Satisfiability and Model Checking
Focus games have been shown to yield game-theoretical characterisations
for the satisfiability and the model checking problem for various temporal
logics. One of the players is given a tool -- the focus -- that enables
him to show the regeneration of temporal operators characterised as least
or greatest fixpoints. His strategy usually is build upon a priority list
of formulas and, thus, is not positional. This paper defines foci games
for satisfiability of LTL formulas. Strategies in these games are trivially
positional since they maximally parallelise all of the focus player's
choices, thus resulting in a 1-player game in effect. The games are shown
to be correct and to yield smaller (counter-)models than the focus games.
Finally, foci games for model checking LTL are defined as well.
A Quick Axiomatisation of LTL with Past
This paper defines focus games for satisfiability of linear time
temporal logic with past operators. The games are defined in such
a way that a complete axiomatisation can easily be obtained from
the game rules.
Don't Know in the μ-Calculus
In this paper we extend to framework of three valued logics to the
setting of the μ-calculus. Three valued logics are important in
the context of verifying systems based on abstractions. Given an
abstract model, a formula might either be satisfied or falsified, or
it might be undetermined since the abstraction is too coarse.
We give a formal semantics of the 3-valued μ-calculus and
present a game-based model-checking algorithm that either verifies
or falsifies the property to check, or, it might answer don't know.
For the latter case, we discuss how to refine the abstraction to finally
answer whether the property holds or not.
A Lower Complexity Bound for Propositional Dynamic Logic with Intersection
This paper shows that satisfiability for Propositional Dynamic Logic with
Intersection is EXPSPACE-hard. The proof uses a reduction from the word
problem for alternating, exponential time bounded Turing Machines.
Symbolic Model Checking of Non-Regular Properties
This paper presents a symbolic model checking algorithm for Fixpoint Logic
with Chop, an extension of the modal mu-calculus capable of defining
non-regular properties. Some empirical data about running times of a naive
implementation of this algorithm are given as well.
Disclaimer: Unfortunately, the algorithm is not presented in a
correct way. Instead of iterating functions until they become stable on
one argument it is necessary to iterate until they become stable on
all arguments and then project down to one argument.
Satisfiability and Completeness of Converse-PDL Replayed
This paper reinvestigates satisfiability and completeness of Propositional
Dynamic Logic with Converse. By giving a game-theoretic characterisation
of its satisfiability problem using focus games, an axiom system that is
extracted from these games can easily be proved to be complete.
Verification of Non-Regular Properties
We present a game-based formalism that can be used to do local model checking
for FLC, a modal fixed point logic that extends the mu-calculus with a
sequential composition operator. This logic is capable of expressing
non-regular properties which are interesting for verification purposes.
Model Checking Games for Modal and Temporal Logics
In this paper we show how to obtain model checking games for modal and
temporal logics in a general way. They are defined by translating the
logics' operators one by one into rules and winning conditions. We point
out what the important properties of the games are because of which they
are sound and complete, and give general correctness proofs.
The most common operators used in modal and temporal logics are treated.
For logics featuring these operators, this paper gives a recipe for
defining model checking games and delivers the correctness proofs. An
important distinction is made between logics that are interpreted over
states and those interpreted over paths of a labelled transition system.
For logics containing other operators than the ones presented here, this
paper serves as a template showing what lemmas should hold and how to
obtain soundness and completeness. Finally, it gives an overview of the
state-of-the-art in game-based model checking for modal and temporal
CTL+ is Complete for Double Exponential Time
We show that the satisfiability problem for CTL+, the branching time
logic that allows boolean combinations of path formulas inside a path
quantifier but no nestings of them, is 2-EXPTIME-hard. The construction
is inspired by Vardi and Stockmeyer's 2-EXPTIME-hardness proof of CTL*'s
satisfiability problem. As a consequence, there is no subexponential
reduction from CTL+ to CTL which preserves satisfiability.
Alternating Context-Free Languages and Linear Time μ-Calculus with Sequential Composition
This paper shows that linear time mu-calculus with sequential
composition defines exactly those properties that are expressible
with alternating context-free grammars for omega-words. This helps
to understand the expressive power of modal mu-calculus with a chop
operator and provides a logical characterisation of the class of
alternating context-free languages.
Satisfiability Games for CTL*
This paper defines games for the full branching time logic CTL*. They
provide a direct method to check satisfiability of a formula since they
work on its subformulas only. Thus, this method avoids determinization
of automata or translations into other logics. Instead, it employs a
simple tool called focus which the players use to highlight one particular
formula in a set of subformulas. Focus games have been proved to be a
useful method for working with temporal logics. For instance, model
checking focus games for CTL* and LTL, as well as satisfiability
checking focus games for LTL and CTL have been shown to work. Indeed,
the games of this paper are an extension of the latter ones. They can
be used as a basis of a decision procedure for CTL* that matches the
known lower bound of double exponential time.
Local Model Checking Games for Fixed Point Logic with Chop
The logic considered in this paper is FLC, fixed point logic with chop. It
is an extension of modal mu-calculus MMC that is capable of defining
non-regular properties which makes it interesting for verification purposes.
Its model checking problem over finite transition systems is PSPACE-hard.
We define games that characterise FLC's model checking problem over arbitrary
transition systems. Over finite transition systems they can be used as a basis
of a local model checker for FLC. I.e. the games allow the transition system
to be constructed on-the-fly. On formulas with fixed alternation depth and
so-called sequential depth deciding the winner of the games is PSPACE-complete.
The best upper bound for the general case is EXPSPACE which can be improved
to EXPTIME at the cost of losing the locality property. On modal mu-calculus
formulas the games behave equally well as the model checking games for MMC,
i.e. deciding the winner is in NP intersect co-NP.
Model Checking Fixed Point Logic with Chop
This paper investigates FLC, fixed point logic with chop, which extends modal
mu-calculus with a sequential composition operator. We prove some interesting
properties of FLC, like the tree model property and bisimulation invariance.
Furthermore, we give examples of formulas that cannot be expressed in modal
mu-calculus. The main part of the paper deals with FLC's model checking problem.
A tableau system is defined and proved sound and complete. It gives rise to an
EXPTIME model checking algorithm. It is also shown that FLC model checking can
be done in PSPACE for formulas with fixed alternation depth. Finally, the
problem is proved to be PSPACE-hard.
Modal mu-calculus and sequential composition
In 1999 Markus Mueller-Olm introduced FLC which enriches modal
mu-calculus with a sequential composition operator. Following his ideas we
define LFLC, its linear time version and present a few results on its
expressiveness beyond regular languages. Furthermore, we will consider
decidability issues (i.e. satisfiability and model checking) of these
Satisfiability Games and Completeness of Temporal Logic
Tableaux-like methods to solve satisfiability or the model checking problem for
certain temporal logics face a very particular difficulty: to capture correctly
the regeneration of fixed point constructs. This arises for example in CTL* model
checking with both least and greatest fixed points, and in checking satisfiability
for LTL, CTL, or even the dynamic logic PDL with least fixed points.
We show how a rather novel approach, called focus, can be employed to overcome
these difficulties elegantly. The decision procedures are formulated in terms of
two-player games taking choices on sets of formulas such that one of the players
has the ability to focus on a particular formula and, hence, follow fixed point
constructs while they are unfolded.
As opposed to automata-based satisfiability checking this way yields a very simple
technique to prove completeness of these logics, i.e. to exhibit an axiomatisation
such that every consistent formula of this system is satisfiable. The constructed
axiom systems reflects the game rules and the winning strategies for one of the
Further work consists of extending these methods to satisfiability of CTL* and the
modal mu-calculus, since the proofs of their completenesses are very delicate.
Moreover, there are other temporal logics over non-standard structures which are
not known to be complete yet.
Focus Games for Satisfiability and Completeness of Temporal Logic
We introduce a simple game theoretic approach to satisfiability checking of temporal logic, for LTL
and CTL, which has the same complexity as using automata. The mechanisms involved are both explicit
and transparent, and underpin a novel approach to developing complete axiom systems for temporal logic.
The axiom systems are naturally factored into what happens locally and what happens in the limit. The
completeness proofs utilise the game theoretic construction for satisfiability: if a finite set of
formulas is consistent then there is a winning strategy (and therefore construction of an explicit
model is avoided).
Model Checking Games for Branching Time Logics
This paper defines and examines model checking games for the branching time temporal logic CTL*.
The games employ a technique called focus which enriches sets by picking out one distinguished element.
This is necessary to avoid ambiguities in the regeneration of temporal operators. The correctness of
these games is proved, and optimisations are considered to obtain model checking games for important
fragments of CTL*. A game based model checking algorithm that matches the known lower and upper
complexity bounds is sketched.
Model Checking Games for CTL*
We define model checking games for the temporal logic CTL* and prove their correctness. They
provide a technique for using model checking interactively in a verification/specification process.
Their main feature is to construct paths in a transition system stepwise. That enables them to be
the basis for a local model checking algorithm with a natural notion of justification. However, this
requires configurations of a game to contain sets of formulas. Moreover, an additional structure on
these sets, called focus, has to be used to guarantee correctness.
A Game Based Approach to CTL* Model Checking
We introduce a definition of model checking games for the full branching time logic CTL*
and sketch a proof of their correctness. These games are a helpful technique for using model checking
in the verification of concurrent systems, because they may not only show that a specified property is
violated, but also why it is.
Truth - A Verification Platform for Concurrent Systems
We briefly explain the design and implementation of the newly
developed tool Truth which serves as a general platform for the
systematic investigation of different specification languages,
semantic models, and logics for concurrent systems, supported by
enhanced visualization capabilities. Modularity is achieved by
employing the rewriting logic approach as a semantic framework for
Further extensions of Truth, being in the design stage, comprise the
support of the trace model of concurrency as well as game-based model
Games for Modal and Temporal Logics
Every logic comes with several decision problems. One of them is the model checking problem: does
a given structure satisfy a given formula? Another is the satisfiability problem: for a given
formula, is there a structure fulfilling it?
For modal and temporal logics; tableaux, automata and games are commonly accepted as helpful techniques
that solve these problems. The fact that these logics possess the tree model property makes tableau
structures suitable for these tasks. On the other hand, starting with Büchi's work, intimate connections
between these logics and automata have been found. A formula can describe an automaton's behaviour, and
automata are constructed to accept exactly the word or tree models of a formula.
In recent years the use of games has become more popular. There, an existential and a universal player play
on a formula (and a structure) to decide whether the formula is satisfiable, resp. satisfied. The logical
problem at hand is then characterised by the question of whether or not the existential player has a winning
strategy for the game.
These three methodologies are closely related. For example the non-emptiness test for an alternating
automaton is nothing more than a 2-player game, while winning strategies for games are very similar to
Game-theoretic characterisations of logical problems give rise to an interactive semantics for the
underlying logics. This is particularly useful in the specification and verification of concurrent systems
where games can be used to generate counterexamples to failing properties in a very natural way.
We start by defining simple model checking games for Propositional Dynamic Logic, PDL, in
Chapter 4. These allow model checking for PDL in linear running time. In fact, they
can be obtained from existing model checking games for the alternating free mu-calculus. However, we include
them here because of their usefulness in proving correctness of the satisfiability games for PDL later on.
Their winning strategies are history-free.
Chapter 5 contains model checking games for branching time logics. Beginning with the
Full Branching Time Logic CTL* we introduce the notion of a focus game. Its key idea is to equip
players with a tool that highlights a particular formula in a set of formulas. The winning conditions for
these games consider the players' behaviours regarding the change of the focus. This proves to be useful in
capturing the regeneration of least and greatest fixed point constructs in CTL*. Deciding the winner
of these games can be done using space which is polynomial in the size of the input. Their winning strategies
are history-free, too.
We also show that model checking games for CTL+ arise from those for CTL* by disregarding the
focus. This does not affect the polynomial space complexity. These can be further optimised to obtain model
checking games for the Computation Tree Logic CTL which coincide with the model checking games for the
alternating free mu-calculus applied to formulas translated from CTL into it. This optimisation improves
the games' computational complexity, too. As in the PDL case, deciding the winner of such a game can be
done in linear running time. The winning strategies remain history-free.
Focus games are also used to give game-based accounts of the satisfiability problem for Linear Time Temporal
Logic LTL, CTL and PDL in Chapter 6. They lead to a polynomial space decision procedure
for LTL, and exponential time decision procedures for CTL and PDL. Here, winning strategies are only
history-free for the existential player. The universal player's strategies depend on a finite
part of the history of a play.
In spite of the strong connections between tableaux, automata and games their differences are more than
simply a matter of taste. Complete axiomatisations for LTL, CTL and PDL can be extracted from the
satisfiability focus games in an elegant way. This is done in Chapter 7 by formulating the game
rules, the winning conditions and the winning strategies in terms of an axiom system. Completeness of this
system then follows from the fact that the existential player wins the game on a consistent formula, i.e.
it is satisfiable.
We also introduce satisfiability games for CTL* based on the focus approach. They lead to a double
exponential time decision procedure. As in the LTL, CTL and PDL case, only the
existential player has history-free winning strategies. Since these strategies witness satisfiability of
a formula and stay in close relation to its syntactical structure, it might be possible to derive a complete
axiomatisation for CTL* from these games as well.
Finally, Chapter 9 deals with Fixed Point Logic with Chop, FLC. It extends modal mu-calculus
with a sequential composition operator. Satisfiability for FLC is undecidable but its model checking
problem remains decidable. In fact it is hard for polynomial space.
We give two different game-based solutions to the model checking problem for FLC. Deciding the winner for
both types of games meets this polynomial space lower bound for formulas with fixed alternation (and sequential)
depth. In the general case the winner can be determined using exponential time, resp. exponential space. The
former result holds for games that give rise to global model checking whereas the latter describes the complexity
of local FLC model checking. FLC is interesting for verification purposes since it -- unlike all the
other logics discussed here -- can describe properties which are non-regular.
The thesis concludes with remarks and comments on further research in the area of games for modal and temporal