
List of accepted papers
(In order of appearance)
Track B: Logic, Semantics and Theory of Programming
 Modular Algorithms for Heterogeneous Modal Logics
 Lutz Schröder and Dirk Pattinson

Statebased systems and modal logics for reasoning about them often
heterogeneously combine a number of features such as nondeterminism 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 statebased systems as multisorted 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.
 CoLogic 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 cologic
programming (coLP for brevity), a paradigm that combines both
inductive and coinductive logic programming. CoLP 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. CoLP has applications to rational trees, verifying
infinitary properties, lazy evaluation, concurrent LP, model checking,
bisimilarity proofs, etc.
 Maximal InfiniteValued 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 wellestablished 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 onetoone
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 fixedpoint 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
firstorder formulae, we here obtain a decidability result for the
boundedness issue for monadic fixed points over arbitrary firstorder
formulae in restriction to acyclic structures.
 Equational Systems and Free Constructions
 Marcelo Fiore and ChungKil 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 namepassing 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 bottomup 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 tracesets of programs and contexts may be viewed as deterministic
strategies and counterstrategies 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 traceset of a configuration of that type.
 Aliased Register Allocation for Straightline Programs is NPComplete
 Jonathan K. Lee, Jens Palsberg and Fernando Magno Quintão Pereira

Register allocation is NPcomplete in general but can be solved in
linear time for straightline 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 commonlyused architectures such as x86, the
HP PARISC, 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
lowaddress 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 straightline programs is
NPcomplete.
 Conservative Ambiguity Detection in ContextFree Grammars
 Sylvain Schmitz

The ability to detect ambiguities in contextfree 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 2Label 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 twolabel 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
tracebased lower part of van Glabbeek's lineartime, branchingtime
spectrum and its simulationbased 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 (CSPstyle) 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 GoubaultLarrecq

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 nondeterministic 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 finitestate automata
recognizing sets of real numbers encoded positionally. It is known
that the sets that are definable in the firstorder 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 wellknown Cobham's theorem on the
finitestate 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.
 MinimumTime Reachability in Timed Games
 Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu and JeanFrançois Raskin

We consider the minimumtime reachability problem
in concurrent twoplayer 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
nontrivial extension of the clockregion equivalence
relation for timed automata.
 ReachabilityTime Games on Timed Automata
 Marcin Jurdziński and Ashutosh Trivedi

In a reachabilitytime 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
reachabilitytime games on strongly nonZeno 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 reachabilitytime games on all timed
automata. The exact computational complexity of solving
reachabilitytime games is also established: the problem is
EXPTIMEcomplete 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 firstorder 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 MSOformulas 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
secondorder 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 wellknown 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
mucalculus is as expressive as MSO over finite and infinite nested
words, and the equivalence holds, more generally, for mucalculus 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
lettertoletter 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 firstorder interpretation (with access to the ancestor relation)
and a monadic marking. Using this remark,
we give new characterisations for prefixrecognisable 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 firstorder 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 firstorder
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 FefermanVaught theorem based
on a restriction by formula length necessarily entails a nonelementary
blowup 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 PSPACEcomplete. 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 PSPACEcomplete, 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
PSPACEcomplete.
 On the Complexity of LTL ModelChecking of Recursive State Machines
 Gennaro Parlato and Salvatore La Torre

Recursive state machines (RSMs) are models for
programs with recursive procedural calls. While LTL
modelchecking is EXPTIMEcomplete on such models, on
finitestate machines, it is PSPACEcomplete in general
and becomes NPcomplete for interesting fragments. In
this paper, we systematically study the computational complexity of
modelchecking 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, modelchecking is
in NP. Thus, differently from the full logic, for this
fragment the abstract complexity of modelchecking does not change
moving from finitestate machines to RSMs. Our results on
the other studied fragments confirm this trend, in the sense that,
moving from finitestate machines to RSMs, the complexity
of modelchecking either rises from PSPACEcomplete to
EXPTIMEcomplete, or stays within NP.

