Reachability Is NP-Complete Even for the Simplest Neural Networks

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and conjunctive input/output specifications. We repair some flaws in the original upper and lower bound proofs. We then show that NP-hardness already holds for restricted classes of simple specifications and neural networks with just one layer, as well as neural networks with minimal requirements on the occurring parameters.



On Finite Closure Ordinals in the μ-Calculus

The modal $\mu$-calculus can only express bisimulation-invariant properties. It is a simple consequence of Kleene's Fixpoint Theorem that on structures with finite bisimulation quotients, the fixpoint iteration of any formula converges after finitely many steps. We show that the converse does not hold: we construct a word with an infinite bisimulation quotient that is locally regular so that the iteration for any fixpoint formula of the modal μ-calculus on it converges after finitely many steps. We also show that the reason for the discrepancy between infinite bisimulation quotients and trans-finite fixpoint convergence lies in the fact that the μ-calculus can only express regular properties.



DiMo - Discrete Modelling Using Propositional Logic

We present a learning tool that addresses competences in using propositional logic for modelling purposes. It provides a language for specifying parametrised propositional formula schemes, a backend tool using an incremental SAT solver to exemplify instances of such a scheme to a user learning how to write correct propositional formulas, and a web-based frontend for easy access.



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 them step-by-step.
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 argument.



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 finite satisfiability.



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 interpretation, etc.
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 undecidable.
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 verification. 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(n³) 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 combinatorics.



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 benchmarks.



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 HFL^k,m which are formed using types of bounded order k and arity m only. We establish k-ExpTime-completeness for model checking each HFL^k,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 HFL^k,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 HFL^k,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 complexity.



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 satisfiability problem.



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 logics.



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 logics.



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 players.
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 concurrency. Further extensions of Truth, being in the design stage, comprise the support of the trace model of concurrency as well as game-based model checking algorithms.



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 tableaux.
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 logics.