List of accepted papers

(In order of appearance)

• Invited Lectures
• Track A: Algorithms, Automata, Complexity and Games
• Track B: Logic, Semantics and Theory of Programming
• Track C: Security and Foundations of Cryptography

Track B: Logic, Semantics and Theory of Programming

Modular Algorithms for Heterogeneous Modal Logics

Lutz Schröder and Dirk Pattinson

State-based systems and modal logics for reasoning about them often heterogeneously combine a number of features such as non-determinism and probabilities. Here, we show that the combination of features can be reflected algorithmically and develop modular decision procedures for heterogeneous modal logics. The modularity is achieved by formalising the underlying state-based systems as multi-sorted coalgebras and associating both a logical and an algorithmic description to a number of basic building blocks. Our main result is that logics arising as combinations of these building blocks can be decided in polynomial space provided that this is the case for the components. By instantiating the general framework to concrete cases, we obtain PSPACE decision procedures for a wide variety of structurally different logics, describing e.g. Segala systems and games with uncertain information.

Co-Logic Programming: Extending Logic Programming with Coinduction

Luke Simon, Ajay Bansal, Ajay Mallya and Gopal Gupta

In this paper we present the theory and practice of co-logic programming (co-LP for brevity), a paradigm that combines both inductive and coinductive logic programming. Co-LP is a natural generalization of logic programming and coinductive logic programming, which in turn generalizes other extensions of logic programming, such as infinite trees, lazy predicates, and concurrent communicating predicates. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent LP, model checking, bisimilarity proofs, etc.

Maximal Infinite-Valued Constraint Languages

Manuel Bodirsky, Hubie Chen, Jan Kára and Timo von Oertzen

We systematically investigate the computational complexity of constraint satisfaction problems for constraint languages over an infinite domain. In particular, we study a generalization of the well-established notion of maximal constraint languages from finite to infinite domains. If the constraint language can be defined with an ω-categorical structure, then maximal constraint languages are in one-to-one correspondence to minimal oligomorphic clones. Based on this correspondence, we derive general tractability and hardness criteria for the corresponding constraint satisfaction problems.

Affine Systems of Equations and Counting Infinitary Logic

Albert Atserias, Andrei Bulatov and Anuj Dawar

We study the definability of constraint satisfaction problems (CSP) in various fixed-point and infinitary logics. We show that testing the solvability of systems of equations over a finite Abelian group, a tractable CSP that was previously known not to be definable in Datalog, is not definable in an infinitary logic with counting and hence that it is not definable in least fixed point logic or its extension with counting. We relate definability of CSPs to their classification obtained from tame congruence theory of the varieties generated by the algebra of polymorphisms of the template structure. In particular, we show that if this variety admits either the unary or affine type, the corresponding CSP is not definable in the infinitary logic with counting. We also study the complexity of determining whether a CSP omits unary and affine types.

Boundedness of Monadic FO over Acyclic Structures

Stephan Kreutzer, Martin Otto and Nicole Schweikardt

We study the boundedness problem for monadic least fixed points as a decision problem. While this problem is known to be undecidable in general and even for syntactically very restricted classes of underlying first-order formulae, we here obtain a decidability result for the boundedness issue for monadic fixed points over arbitrary first-order formulae in restriction to acyclic structures.

Equational Systems and Free Constructions

Marcelo Fiore and Chung-Kil Hur

The purpose of this paper is threefold: to present a general abstract, yet practical, notion of equational system; to investigate and develop a theory of free constructions for such equational systems; and to illustrate the use of equational systems as needed in modern applications, specifically to the theory of substitution in the presence of variable binding and to models of name-passing process calculi.

Categorical Views on Computations on Trees

Ichiro Hasuo, Bart Jacobs and Tarmo Uustalu

