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.

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 leading to logics with different expressive power and complexity, whose importance is motivated by their use in model checking, synthesis, abstract interpretation, etc. We show that even with context-free languages on the until operator the logic still allows for polynomial time model-checking despite the significant increase in expressive power. This makes the logic a promising candidate for applications in verification. In addition, we analyse the complexity of satisfiability and compare the expressive power of these logics to CTL* and extensions of PDL.

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.

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.

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

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.