Abstract: This paper proves a long standing conjecture in formal language theory. It shows that all regular languages are Church-Rosser congruential. The class of Church-Rosser congruential languages was introduced by McNaughton, Narendran, and Otto in 1988. A language L is Church-Rosser congruential if there exists a finite, confluent, and length-reducing semi-Thue system S such that L is a finite union of congruence classes modulo S. It was known that there are deterministic linear context-free languages which are not Church-Rosser congruential, but on the other hand it was strongly believed that all regular languages are of this form. This paper solves the conjecture affirmatively by actually proving a more general result.

Abstract: Parity games are a much researched class of games in NP \cap CoNP that are not known to be in P. Consequently, researchers have considered specialised algorithms for the case where certain graph parameters are small. In this paper, we show that, if a tree decomposition is provided, then parity games with bounded treewidth can be solved in O(k^{3k + 2} \cdot n^2 \cdot (d + 1)^{3k}) time, where n, k, and d are the size, treewidth, and number of priorities in the parity game. This significantly improves over previously best algorithm, given by Obdr\v{z}\'alek, which runs in O(n \cdot d^{2(k+1)^2}) time. Our techniques can also be adapted to show that the problem lies in the complexity class NC^2, which is the class of problems that can be efficiently parallelized. This is in stark contrast to the general parity game problem, which is known to be P-hard, and thus unlikely to be contained in NC.

Abstract: In this paper we study the complexity of computing the game bisimulation metric defined by Luca de Alfaro et al. on Markov Decision Processes. It is proved that the undiscounted version of the metric is characterized by a quantitative game $\mu$-calculus defined by Luca de Alfaro and Rupak Majumdar, which can express reachability and $\omega$-regular specifications. And the discounted version of the metric is characterized by the discounted version of the quantitative game $\mu$-calculus. In the discounted case, we show that the metric can be computed exactly by extending the method for Labelled Markov Chains by Di Chen et al. And in the undiscounted case, we prove that the problem whether the metric between two states is under a given threshold can be decided in $\mathsf{NP}\cap\mathsf{coNP}$, which improves the previous $\mathsf{PSPACE}$ upperbound by Krishnendu Chatterjee et al.

Abstract: Quantitative languages are extension of boolean languages that assign to each word a real number. With quantitative languages, systems and specifications can be formalized more accurately. For example, a system may use a varying amount of some resource (e.g., memory consumption, or power consumption) depending on its behavior, and a specification may assign a maximal amount of available resource to each behavior, or fix the long-run average available use of the resource.
Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. Mean-payoff automata forms a class of quantitative languages that is not robust, since it is not closed under the basic algebraic operations: min, max, sum and numerical complement. The class of mean-payoff automaton expressions, recently introduced by Chatterjee et al., is currently the only known class of quantitative languages that is robust, expressive and decidable. This class is defined as the closure of mean-payoff automata under the basic algebraic operations. In this work, we prove that all the classical decision problems for mean-payoff expressions are PSPACE-complete. Our proof improves the previously known 4EXPTIME upper bound. In addition, our proof is significantly simpler, and fully accessible to the automata-theoretic community.

Abstract: Cost functions are defined as mappings from a domain like words or trees to N ∪ {∞}, modulo an equivalence relation ≈ which ignores exact values but preserves boundedness properties. Cost logics, in particular cost monadic second-order logic, and cost automata, are different ways to define such functions. These logics and automata have been studied by Colcombet et al. as part of a “theory of regular cost functions”, an extension of the theory of regular languages which retains robust equivalences, closure properties, and decidability. We develop this theory over infinite words, and show that the classical results FO = LTL and MSO = WMSO also hold in this cost setting (where the equivalence is now up to ≈). We also describe connections with forms of weak alternating automata with counters.

Abstract: Frick and Grohe [J. ACM 48 (2006), 1184-1206] introduced a notion of graph classes with locally bounded tree-width and established that every first order logic property can be decided in almost linear time in such a graph class. Here, we introduce an analogous notion for matroids (locally bounded branch-width) and show the existence of a fixed parameter algorithm for first order logic properties in classes of regular matroids with locally bounded branch-width. To obtain this result, we show that the problem of deciding the existence of a circuit of length at most k containing two given elements is fixed parameter tractable for regular matroids.