Computations on trees form a classical topic in computing. These computations can be described in terms of machines (typically called tree transducers), or in terms of functions. This paper focuses on three flavors of bottom-up computations, of increasing generality. It brings categorical clarity by identifying a category of tree transducers together with two different behavior functors. The first sends a tree transducer to a coKleisli or biKleisli map (describing the contribution of each local node in an input tree to the global transformation) and the second to a tree function (the global tree transformation). The first behavior functor has an adjoint realization functor, like in Goguen's early work on automata. Further categorical structure, in the form of Hughes's Arrows, appears in properly parameterized versions of these structures.

A Fully Abstract Trace Semantics for General References

James Laird

We describe a fully abstract trace semantics for a functional language with locally declared general references (a fragment of Standard ML). It is based on a bipartite LTS in which states alternate between program and environment configurations and labels carry only (sets of) basic values, location and pointer names. Interaction between programs and environments is either direct (initiating or terminating subprocedures) or indirect (by the overwriting of shared locations): actions reflect this by carrying updates to the shared part of the store.

The trace-sets of programs and contexts may be viewed as deterministic strategies and counter-strategies in the sense of game semantics: we prove soundness of the semantics by showing that the evaluation of a program in an environment tracks the interaction between the corresponding strategies. We establish full abstraction by proving a definability result: every bounded deterministic strategy of a given type is the trace-set of a configuration of that type.

Aliased Register Allocation for Straight-line Programs is NP-Complete

Jonathan K. Lee, Jens Palsberg and Fernando Magno Quintão Pereira

Register allocation is NP-complete in general but can be solved in linear time for straight-line programs where each variable has at most one definition point if the bank of registers is homogeneous. In this paper we study registers which may alias: an aliased register can be used both independently or in combination with an adjacent register. Such registers are found in commonly-used architectures such as x86, the HP PA-RISC, the Sun SPARC processor, and MIPS floating point. In 2004, Smith, Ramsey, and Holloway presented the best algorithm for aliased register allocation so far; their algorithm is based on a heuristic for coloring of general graphs. Most architectures with register aliasing allow only aligned registers to be combined: for example, the low-address register must have an even number. Open until now is the question of whether working with restricted classes of programs can improve the complexity of aliased register allocation with alignment restrictions. In this paper we show that aliased register allocation with alignment restrictions for straight-line programs is NP-complete.

Conservative Ambiguity Detection in Context-Free Grammars

Sylvain Schmitz

The ability to detect ambiguities in context-free grammars is vital for their use in several fields, but the problem is undecidable in the general case. We present a safe, conservative approach, where the approximations cannot result in overlooked ambiguous cases. We analyze the complexity of the verification, and provide formal comparisons with several other ambiguity detection methods.

Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus

Naoki Kobayashi and Takashi Suto

The trace equivalence of BPP was shown to be undecidable by Hirshfeld. We show that the trace equivalence remains undecidable even if the number of labels is restricted to two. The undecidability result holds also for the simulation of two-label BPP processes. These results imply undecidability of some behavioral type systems for the π-calculus.

Ready Simulation for Concurrency: It's Logical!

Gerald Lüttgen and Walter Vogler

This paper provides new insight into the connection between the trace-based lower part of van Glabbeek's linear-time, branching-time spectrum and its simulation-based upper part. We establish that ready simulation is fully abstract with respect to failures inclusion, when adding the conjunction operator that was proposed by the authors in [TCS 373(1–2):19–40] to the standard setting of labelled transition systems with (CSP-style) parallel composition. More precisely, we actually prove a stronger result by considering a coarser relation than failures inclusion, namely a preorder that relates processes with respect to inconsistencies that may arise under conjunctive composition. Ready simulation is also shown to satisfy standard logic properties and thus commends itself for studying mixed operational and logic languages.

Continuous Capacities on Continuous State Spaces

Jean Goubault-Larrecq

