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
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
- 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
- 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
- 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,
stopping priority games a play can be stopped by the environment after a
finite number of stages, however, infinite plays are
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.
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
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
- 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 MITL0,∞,
and prove that the related satisfiability and
model checking (w.r.t. L/U automata) problems are
- 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.