Abstract: We introduce a new cartesian closed category of two-level arenas and innocent strategies to model intersection types that are refinements of simple types. Intuitively a property (respectively computation) on the upper level refines that on the lower level. We prove Subject Expansion---any lower-level computation is closely and canonically tracked by the upper-level computation that lies over it---which is a measure of the robustness of the two-level semantics. The game semantics of the type system is fully complete: every winning strategy is the denotation of some derivation. To demonstrate the relevance of the game model, we use it to construct new semantic proofs of non-trivial algorithmic results in higher-order model checking.

Abstract: We establish connections between the size of circuits and formulas computing monotone Boolean functions and the size of first-order and nonrecursive Datalog rewritings for conjunctive queries over OWL 2 QL ontologies. We use known lower bounds and separation results from circuit complexity to prove similar results for the size of rewritings that do not use non-signature constants. For example, we show that, in the worst case, positive existential and nonrecursive Datalog rewritings are exponentially longer than the original queries; nonrecursive Datalog rewritings are in general exponentially more succinct than positive existential rewritings; while first-order rewritings can be superpolynomially more succinct than positive existential rewritings.

Abstract: In simply typed lambda-calculus with one ground type the following theorem due to Loader holds.
(i) Given the full model F over a finite set, the question whether some element f in F is lambda-definable is undecidable. In the lambda-calculus with intersection types based on countably many atoms, the following is proved by Urzyczyn. (ii) It is undecidable whether a type is inhabited. Both statements are major results presented in [Barendregt, Dekkers and Statman]. We show that (i) and (ii) follow from each other in a natural way, by interpreting intersection types as continuous functions logically related to elements of F. From this, and a result by Joly on lambda-definability, we get that Urzyczyn's theorem already holds for intersection types with at most two atoms.

Abstract: We reconsider the problem of containment of monadic datalog (MDL) queries in unions of conjunctive queries (UCQs). Prior work has dealt with special cases of the problem, but has left the precise complexity characterization open. We begin by establishing a 2EXPTIME lower bound on the MDL/UCQ containment problem, resolving an open problem from the early 1990s. We then present a general approach for getting tighter bounds on the complexity, based on analysis of the number of mappings of queries into tree-like instances. We give two applications of the machinery. First we give an important special case of the MDL/UCQ containment problem that is in co-NEXPTIME, and a case that is in EXPTIME. Second we show that the same technique can be used to get a new tight upper bound for containment of tree automata in UCQs. We provide coding arguments showing that the new MDL/UCQ upper bounds are tight.

Abstract: In this paper, we study boolean (not necessarily positive) combinations of open sets. In other words, we study positive boolean combinations of safety and reachability conditions. We give an algorithm, which inputs a regular language of infinite trees, and decides if the language is a boolean combination of open sets.

Abstract: We define a variant of first-order logic that deals with data words, data trees, data graphs etc. The definition of the logic is based on nominal sets. The key idea is that we allow infinite disjunction, as long as the set of disjuncts is finite modulo renaming of data values. We study model theory for this logic; in particular we prove that the infinite disjunction can be eliminated from formulas.

Abstract: Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in a timed automaton; with "robust", we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete.

Abstract: Theory of tree transducers provides a foundation for understanding expressiveness and complexity of analysis problems for specification languages for transforming hierarchically structured data such as XML documents. We introduce streaming tree transducers as an analyzable, executable, and expressive model for transforming unranked ordered trees (and hedges) in a single pass. Given a linear encoding of the input tree, the transducer makes a single left-to-right pass through the input, and computes the output in linear time using a finite-state control, a visibly pushdown stack, and a finite number of variables that store output chunks that can be combined using the operations of string-concatenation and tree-insertion. We prove that the expressiveness of the model coincides with transductions definable using monadic second-order logic (MSO). Existing models of tree transducers either cannot implement all MSO-definable transformations, or require regular look ahead that prohibits single-pass implementation. We show a variety of analysis problems such as type-checking and checking functional equivalence are decidable for our model.