We propose axiomatizing some stochastic games, in a continuous state space setting, using continuous belief functions, resp. plausibilities, instead of measures. Then, stochastic games are just variations on continuous Markov chains. We argue that drawing at random along a belief function is the same as letting the probabilistic player P play first, then letting the non-deterministic player C play demonically. The same holds for an angelic C, using plausibilities instead. We then define a simple modal logic, and characterize simulation in terms of formulae of this logic. Finally, we show that (discounted) payoffs are defined and unique, where in the demonic case, P maximizes payoff, while C minimizes it.

A Generalization of Cobham's Theorem to Automata over Real Numbers

Bernard Boigelot and Julien Brusten

This paper studies the expressive power of finite-state automata recognizing sets of real numbers encoded positionally. It is known that the sets that are definable in the first-order additive theory of real and integer variables ⟨R,Z,+,<⟩ can all be recognized by weak deterministic Büchi automata, regardless of the encoding base r>1. In this paper, we prove the reciprocal property, i.e., that a subset of R that is recognizable by weak deterministic automata in every base r>1 is necessarily definable in ⟨R,Z,+,<⟩. This result generalizes to real numbers the well-known Cobham's theorem on the finite-state recognizability of sets of integers. Our proof gives interesting insight into the internal structure of automata recognizing sets of real numbers, which may lead to efficient data structures for handling these sets.

Minimum-Time Reachability in Timed Games

Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu and Jean-François Raskin

We consider the minimum-time reachability problem in concurrent two-player timed automaton game structures. We show how to compute the minimum time needed by a player to reach a target location against all possible choices of the opponent. We do not put any syntactic restriction on the game structure, nor do we require any player to guarantee time divergence. We only require players to use receptive strategies which do not block time. The minimal time is computed in part using a fixpoint expression, which we show can be evaluated on equivalence classes of a non-trivial extension of the clock-region equivalence relation for timed automata.

Reachability-Time Games on Timed Automata

Marcin Jurdziński and Ashutosh Trivedi

In a reachability-time game, players Min and Max choose moves so that the time to reach a final state in a timed automaton is minimised or maximised, respectively. Asarin and Maler showed decidability of reachability-time games on strongly non-Zeno timed automata using a value iteration algorithm. This paper complements their work by providing a strategy improvement algorithm for the problem. It also generalizes their decidability result because the proposed strategy improvement algorithm solves reachability-time games on all timed automata. The exact computational complexity of solving reachability-time games is also established: the problem is EXPTIME-complete for timed automata with at least two clocks.

Perfect Information Stochastic Priority Games

Hugo Gimbert and Wiesław Zielonka

We introduce stochastic priority games — a new class of perfect information stochastic games. These games can take two different, but equivalent, forms. In stopping priority games a play can be stopped by the environment after a finite number of stages, however, infinite plays are also possible. In discounted priority games only infinite plays are possible and the payoff is a linear combination of the classical discount payoff and of a limit payoff evaluating the performance at infinity. Shapley games and parity games are special extreme cases of priority games.

Bounded Depth Data Trees

Henrik Björklund and Mikołaj Bojańczyk

A data tree is a tree where each node has a label from a finite set, and a data value from a possibly infinite set. We consider data trees whose depth is bounded beforehand. By developing an appropriate automaton model, we show that under this assumption various formalisms, including a two variable first-order logic and a subset of XPath, have decidable emptiness problems.

Unranked Tree Automata with Sibling Equalities and Disequalities

Wong Karianto and Christof Löding

We propose an extension of the tree automata with constraints between direct subtrees (Bogaert and Tison, 1992) to unranked trees. Our approach uses MSO-formulas to capture the possibility of comparing unboundedly many direct subtrees. Our main result is that the nonemptiness problem for the deterministic automata, as in the ranked setting, is decidable. Furthermore, we show that the nondeterministic automata are more expressive than the deterministic ones.

Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization

Marcelo Arenas, Pablo Barceló and Leonid Libkin

Nested words are a restriction of the class of visibly pushdown languages that provide a natural model of runs of programs with recursive procedure calls. The usual connection between monadic second-order logic (MSO) and automata extends from words to nested words and gives us a natural notion of regular languages of nested words.

In this paper we look at some well-known aspects of regular languages — their characterization via fixed points, deterministic and alternating automata for them, and synchronization for defining regular relations — and extend them to nested words. We show that mu-calculus is as expressive as MSO over finite and infinite nested words, and the equivalence holds, more generally, for mu-calculus with past modalities evaluated in arbitrary positions in a word, not only in the first position. We introduce the notion of alternating automata for nested words, show that they are as expressive as the usual automata, and also prove that Muller automata can be determinized (unlike in the case of visibly pushdown languages). Finally we look at synchronization over nested words. We show that the usual letter-to-letter synchronization is completely incompatible with nested words (in the sense that even the weakest form of it leads to an undecidable formalism) and present an alternative form of synchronization that gives us decidable notions of regular relations.

A Combinatorial Theorem for Trees

Thomas Colcombet

Following the idea developed by I. Simon in his theorem of Ramseyan factorisation forests, we develop a result of "deterministic factorisations". This extra determinism property makes it usable on trees (finite or infinite).

We apply our result for proving that, over trees, every monadic interpretation is equivalent to the composition of a first-order interpretation (with access to the ancestor relation) and a monadic marking. Using this remark, we give new characterisations for prefix-recognisable structures and for the Caucal hierarchy.

Furthermore, we believe that this approach has other potential applications.

Model Theory Makes Formulas Large

Anuj Dawar, Martin Grohe, Stephan Kreutzer and Nicole Schweikardt

Gaifman's locality theorem states that every first-order sentence is equivalent to a local sentence. We show that there is no elementary bound on the length of the local sentence in terms of the original.

The classical Łoś-Tarski theorem states that every first-order sentence preserved under extensions is equivalent to an existential sentence. We show that there is no elementary bound on the length of the existential sentence in terms of the original. Recently, variants of the Łoś-Tarski theorem have been proved for certain classes of finite structures, among them the class of finite acyclic structures and more generally classes of structures of bounded tree width. Our lower bound also applies to these variants.

We further prove that a version of the Feferman-Vaught theorem based on a restriction by formula length necessarily entails a non-elementary blow-up in formula size.

All these results are based on a similar technique of encoding large numbers by trees of small height in such a way that small formulas can speak about these numbers. Notably, our lower bounds do not apply to restrictions of the results to structures of bounded degree. For such structures, we obtain elementary upper bounds in all cases. However, even there we can prove at least doubly exponential lower bounds.

Decision Problems for Lower/Upper Bound Parametric Timed Automata

Laura Bozzelli and Salvatore La Torre

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as un upper bound. For such automata, we show that checking if for a parameter valuation (resp., all parameter valuations) there is an infinite accepting run is PSPACE-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still PSPACE-complete, if the lower bound parameters are not compared to the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of MITL_0,∞, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are PSPACE-complete.

On the Complexity of LTL Model-Checking of Recursive State Machines

Gennaro Parlato and Salvatore La Torre

Recursive state machines (RSMs) are models for programs with recursive procedural calls. While LTL model-checking is EXPTIME-complete on such models, on finite-state machines, it is PSPACE-complete in general and becomes NP-complete for interesting fragments. In this paper, we systematically study the computational complexity of model-checking RSMs against several syntactic fragments of LTL. Our main result shows that if in the specification we disallow next and until, and retain only the box and diamond operators, model-checking is in NP. Thus, differently from the full logic, for this fragment the abstract complexity of model-checking does not change moving from finite-state machines to RSMs. Our results on the other studied fragments confirm this trend, in the sense that, moving from finite-state machines to RSMs, the complexity of model-checking either rises from PSPACE-complete to EXPTIME-complete, or stays within NP.