Abstract: We study algebraic synchronization trees, i.e., initial solutions of algebraic recursion schemes over the continuous categorical algebra of synchronization trees. In particular, we investigate the relative expressive power of algebraic recursion schemes over two signatures, which are based on those for Basic CCS and Basic Process Algebra, as a means for defining synchronization trees up to isomorphism as well as modulo bisimilarity and language equivalence. The expressiveness of algebraic recursion schemes is also compared to that of the low classes in the Caucal hierarchy.

Abstract: We introduce a natural extension of collapsible pushdown systems called annotated pushdown systems that replaces collapse links with stack annotations. We believe this new model has many advantages. We present a saturation method for global backwards reachability analysis of these models that can also be used to analyse collapsible pushdown systems. Beginning with an automaton representing a set of configurations, we build an automaton accepting all configurations that can reach this set. We also improve upon previous saturation techniques for higher-order pushdown systems by significantly reducing the size of the automaton constructed and simplifying the algorithm and proofs.

Abstract: We consider the problem of computing the value and an optimal strategy for minimizing the expected termination time in one-counter Markov decision processes. Since the value may be irrational and an optimal strategy may be rather complicated, we concentrate on the problems of approximating the value up to a given error eps > 0 and computing a finite representation of an eps-optimal strategy. We show that these problems are solvable in exponential time for a given configuration, and we also show that they are computationally hard in the sense that a polynomial-time approximation algorithm cannot exist unless P=NP.

Abstract: We extend the theory of Cellular Automata to arbitrary, time-varying graphs.

Abstract: This paper introduces an abstract notion of fragments of monadic second-order logic. This concept is based on purely syntactic closure properties. We show that over finite words, every logical fragment defines a lattice of languages with certain closure properties. Among these closure properties are residuals and inverse C-morphisms. Here, depending on certain closure properties of the fragment, C is the family of arbitrary, non-erasing, length-preserving, length-multiplying, or length-reducing morphisms. In particular, definability in a certain fragment can often be characterized in terms of the syntactic morphism. This work extends a result of Straubing in which he investigated certain restrictions of first-order logic formulae. In contrast to Straubing's model-theoretic approach, our notion of a logical fragment is purely syntactic and it does not rely on Ehrenfeucht-Fraisse games. As motivating examples, we present (1) a fragment which captures the stutter-invariant part of piecewise-testable languages and (2) an acyclic fragment of Sigma_2. As it turns out, the latter has the same expressive power as two-variable first-order logic FO^2.

Abstract: We define a general framework for formulating model-comparison games. This framework, which we call partition games, includes as special cases the pebble games for finite-variable logics and finite-variable logics with counting. We introduce two new pebble games that are obtained by imposing linear-algebraic conditions on the moves in a partition game. The first of these, called the matrix-equivalence game, characterises equivalence in the finite-variable fragments of matrix-rank logic. The second, called the invertible-map game, yields a refinement of the equivalence defined by the matrix-equivalence game and we show that this game equivalence is polynomial-time decidable. This yields a family of polynomial-time approximations of graph isomorphism that is strictly stronger than the Weisfeiler-Lehman method.

Abstract: We introduce a variant of nominal sets that is well-suited for languages recognized by timed automata. We state and prove a machine-independent characterization of languages recognized by deterministic timed automata. Finally, in the setting of nominal sets we define a class of automata, called timed register automata, that extends timed automata and is effectively closed under minimization.

Abstract: We present a full classification of decidable and undecidable cases for contextual equivalence in a finitary ML-like language equipped with full ground storage (both integers and reference names can be stored). The simplest undecidable type is unit -> unit -> unit. At the technical level, our results marry game semantics with automata-theoretic techniques developed to handle infinite alphabets. On the automata-theoretic front, we show decidability of the emptiness problem for register pushdown automata extended with fresh-symbol generation.

Abstract: We study generalised polynomial functors between presheaf categories, developing their mathematical theory together with computational applications. The main theoretical contribution is the introduction of discrete generalised polynomial functors, a class that lies in between the classes of cocontinuous and finitary functors, and is closed under composition, sums, finite products, and differentiation. A variety of concrete applications are given: to the theory of nominal algebraic effects; to the algebraic modelling of languages, and equational theories there of, with variable binding and polymorphism; and to the synthesis of dependent zippers.

Abstract: We present a new, self-contained proof of the limitedness problem. The key novelty is a description using profinite words, which unifies and simplifies the previous approaches, and seamlessly extends the theory of regular languages. We also define a logic over profinite words, called MSO+inf and show that the satisfiability problem of MSO+B reduces to the satisfiability problem of our logic.

Abstract: We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for two natural classes of such logics. Moreover, we show that an entirely general completeness result is not possible. We study the expressive power of our language, contrasting it with both coalgebraic modal logic and existing first-order proposals for special classes of Set-coalgebras (apart for relational structures, also neighbourhood frames and topological spaces). The semantic characterization of expressivity is based on the fact that our language inherits a coalgebraic variant of the Van Benthem-Rosen Theorem. Basic modeltheoretic constructions and results, in particular ultraproducts, obtain for the two classes which allow completeness—and in some cases beyond that.

Abstract: This paper presents a nine-rule *language-independent* proof system that takes an operational semantics as axioms and derives program properties, including ones corresponding to Hoare triples. This eliminates the need for language-specific Hoare-style proof rules in order to verify programs, and, implicitly, the tedious step of proving such proof rules sound for each language separately. The key proof rule is *Circularity*, which is coinductive in nature and allows for reasoning about constructs with repetitive behaviors (e.g., loops). The generic proof system is shown sound and has been implemented in the MatchC program verifier.

Abstract: We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. Completion of rewriting systems with binders is a notably difficult problem; the completion procedure presented in this paper is the first to deal with binders in rewrite rules.

Abstract: We introduce two natural variants of prefix rewriting on nested-words. One captures precisely the transition graphs of order-$2$ pushdown automata and the other precisely those of order-$2$ collapsible pushdown automata ($2$-CPDA). To our knowledge this is the first precise `external' characterisation of $2$-CPDA graphs and demonstrates that the class is robust and hence interesting in its own right. The comparison with our characterisation for $2$-PDA graphs also gives an idea of what `collapse means' in terms outside of higher-order automata theory. Additionally, a related construction gives us a decidability result for first-order logic on a natural subclass of $3$-CPDA graphs, which in some sense is optimal.

Abstract: Kolaitis and Kopparty have shown that for any first-order formula with parity quantifiers over the language of graphs there is a family of multi-variate polynomials of constant-degree that agree with the formula on all but a $2^{-\Omega(n)}$-fraction of the graphs with $n$ vertices. The proof of this result yields a bound on the degree of the polynomials that is a tower of exponentials of height as large as the nesting depth of parity quantifiers in the formula. We show that this tower-type dependence on the depth of the formula is necessary. We build a family of formulas of depth $q$ whose approximating polynomials must have degree bounded from below by a tower of exponentials of height proportional to $q$. Our proof has two main parts. First, we adapt and extend known results describing the joint distribution of the parity of the number of copies of small subgraphs on a random graph to the setting of graphs of growing size. Secondly, we analyse a variant of Karp's graph canonical labelling algorithm and exploit its massive parallelism to get a formula of low depth that defines an almost canonical pre-order on a random graph.

Abstract: In this paper, we present a new model of class-based Algol-like programming languages inspired by automata-theoretic concepts. The model may be seen as a variant of the "object-based" model previously proposed by Reddy, where objects are described by their observable behaviour in terms of events. At the same time, it also reflects the intuitions behind state-based models studied by Reynolds, Oles, Tennent and O'Hearn where the effect of commands is described by state transformations. The idea is to view stores as automata, capturing not only their states but also the allowed state transformations. In this fashion, we are able to combine both the state-based and event-based views of objects. We illustrate the efficacy of the model by proving several test equivalences and discuss its connections to the previous models.