Tutorial day: 2 SEPTEMBER

Conference: 3–5 SEPTEMBER

There are no proceedings. You present your best work, be it published elsewhere or yet unpublished.

The conference is three days long. The contributed talks are around ten minutes.

The conference itself will be free and will include most if not all lunches. Paris is easy to reach.

Let's use the conference model that is so successful in other fields, like mathematics.

Registration is open until June 30th, 2014.

09:0009:30
Welcome & Breakfast

09:3012:30
Tutorial

09:3012:30
Tutorial: Semigroups, Automata and Logic

12:3014:30
Lunch

14:3017:00
Tutorial

14:3017:00
Tutorial: Communication Complexity:
New Results and Directions

In this survey talk we will review the basics of communication complexity, and then discuss the following exciting directions from the last few years.

- We will discuss information complexity, its close connection with communication complexity, and many of the important results that have been proven in this area in the last five years.
- New lower bounds on the communication complexity of search problems, and applications including very strong monotone circuit lower bounds, as well as proof complexity lower bounds.
- The last five years has seen some very exciting results in the area of Extended Formulations. It is now known that no linear or semi-definite extended formulation can solve or even approximate many NP-hard problems. Moreover, these lower bounds are tightly connected to a new communication model where the protocol only needs to output the correct value in expectation (over the randomness of the protocol). We will discuss this connection, and survey what is known about lower bounds.

09:0010:00
Invited talk

09:0010:00
Invited talk: Synthesis of Transducers
from Automatic Specifications

Given a specification as a binary relation that relates inputs to admissible outputs, the synthesis problem asks for a program that produces for each input an output that is admissible according to the specification. We consider this problem over the domain of words and trees. The specifications are given by automatic relations, that is, relations that can be defined by finite automata that read pairs of structures and accept those pairs that are in the relation. For such specifications, we study the synthesis problem of deterministic finite state transducers. In particular, we present some recent results and ongoing work on the synthesis of tree transducers.

10:0010:30
Breakfast & coffee

10:3011:45
Session 1

10:3010:42
Automata Techniques for Epistemic
Protocol Synthesis in DEL

In this talk we describe how automata techniques can be applied to problems studied in Dynamic Epistemic Logic, such as epistemic planning. To do so, we first remark that repeatedly executing ad infinitum a propositional event model from an initial epistemic model yields a relational structure that can be finitely represented with automata. This correspondence, together with recent results on uniform strategies, allows us to give an alternative decidability proof of the epistemic planning problem for propositional events, with as by-products accurate upper-bounds on its time complexity, and the possibility to synthesize a finite word automaton that describes the set of all solution plans. In fact, using automata techniques enables us to solve a much more general problem, that we introduce and call epistemic protocol synthesis.

10:4210:54
Meet Your Expectations With
Guarantees: Beyond Worst-Case Synthesis in Quantitative
Games

Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. We consider mean-payoff and shortest path settings. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.

This talk is based on a joint paper with Véronique Bruyère, Emmanuel Filiot and Jean-François Raskin, published in STACS 2014 [BFRR14]. An extended version can be found on arXiv [BFRR13].

- [BFRR13]
- V. Bruyère, E. Filiot, M. Randour, and J.-F. Raskin. Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. CoRR, abs/1309.5439, 2013
- [BFRR14]
- V. Bruyère, E. Filiot, M. Randour, and J.-F. Raskin. Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. In Proc. of STACS, volume 25 of LIPIcs, pages 199–213. Schloss Dagstuhl - LZI, 2014.

10:5411:06
Petri Games: Synthesis of Distributed
Systems with Causal Memory

We present Petri games as a new foundation for the synthesis of distributed systems. The players of a Petri game are tokens on a Petri net. Petri games differ from the standard Pnueli/Rosner model for distributed synthesis, which is based on the notion of partial observability, i.e., the strategy of each process of the implementation may only depend on a subset of the system variables. Synthesis under the Pnueli/Rosner model is only decidable for restricted system architectures like pipelines and rings. Instead of partial observation, Petri games are based on causality. This change leads to new decidability results and algorithms for the synthesis of distributed systems.

11:0611:18
First-Order Definable String
Transformations

The connection between languages defined by computational models and logic for languages is well-studied. Monadic second-order logic and finite automata are shown to closely correspond to each-other for the languages of strings, trees, and partial-orders. Similar connection are shown for first-order logic and finite automata with certain aperiodicity restriction. Courcelle in 1994 proposed a way to use logic to define functions over structures where the output structure is defined using logical formulas interpreted over the input structure. Engelfriet and Hoogeboom discovered the corresponding "automata connection" by showing that two-way generalised sequential machines capture the class of monadic-second order definable transformations. Alur and Cerny further refined the result by proposing a one-way deterministic transducer model with string variables—called the streaming string transducers—to capture the same class of transformations.

In this paper we establish a transducer-logic correspondence for Courcelle's first-order definable string transformations. We propose a new notion of transition monoid for streaming string transducers that involves structural properties of both underlying input automata and variable dependencies. By putting an aperiodicity restriction on the transition monoids, we define a class of streaming string transducers that captures exactly the class of first-order definable transformations.

11:1811:30
Decomposition of *k*-valued
Streaming String Transducers

We
present a decomposition for a particular class of *k*-valued streaming
string transducers. This decomposition allows us to prove that the
equivalence problem for this particular class of transducers is
decidable.

This is joint work with Anca Muscholl.

11:3011:42
Coinduction-up-to

Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. The use of such techniques dates back to Milner's initial work on bisimilarity. Since then, coinduction up-to proved useful, if not essential, in numerous proofs about concurrent systems; it has been used to obtain decidability results, and more recently to improve standard automata algorithms.

We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modelled as coalgebras. By tuning the parameters of our framework, we obtain novel techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.

This is joint work with Filippo Bonchi, Daniela Petrisan and Damien Pous.

11:4512:00
Break

12:0013:00
Session 2A

12:0012:12
Turing Machines with Atoms and
Constraint Satisfaction Problems

We study deterministic computability over sets with atoms. We characterize those alphabets for which Turing machines with atoms determinize. To this end, the determinization problem is expressed as a Constraint Satisfaction Problem, and a characterization is obtained from deep results in CSP theory.

This is joint work with Bartek Klin, Sławomir Lasota and Szymon Toruńczyk.

12:1212:24
Descriptive Complexity and Constraint
Satisfaction Problems

We give a common generalization of two theorems from Descriptive Complexity:

- the Immerman-Vardi Theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and
- the Cai-Fürer-Immerman Theorem, which says that over all finite structures, the logic LFP+C does not capture PTime.

Our generalization relies on a connection with Constraint Satisfaction Problems and recent results from CSP theory.

The presented results are a consequence of the results presented in the previous talk by Joanna Ochremiak. Both talks are based on a joint paper with Bartek Klin, Sławomir Lasota and Joanna Ochremiak accepted to CSL-LICS 2014.

12:2412:36
LOIS: a Practical C++ Library for
Handling Infinite Sets

We present a C++ library allowing computation over infinite sets. The programmer is able to represent infinite sets in finite memory, as well as loop over them in finite time. The elements of these sets can be elements from some—usually infinite—structure, as well as integers, pairs, tuples, and infinite sets of elements. For example, our library allows writing a program which proves that the random bipartite graph (take an infinite bipartite graph and choose each edge with probability ½) is connected and has diameter 3 in a very natural way, as one would normally write breadth first search on a finite graph.

Such an approach has
applications in automata theory. For example, the set of
states of Kaminski and Francez's register automata on data
words can be viewed as disjoint unions of sets of form
*A ^{k}*, where

In theory, the system could be extended to work with any underlying structure, as long as its first order theory is decidable, and the iteration/recursion depth is bounded in the given program; currently, dense order, infinite random graph, and random tree theories are implemented.

12:3612:48
Choiceless Polynomial Time on
Structures with Small Abelian Colour Classes

Choiceless Polynomial Time (CPT) is one of the candidates in the quest for a logic for polynomial time. It is a strict extension of fixed-point logic with counting (FPC) but to date it is unknown whether it expresses all polynomial-time properties of finite structures.

We
study the CPT-definability of the isomorphism problem for
relational structures of bounded colour class size
*q* (for short, *q*-bounded structures). Our main
result gives a positive answer, and even CPT-definable
canonisation procedures, for classes of *q*-bounded
structures with small Abelian groups on the colour
classes. Such classes of *q*-bounded structures with Abelian
colours naturally arise in many contexts. For instance,
2-bounded structures have Abelian colours which shows that
CPT captures PTIME on 2-bounded structures. In particular,
this shows that the isomorphism problem of multipedes is
definable in CPT, an open question posed by Blass,
Gurevich, and Shelah.

12:4813:00
Interpretation Logic: an Alternative
Characterisation of Choiceless Polynomial Time

We introduce a characterisation of Choiceless Polynomial Time based on first-order interpretations. Choiceless Polynomial Time with counting (introduced by Blass, Gurevich and Shelah) succeeds to define several queries that separate other logics from PTIME (e.g. the Cai-Fürer-Immerman query) and is thus an interesting candidate for a logic capturing PTIME. Originally, Choiceless Polynomial Time has been formalised as a machine model operating on structures by means of set-theoretic operations, especially creation of hereditarily finite sets. Despite the benefits of viewing the logic as a machine model, this makes it less accessible to model theoretic techniques.

Computations in Choiceless Polymomial Time primarily define new relations over hereditarily finite sets. This closely resembles the process of updating relations with first-order interpretations, which suggests a characterisation with iterated first-order interpretations. Representing Choiceless Polynomial Time on the basis of first-order logic not only allows for a more concise definition, it also permits analysis using tools of finite model theory. Moreover, our characterisation makes it easy to define natural fragments of our logic and hence of Choiceless Polynomial Time. A characterisation of these fragments may, in turn, give useful insights into the expressibility of Choiceless Polynomial Time itself.

We formalise the idea of iterated first-order interpretations with appropriate polynomial time and space constraints to create Interpretation Logic, a logic that is equivalent to Choiceless Polynomial Time. The main principle of Interpretation Logic is to iterate the application of a first-order interpretation to the input structure, where the halting condition and evaluation are given in first-order logic as well. In order to obtain a representation of the extension of Choiceless Polynomial Time by the counting operation, we show that it suffices to equip our logic with an equicardinality operation, namely, the Härtig quantifier. More precisely, we show that Choiceless Polynomial Time with counting can already be simulated by the extension of Choiceless Polynomial Time by an equicardinality operator. This is possible because Choiceless Polynomial Time programs have access to operations on hereditarily finite sets and thus on finite ordinals.

Our main result is the equivalence of this extension of first-order logic by the equicardinality operation and the extension of Interpretation Logic by the Härtig quantifier, where the simulation requires representation of higher-order objects in the interpreted structures as well as a correspondence between different measures of space complexity.

12:0013:00
Session 2B

12:0012:12
Games on Graphs with Robust
Multidimensional Mean-Payoff Objectives

Two-player
games on graphs provide the mathematical foundation for
the study of reactive systems. In the quantitative
framework, an objective assigns a value to every play, and
the goal of Player 1 is to minimize the value of the
objective. In this framework, there are two relevant
synthesis problems to consider: the quantitative analysis
problem is to compute the minimal (or infimum) value that
Player 1 can assure, and the boolean analysis problem asks
whether Player 1 can assure that the value of the
objective is at most ν (for a given threshold
ν). Mean-payoff expression games are played on a
multidimensional weighted graph. An atomic mean-payoff
expression objective is the mean-payoff value (the
long-run average weight) of a certain dimension, and the
class of mean-payoff expressions is the closure of atomic
mean-payoff expressions under the algebraic operations of
*max*, *min*, numerical complement and
*sum*.

In this work, we study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with mean-payoff expression objectives. While in general, optimal strategies for these games require infinite-memory, in synthesis we are typically interested in the construction of a finite-state system. Hence, we consider games in which Player 1 is restricted to finite-memory strategies, and our main contribution is as follows. We prove that for mean-payoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is inter-reducible with Hilbert's tenth problem over rationals—a fundamental long-standing open problem in computer science and mathematics. We also show that when both players may play with infinite memory both problems become undecidable.

12:1212:24
Secure Equilibria in Weighted
Games

We consider two-player non zero-sum infinite duration games played on weighted graphs. We extend the notion of secure equilibrium introduced by Chatterjee et al., from the Boolean setting to this quantitative setting. As for the Boolean setting, our notion of secure equilibrium refines the classical notion of Nash equilibrium. We prove that secure equilibria always exist in a large class of weighted games which includes common measures like sup, inf, lim sup, lim inf, mean-payoff, and discounted sum. Moreover we show that it is possible to synthesize such strategy profiles that are finite-memory and use few memory. Finally, we prove that the constrained existence problem for secure equilibria is decidable for sup, inf, lim sup, lim inf and mean-payoff measures. Our solutions rely on new results for zero-sum quantitative games with lexicographic objectives that are interesting on their own right.

12:2412:36
Two-Player Perfect-Information
Shift-Invariant Submixing Stochastic Games are
Half-Positional

The object of study are two-player
stochastic games with perfect information and infinite duration,
the property of these games that we study is positionality, namely
the question: when can one player play optimally without memory
and without a source of random bits? We give a sufficient
condition on the payoff function to achieve half-positionality
(Player 1 can play optimally with a positional strategy). The
condition is that the payoff function should be *shift-invariant*
and *submixing*. In [2] it is shown that one-player stochastic
games with shift-invariant and submixing payoff functions are
positional, and in [3] the *half-positionality* of *deterministic*
two-player games with shift-invariant and submixing payoff
functions is demonstrated. We extend these two results to
half-positionality of *two*-player *stochastic*
games.

In the way of proving our main result we also show that for all ε > 0, given that the payoff function is shift-invariant, both players have ε-subgame perfect strategies, i.e. strategies that are ε-optimal not only from the beginning of the game but also for any finite play already played.

The submixing and shift-invariant payoff functions form a class that is large enough to have the half-positionality of games equipped the following well-known payoff functions follow easily from our main result:

- mean-payoff:
- each state is labeled by some reward, and the payoff function computes the average accumulated reward.
- discounted payoff:
- each state is labeled by some immediate reward and a discount factor and the payoff function measures the long-term performance with an inflation rate
- parity condition:
- states are labeled by integers, Player 1 wins if the largest integer seen infinitely often is odd
- limsup (liminf) payoff:
- states are labeled by rewards, and the payoff function computes the limsup (liminf) of the rewards.

The (half)-positionality of games equipped with the payoff functions above have been shown by numerous authors, using different techniques. A unified proof is a consequence of our main result.

Given a payoff function such that every one-player
stochastic game equipped with it is positional does *not* imply
that the two-player game is half-positional. We provide an
example that proves this.

- Gimbert, Hugo, and Edon Kelmendi. "Two-Player Perfect-Information Shift-Invariant Submixing Stochastic Games Are Half-Positional." arXiv preprint arXiv:1401.6575 (2014).
- Gimbert, Hugo. "Pure stationary optimal strategies in Markov decision processes." STACS 2007. Springer Berlin Heidelberg, 2007. 200-211.
- Kopczyński, Eryk. "Half-positional determinacy of infinite games." Automata, Languages and Programming. Springer Berlin Heidelberg, 2006. 336-347.

12:3612:48
Reachability Payoff Games

Reachability payoff games are two-player zero-sum games played on directed graphs with weights on edges, where two players take turns to choose transitions in order to optimize the total cost to reach a target set of vertices. More precisely, Player 1 wants to reach the target by minimizing its cost, whereas Player 2 wants to avoid the target, or, if not possible, maximize the cost of Player 1. When weights of edges are non-negative, polynomial algorithms are known in order to compute optimal values as well as optimal strategies for both players, see, e.g., an adaptation of Dijkstra's shortest path algorithm by Khachiyan et al. Moreover, both players are known to have optimal memoryless strategies. The case where weights can be any integer is more complex, especially in the presence of negative cycles. Filiot, Gentilini and Raskin prove that deciding whether the value of such a game is positive can be done in NP ∩ co-NP, by using methods similar to the one used for mean-payoff games: this holds even though optimal strategies may require memory, contrary to the nonnegative case.

Our contribution is threefold. First, we present a value iteration algorithm to compute the optimal values, as well as optimal strategies for both players when they exist. This iterative algorithm has a pseudo-polynomial complexity (i.e., polynomial if weights of edges are encoded in unary). We also show that Player 2 always has optimal memoryless strategies and that a memory of size pseudo-polynomial is sufficient (and sometimes necessary) for Player 1. Finally, we present a value-iteration algorithm for total-payoff games (without reachability) using a pseudo-polynomial reduction to reachability Total Payoff games.

12:4813:00
Adding Negative Prices to Priced Timed
Games

Priced timed games (PTGs) are two-player zero-sum games played on the infinite graph of configurations of priced timed automata where two players take turns to choose transitions in order to optimize cost to reach target states. Bouyer et al. and Alur, Bernadsky, and Madhusudan independently proposed algorithms to solve PTGs with non-negative prices under certain divergence restriction over prices. Brihaye, Bruyère, and Raskin later provided a justification for such a restriction by showing the undecidability of the optimal strategy synthesis problem in the absence of this divergence restriction. This problem for PTGs with one clock has long been conjectured to be in polynomial time, however the current best known algorithm, by Hansen, Ibsen-Jensen, and Miltersen, is exponential. We extend this picture by studying PTGs with both negative and positive prices. We refine the undecidability results for optimal strategy synthesis problem, and show undecidability for several variants of optimal reachability cost objectives including reachability cost, time-bounded reachability cost, and repeated reachability cost objectives. We also identify a subclass with bi-valued price-rates and give a pseudo-polynomial (polynomial when prices are nonnegative) algorithm to partially answer the conjecture on the complexity of one-clock PTGs.

13:0014:30
Lunch

14:3015:30
Invited talk

14:3015:30
Invited talk: A Lambda Approach

Turing machines and lambda-calculus were the first two approaches to define computability. In verification the Turing machine approach is predominant: finite automata, counter machines, pushdown automata, multi-pushdown automata, etc. Typing disciplines are another approach to program correctness. Rich types can express a variety of program properties, as for example that a list is sorted, or that resources are accessed. In typing disciplines the lambda approach is paramount. The perspectives of verification and typing are different. One seldom types a pushdown automaton; similarly it is not yet common to consider lambda terms as machines. In this talk we argue that the latter is not only quite natural, but also useful.

Simply typed lambda-calculus with fixpoints is an abstraction of higher-order functional programs. It faithfully models the control in such programs but abstracts from data: all constants are non-interpreted. In particular, terms of this calculus can encode finite automata so that an evaluation of a term gives the behaviour of the automaton it encodes (a regular tree). In a similar way terms can encode pushdown automata.

Lambda-calculus comes with its methods of evaluation that do not rely on pushdowns. This gives a new perspective on the so called pushdown hierarchy: automata with higher-order stacks. For example, Muchnik's theorem stating the compatibility of some graph unfoldings with MSOL finds a new explanation in this context. Lambda-calculus has a richer syntax that allows naturally to talk about contexts, multi-contexts, higher-order contexts etc. Lambda-calculus comes with models that make it possible to understand better the invariants of computation. In summary, simply typed lambda-calculus with recursion offers new questions that, also for reasons of perspective, were not considered by the typing community.

15:3015:45
Coffee Break

15:4517:00
Session 3

15:4515:57
How Many Numbers Can a Lambda-term
Contain?

It
is well known that simply-typed lambda-terms can be
used to represent natural numbers, as well as some
other data types. Of course there exist higher-order
functions containing arbitrarily many numbers, like *g*(*f*) = *n*_{1} + *f*(*n*_{2} + *f*(*n*_{3} + *f*(⋯ + *f*(*n*_{k})⋯))). If we want to know precisely the result of our function *g* for each *f*, we need to remember each *n*_{1},…,*n*_{k} separately. If, however, we allow approximation of the result up to some error, the situation changes dramatically.

In this paper we consider the domination-equivalence relation, widely used e.g. in the context of regular cost functions:
two functions are *domination-equivalent* if for each set of arguments *X*, one function is bounded if and only if the second function is bounded.
We prove that, modulo this equivalence relation, for each type there exist only finitely many shapes

of functions, and for each of them we need to specify only a fixed number of constants appearing in the function. For example, our function *g*, assuming that all *n*_{1},…,*n*_{k} are positive, is equivalent to *g*'(*f*) = *n*_{1} + *f*(*m*), where *m* = *n*_{2}+⋯+*n*_{k}.

As a consequence, we obtain a result concerning representation of tuples in lambda-terms. We know that pairs or tuples of natural numbers can be represented in lambda-terms. Notice, however, that, in the standard implementation, the type of terms representing *k*-tuples of numbers depends on *k*. From our result it follows that, indeed, in a lambda-term of a fixed type we can store only a fixed number of natural numbers, in such a way that they can be extracted using lambda-terms. Moreover, the same result holds when we allow that the numbers can be extracted approximately, up to some error (even when we only want to know whether a set is bounded or not).

Our results hold as well when we consider the lambda-Y-calculus, that is when we add the Y combinator to our syntax, introducing infinite recursion.

15:5716:09
Böhm Trees as Higher-Order Recursive
Schemes

Higher-order recursive schemes (HORS) are schematic
representations of functional programs. They generate possibly
infinite ranked labelled trees and, in that respect, are known to be
equivalent to a restricted fragment of the λ*Y*-calculus,
consisting of ground-type terms whose free variables have types
of the form *o* → ... → *o* (with *o* as a special
case).

In this paper, we show that any λ*Y*-term
(with no restrictions on term type or the types of free
variables) can actually be represented by a HORS. That is, for
any λ*Y*-term *M*, there exists a HORS generating a tree that
faithfully represents *M*'s Böhm tree. In particular, the HORS
captures higher-order binding information contained in the Böhm
tree. An analogous result holds for finitary PCF.

As a consequence, we can reduce a variety of
problems related to the λ*Y*-calculus or finitary PCF to
problems concerning higher-order recursive schemes. For instance,
Böhm tree equivalence can be reduced to the equivalence problem
for HORS. Our results also enable MSO model-checking of Böhm
trees.

16:0916:21
Reachability in Pushdown Register
Automata

We
investigate reachability in pushdown automata over
infinite alphabets: machines with finite control, a finite
collection of registers and pushdown stack. First we show
that, despite the stack's unbounded storage capacity, in
terms of reachability/emptiness these machines can be
faithfully represented by using only 3*r* elements of
the infinite alphabet, where *r* is the number of
registers. Moreover, this bound is tight. Next we settle
the complexity of the associated reachability/emptiness
problems. In contrast to register automata, where
differences in register storage policies gave rise to
differing complexity bounds, the emptiness problem for
pushdown register automata is EXPTIME-complete in all
cases. We also provide a solution to the global
reachability problem, based on representing pushdown
configurations with a special register automaton. Finally,
we examine extensions of pushdown storage to higher orders
and show that reachability is undecidable already at order
2, unlike in the finite alphabet case.

Joint work with Andrzej Murawski and Steven Ramsay. Full paper to appear in MFCS'14.

16:2116:33
Rewriting Higher-Order Stack Trees

Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph. We unify both models by introducing the notion of stack trees, whose nodes are labelled by higher-order stacks, and define the corresponding class of higher-order closed tree rewriting systems. These graphs retain the decidability properties of ground tree rewriting graphs while generalising the pushdown hierarchy of graphs.

16:3316:45
Senescent Ground Tree Rewrite
Systems

Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scope-bounded multi-stack pushdown systems, we show — via reductions to and from reset Petri-nets — that these systems have an Ackermann-complete control state reachability problem. However, reachability of a regular set of trees remains undecidable.

This work is to appear in CSL-LICS 2014.

16:4516:57
Decidability of the Weak Bruhat
Ordering on Permutations via MSOL and S1S

We prove that the equational theory of all the permutohedra is decidable.

17:0017:15
Break

17:1518:15
Session 4

17:1517:27
Going Higher in the First-order
Quantifier Alternation Hierarchy on Words

I will present new results on the
quantifier alternation hierarchy in first-order logic on finite
words. Levels in this hierarchy are defined by counting the
number of quantifier alternations in formulas. A famous open
problem in formal language theory is to find
*decidable characterizations* for every level. That is an
algorithm which, given as input a regular language, decides it
can be expressed by a formula of the level in
question.

For a long time this problem has been open for
every level above level 3/2 (formulas having only 1
alternation). In the talk, I will present techniques for
obtaining decidable characterizations for levels 2 (boolean
combinations of formulas having only 1 alternation) and
5/2 (formulas having 2 alternations). The techniques work by
considering a deeper problem, called *separation*, which, once
solved for lower levels, allows to obtain decidable
characterizations for higher levels.

17:2717:39
Separability of Context-Free Languages
by Piecewise Testable Languages

Language
*S* separates languages *K* and *L* if
*S* contains *K* and has empty an intersection
with *L*. We show the decidability of the following
question: given two context-free languages, does
there exists a piecewise testable language which
separates them?

It is known that separating context-free languages is undecidable for all classes containing definite languages. Therefore the class of piecewise testable languages seems to be the first nontrivial class of languages for which the above problem is decidable.

17:3917:51
Adding Modular Predicates

The
decision problem for a given class of regular languages
consists in deciding, given a regular language, whether or
not it belongs to this class. Solving the decision problem
for various fragments of monadic second order is a
well-studied problem on regular languages. Fragments of
logic are usually defined in terms of their quantifier
complexity (Σ_{n}-classes) or number of
variables allowed in the formulae. Another possible
parameter is to impose restrictions on the
numerical predicates in the
signature. There are essentially three basic
groups of such predicates: the linear order, the local
predicates LOC and the modular predicates
MOD. In this talk, we will presents generic
algorithmic procedure for the enrichement of a fragment by
modular predicates, depending on algebraic assumptions on
the initial fragment.

17:5118:03
A New Tool to Study the Order Problem
in Groups Generated by Invertible-Reversible
Automata

We develop a new tool, called the orbit automaton, to study the order problem in (semi)groups generated by finite invertible-reversible Mealy automata. The technique is based on studying the underlying orbit tree of the action of a group on a tree. We show that for some groups, where all other known methods fail, it allows us to prove the existence of elements of infinite order.

18:0318:15
The Equational Theory of Aperiodic
Semigroups is Decidable in Exponential Time

Due to a result by McCammond (Int. J. Algebra Comput. 2001) it is decidable whether all aperiodic semigroups satisfy some given identity of ω-terms. The respective decision procedure works by computing normal forms, but unfortunately neither its worst-case running time nor the maximal size of the intermediate terms have been estimated. We pursue a different approach and solve the same problem by means of first-order definability of regular languages and an infinite Ehrenfeucht-Fraïssé game on ω-terms. In this way, we obtain an algorithm which decides whether a given identity of ω-terms holds in all aperiodic semigroups and whose running time is exponential in the size of the ω-terms. This result was obtained in the course of developing a framework which allows for separating the bookkeeping involved in winning strategies for Ehrenfeucht-Fraïssé games on finite words from the actual strategy.

09:0010:00
Invited talk

09:0010:00
Invited talk: Communication Cost in
Parallel Query Processing

Fix
a full, conjunctive query, and consider the following
problem: what is the amount of communication required to
compute the query in parallel on *p* servers, over a
large database instance? We define the Massively Parallel
Communication (MPC) model, where the computation proceeds
in rounds consisting of local computations followed by a
global reshuffling of the data. Servers have unlimited
computational power and are allowed to exchange any data,
the only cost parameters are the number of rounds and the
maximum amount of communication per server. There is a
tradeoff between these two parameters. I will describe
tight bounds on the amount of communication for the case
of a single round, expressed in terms of a fractional edge
packing of the query expression, and will given some
weaker results for multi-round algorithms. Both these
settings assume data with no skew. Finally, I will
briefly discuss the single round, skewed-data case.

Joint work with Paul Beame and Paris Koutris.

10:0010:30
Breakfast & coffee

10:3011:45
Session 5

10:3010:42
MSO Queries on Trees: Enumerating
Answers under Updates

We
investigate efficient view maintenance for MSO-definable
queries over trees or, more precisely, efficient
enumeration of answers to MSO-definable queries over words
and trees which are subject to local updates. For words we
exhibit an algorithm that uses an *O*(*n*)
preprocessing phase and enumerates answers with
*O*(log *n*) delay between them. When the word
is updated, the algorithm can avoid repeating expensive
preprocessing and restart the enumeration phase within
*O*(log *n*) time. For trees, our algorithm uses
*O*(*n*) preprocessing time, enumerates answers
with *O*(log^{2} *n*) delay, and can
restart enumeration within *O*(log^{2}
*n*) time after receiving an update to the tree. This
significantly improves the cost of recomputing the answers
of a query from scratch. Our algorithms and complexity
results in the paper are presented in terms of
node-selecting automata representing the MSO
queries.

10:4210:54
Query Determinacy and Rewriting using
Views

We
consider the view determinacy problem over graph databases,
i.e. edge-labeled graphs, for regular path queries. These queries
select pairs of nodes in a graph that are connected through a path
whose sequence of labels satisfies a given regular expression. A view
specification is a set of such queries. We say that a view
specification *V* determines a query *Q* if, for all databases *D*, the
answers to *V* on *D* contain enough information to answer *Q*.

In this talk, we present two contributions to this question. First, we show that, when it is additionnally required that there exists a monotone rewriting of the query using the view, then this rewriting can be expressed as a Datalog query, and can therefore be evaluated in polynomial time.

Second, we show that, if we restrict views and queries to only use one relational symbol, that is to only talk about distances between nodes, then we can decide almost all queries that are determined by a given view. We call this weaker notion asymptotic determinacy. Moreover, when the queries are determined by the views, we also provide first-order rewritings of the queries using the views.

10:5411:06
Regular Path Queries on Graphs with
Data: A Rigid Approach

Regular
path queries (RPQ) is a classical navigational query formalism for
graph databases to specify constraints on labeled paths. Recently,
RPQs have been extended by Libkin and Vrgoc to incorporate data value
comparisons among different nodes on paths, called regular path
queries with data (RDPQ). It has been shown that the evaluation
problem of RDPQs is PSPACE-complete and NLOGSPACE-complete in data
complexity. On the other hand, the containment problem of RDPQs is in
general undecidable. In this paper, we propose a novel approach to
extend regular path queries with data value comparisons, called rigid
regular path queries with data (RRDPQ). The main ingredient of this
approach is an automata model called nondeterministic rigid register
automata (NRRA), in which the data value comparisons are rigid, in the
sense that if the data value in the current position *x* is compared to
a data value in some other position *y*, then by only using the labels
(but not data values), the position *y* can be uniquely determined from
*x*. We show that NRRAs are robust in the sense that nondeterministic,
deterministic and two-way variant of NRRAs, as well as an extension of
regular expressions, are all of the same expressivity. We then argue
that the expressive power of RDPQs are reasonable by demonstrating
that for every graph database, there is a localized transformation of
the graph database so that every RDPQ in the original graph database
can be turned into an equivalent RRDPQ over the transformed
one. Finally, we investigate the computational properties of RRDPQs
and conjunctive RRDPQs (CRRDPQ). In particular, we show that the
containment of CRRDPQs (and RRDPQs) can be decided in
2EXPSPACE.

11:0611:18
Faster Existential FO Model Checking
on Posets

We improve upon (and give a simpler proof of) a recent result of Bova, Ganian and Szeider (CSL-LICS 2014), which states that the model checking problem for the existential fragment of first order logic and partially ordered sets is fixed-parameter tractable if the width (size of the largest antichain) of the poset is fixed. We give two algorithms which show that the problem is fixed-parameter tractable not only in the size of the formula, but also in the width of the poset. The first algorithm is based on a natural, and easy to understand, reduction to a CSP instance of a special kind, while the second algorithm, with better time complexity, uses a reduction to a restricted variant of the multicoloured clique problem, which is then efficiently solved. We complement these results by showing that, under a certain complexity-theoretical assumption, the existential FO model-checking problem does not have a polynomial kernel.

11:1811:30
Ordered Navigation on Multi-attributed
Data Words

We consider temporal logics on multi-attributed data words which are words where each position additionally carries multiple data values. Recently, BD-LTL was introduced as a temporal logic on data words extending LTL by navigation along positions of single data values. As allowing for navigation wrt. tuples of data values renders the satisfiability problem of the logic undecidable, we introduce ND-LTL, an extension of BD-LTL by a restricted form of tuple-navigation. We impose a tree order on the attributes that has to be respected during navigation. Tree orders can model naturally occurring dependency relations in object oriented or parallel systems. While complete ND-LTL is still undecidable, the two natural fragments allowing for either future or past navigation along data values are Ackermann-hard, yet decidable. Imposing the same restrictions on BD-LTL yields two 2ExpSpace-complete fragments while satisfiability for the full logic is known to be as hard as reachability in Petri nets.

11:3011:42
Extremely Uniform Branching Programs

We propose
a new descriptive complexity notion of uniformity for
branching programs solving problems defined on structured data.
We observe that FO[=]-uniform (*n*-way) branching programs are
unable to solve the tree evaluation problem studied by Cook,
McKenzie, Wehr, Braverman and Santhanam in 2012 because such
programs possess their thriftiness
property. Similarly, FO[=]-uniform (*n*-way) branching programs
are unable to solve the P-complete GEN problem because such
programs possess the incremental property studied by Gál, Koucký
and McKenzie in 2008.

Joint work with Andreas Krebs and Pierre McKenzie to appear in NCMA 2014.

11:4512:00
Break

12:0013:00
Session 6A

12:0012:12
Non-Elementary Complexities for
Branching VASS, MELL, and Extensions

We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case—and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete.

Joint work with Sylvain Schmitz, published in the proceedings of CSL-LICS '14, and available at arXiv:1401.6785 [cs.LO]

12:1212:24
Hyper-Ackermannian Bounds for Pushdown
Vector Addition Systems

This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian).

This is a joint work with M. Praveen and Grégoire Sutre. The full paper is available as a CSL-LICS '14 paper.

12:2412:36
Branching Time Logic and Flat Counter
Systems

Reachability and model-checking problems for flat counter systems are known to be decidable. Even though sharp complexity bounds for model-checking problem for various linear time logics over flat counter system is known, for model checking problems of branching time logic and flat counter system, the best known upper bound is made of a tower of several exponentials. Herein, we investigate and provide new results on the model checking problem of flat counter systems with branching-time properties. We show an equivalence between satisfiability of Presburger arithmetic and model-checking branching-time logics like CTL*, CTL, CTL[EF] over flat counter systems.

12:3612:48
Subclasses of Presburger Arithmetic
and the Weak EXP Hierarchy

I will show that for any fixed *i* > 0, validity in Presburger arithmetic with *i* + 1 quantifier
alternations beginning with an existential quantifier is complete for
the *i*-th level of the weak EXP hierarchy, an analogue to the
polynomial-time hierarchy residing between NEXP and
EXPSPACE.

12:4813:00
Automaton over Reals Accepting an
FO[+,<]-set

In this
talk, we intend to show a polynomial-time algorithm which
takes as input a finite deterministic weak-Büchi automaton
reading *d*-tuples of digits, and decides if the subset of
[0,1]^{d} accepted by this automaton is
definable by a FO[+,<]-formula.

12:0013:00
Session 6B

12:0012:12
Zero-Reachability in Probabilistic
Multi-Counter Automata

We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases.

In the first case, when we are interested in
the probability of all runs that visit zero in *some* counter, we show that the qualitative zero-reachability is
decidable in time which is polynomial in the size of a given pMC
and doubly exponential in the number of counters. Further, we
show that the probability of all zero-reaching runs can be
effectively approximated up to an arbitrarily small given error
ε > 0 in time which is polynomial in
log(ε), exponential in the size of a given pMC, and
doubly exponential in the number of counters.

In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error ε > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.

12:1212:24
Solving Adversarial Patrolling Games
with Bounded Error

Patrolling games are partially observable games played by two players, the defender and the attacker. The defender aims for detecting intrusions into vulnerable targets by following randomized routes among them. The time needed to complete an intrusion at each target is finite, and the aim of the attacker is to maximize the probability of a successful (i.e., undetected) intrusion. The attacker knows the defender's strategy and may observe her moves and her current position.

We show how to translate patrolling games into turn-based perfect information stochastic games with safety objectives so that optimal strategies in the perfect information games can be transferred back to patrolling games. We design, to the best of our knowledge, the first algorithm which can compute an ε-optimal strategy for the defender among all (history-dependent) strategies.

12:2412:36
Minimizing Running Costs in
Consumption Systems

In our paper we study the controller synthesis problem for resource-dependent systems with a finite battery capacity, where the task of the controller is to minimize the long-run average consumption while preserving the functionality of the system encoded by a given linear-time property. We show that an optimal controller always exists, and it may either need only finite memory or require infinite memory (it is decidable in polynomial time which of the two cases holds). Further, we show how to compute an effective description of an optimal controller in polynomial time. Finally, we consider the limit values achievable by larger and larger battery capacity, show that these values are computable in polynomial time, and we also analyze the corresponding rate of convergence. To the best of our knowledge, these are the first results about optimizing the long-run running costs in systems with bounded energy stores.

The presentation is based on the paper
Minimizing Running Costs in Consumption Systems

by T. Brazdil,
D. Klaska, A. Kucera and P. Novotny, which was accepted for
publication in proceedings of CAV 2014.

12:3612:48
The Value 1 Problem for Probabilistic
Automata

I will discuss recent developments about algorithmic properties for probabilistic automata over finite words. This computation model is a generalization of (classical) automata, where transitions are stochastic.

Despite its simple and natural definition, this model turns out to be very expressive, and since its introduction in 1963 many properties have been shown to be undecidable. Over the last years, there has been a renewned interested in probabilistic automata, with a focus on constructing algorithms to partially solve natural yet undecidable properties.

I will discuss our attempts to understand what is decidable about the value 1 problem: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1?

12:4813:00
Tractable Query Answering under
Probabilistic Constraints

Large knowledge bases such as
YAGO or DBpedia
can be used to answer queries in various domains. However, as they
are automatically harvested from Web sources, they may be
*incomplete*: important facts may be missing because they were
not materialized in the original sources, or could not be
extracted correctly. To mitigate this problem, approaches such as
association rule mining can extract
statistical rules from the data which hold in most situations. For
instance, people are usually nationals of the country where they
are born; people who died in a place are often buried there. The
application of such rules allows us to infer some of the missing
facts, which may help mitigate the issue of incompleteness. Hence,
we study the problem of query answering on large-scale knowledge
bases under the constraints of such probabilistic deduction
rules. As such rules only represent statistical tendencies,
one needs to keep track of uncertainty on rule consequences when
reasoning about them. There is a large body of work on
probabilistic data management; yet,
in that setting, many important tasks are intractable. For example,
fixed conjunctive queries may be
#P-hard to evaluate on a probabilistic
instance, even in the very simple tuple-independent
database (TID) model. To work around
such hardness results, existing work has already investigated
which query classes are tractable over all data instances, with a
complex dichotomy between safe and
unsafe queries.

Yet, there has
been no attempt to generalize the observation that
query evaluation is tractable, for *all* queries and for much
more expressive query languages, on some instances such as
probabilistic XML trees. Our work follows
this intuition and revisits the probabilistic inference problem by
studying *instance classes* that ensure tractability. More
precisely, we study complexity as a function of
instance *treewidth*, which is motivated by well-known
tractability results on evaluating monadic second-order (MSO)
queries on non-probabilistic bounded-treewidth
instances and counting queries
on bounded-treewidth graphs. This approach
is also practically relevant, as the treewidth of real-world data
is usually much less than its size. We thus show that, for the TID
model, MSO query evaluation has linear data complexity if the
treewidth of the instance is fixed.

The TID model is not
sufficient to represent the consequences of uncertain deduction
rules, however: it assumes *independence* of all facts,
whereas rule application imposes *correlations* between cause
and consequence facts. Correlations are usually represented by
probabilistic events shared between multiple facts, yet their
presence makes it generally intractable to evaluate even the
simplest queries, both in the relational
and XML settings. However, we
show that query evaluation is tractable if the instance
has bounded width under a new notion of tree decomposition that
accounts for probabilistic events; intuitively, we enforce their
compatibility with the tree structure. This result implies, for
example, that it is tractable to evaluate queries on the
block-independent
disjoint probabilistic relational
model, if the underlying instance has bounded treewidth in the
usual sense and if the size of blocks is bounded by a constant. In
the XML setting, it implies that query evaluation is tractable
whenever there are only a bounded number of relevant events to
propagate at any point along the tree.

We last turn to
our original problem of query evaluation on
probabilistic instances under *uncertain deduction rules*:
the goal is to determine the answers of a query on a knowledge
base, annotated by their probability, when some of the instance
facts are uncertain, and when new uncertain facts can be generated
using the provided rules. We formally define this problem as
computing the probability of query answers in the universal model
obtained by a probabilistic version of the standard chase
procedure. We then show its tractability for the language of
guarded tuple-generating dependencies under
the assumption that the chase terminates, which may be enforced,
e.g., by syntactic conditions such as
weak acyclicity. Indeed, we show that the
rule consequences and resulting correlation events have a
bounded-width decomposition in this case. A possible avenue
for future work is to generalize the rule language
to non-terminating guarded rules, or to, e.g., disjunctive
rules. Another important extension for practical knowledge bases
would be to account for equality-generating dependencies, or for
possible element reuse among the nulls created during the chase;
however, we suspect that such extensions would lead
to undecidability. Last, it would be useful to study how to
implement the proposed methods in practice, including techniques
such as sampling or pruning irrelevant facts.

13:0014:30
Lunch

14:3015:30
Invited talk

14:3015:30
Invited talk: Aspects of Dynamic Complexity

In most real-life databases data changes frequently and
thus makes efficient query answering
challenging. Auxiliary data might help to avoid computing
query answers from scratch all the time. One way to study
this incremental maintenance scenario is from the
perspective of dynamic algorithms with the goal to reduce
(re-)computation time. Another option is to investigate
it from the perspective of low-level parallel
computational complexity [1] or parallelizable database
queries [2]. As the lowest

complexity class
AC^{0} (with a suitable unifomity condition) and
the core of the standard database query language SQL both
coincide with first-order predicate logic, one naturally
arrives at the question which queries can be
answered/maintained dynamically with first-order predicate
logic (DynFO).

The most prominent open question in Dynamic Complexity is
whether the reachability query on graphs (arguably the
simplest recursive

query) can be maintained in DynFO. It
has been shown that it can be maintained in DynFO on
undirected [1] or acyclic directed graphs [2] and on
directed embedded planar graphs [3], but the general case
remains open. Further results in [3] indicate that
reachability on graphs might be maintainable in DynFO,
after all.

Despite considerable effort in recent years, showing that
a given query can not be maintained in DynFO is a very
challenging problem, for which currently no methods are
available. Furthermore, even though AC^{0} is a small
complexity class in the static setting, first-order logic
is already quite powerful in the dynamic world. These two
observations have recently led to the study of fragments
of DynFO, e.g., by restricting or forbidding
quantification, with the idea to start developing
inexpressibility tools there.

The talk will give an introduction into dynamic complexity, survey some of itsmost important results, and report about recent work on fragments of DynFO.

- Sushant Patnaik and Neil Immerman. Dyn-FO: A parallel,
dynamic complexity class.
*J. Comput. Syst. Sci.*, 55(2):199--209, 1997. - Guozhu Dong and Jianwen Su. Incremental and
decremental evaluation of transitive closure by
first-order queries.
*Inf. Comput.*, 120(1):101--106, 1995. - Samir Datta, William Hesse and Raghav
Kulkarni. Dynamic Complexity of Directed Reachability and
Other Problems.
*ICALP 2014*.

15:3015:45
Coffee Break

15:4517:00
Session 7

15:4515:57
MSO+U

MSO+U is
an extension of monadic second-order logic, which adds a
quantifier U, called the unbounding quantifier. A formula
U*X*.φ(*X*) says that φ(*X*) is
true for arbitrarily big finite sets *X*. Languages
definable in MSO+U look like they admit finite state
recognisers. For instance consider the left Myhill-Nerode
equivalence: finite words *w* and *w*' are
equivalent if for every infinite word *u*, either
both or none of the words *wu*, *w*'*u* are
in the language. It is not difficult to show that
languages recognised in MSO+U have finitely many
equivalence classes under this relation.

In the talk, I will discuss two results: a positive result about decidability of Weak MSO+U, and a negative result about undecidability of MSO+U on infinite trees.

The positive result is that finite state recognisers do exist when set quantification is restricted to finite sets, i.e. in Weak MSO+U. With finite set quantification only, the logic admits automata models for both infinite words and infinite trees, and is decidable.

The negative
result is about MSO+U over infinite words and trees. (The
negative result is joint work with Tomasz Gogacz, Henryk
Michalewski and Michał Skrzypczak.) This logic turns out
to be dangerously expressive already over infinite words,
e.g. it can recognise languages that are arbitrarily high
in the projective hierarchy known from descriptive
complexity. This topological complexity can be combined
with Shelah's proof of undecidability of MSO over the real
numbers, to show that MSO+U is undecidable over infinite
trees (under the set-theoretic assumption that
*V* = *L*).

15:5716:09
Asymptotic Behaviour of Max-Plus
Automata and Size-Change Abstraction

Max-plus
automata are weighted automata over the semiring
(ℕ ∪ {-∞}, max, +) that compute some
functions from words to ℕ ∪ {-∞}. In this
talk, we will study the asymptotic behaviour of a max-plus
automaton and more precisely the maximum length of a word
of weight at most *n*. In particular, we will see
that this function is of the form
Θ(*n*^{α}) for a computable
rational α. This result can, in combination with
the size-change abstraction, be used for inferring the
termination time of an algorithm as a function of the size
of its input.

This is a joint work with Thomas Colcombet and Florian Zuleger.

16:0916:21
Expressiveness of Min-Max Automata

A min-max automaton is a finite state automaton with a finite number of registers storing non-negative integer values that are updated by expressions consisting of register names and operations min, max and +1. We discuss the expressiveness results concerning these automata.

This is a joint work with Thomas Colcombet and Stefan Göller.

16:2116:33
First-order Cost Logics and Automatic
Structures

We provide new characterizations of the class of regular cost functions (Colcombet 2009) in terms of different quantitative first-order logics. This result extends a classical result connecting the regular languages with the languages definable by a first-order formula over the infinite (binary) tree of finite words with equal length predicate. Furthermore, we use these results to identify a structure that is complete for the class of resource automatic structures and investigate approaches how resource (tree) automatic structures can be used to obtain decidability results for costWMSO and WMSO+U as well.

Parts of this are joint work with Simon
Leßenich, Christof Löding and Amaldev Manuel and will
appear in MFCS 2014 as Definability and
Transformations for Cost Logics and Automatic
Structures

16:3316:45
A Quantitative Counting Monadic
Second-Order Logic

We propose a new quantitative extension of monadic second-order logic, which we call qcMSO, that adds a mechanism to count the size of sets to MSO. We prove that this logic subsumes both MSO+U and costMSO, as for every formula of these logics there is a formula of qcMSO with the same evaluation. Furthermore, central costMSO questions such as boundedness or dominance can be expressed in qcMSO. Using techniques from the field of counter automata, we prove that the weak variant of our logic is decidable on both the infinite linear order and the infinite binary tree, which provides a uniform approach to algorithmic solutions for MSO+U and costMSO problems.

Joint work with Łukasz Kaiser (LIAFA, CNRS & Université Paris Diderot - Paris 7) and Martin Lang (Informatik 7, RWTH Aachen University).

16:4516:57
An Intriguing Tiling Problem

This talk introduces some simple tiling problems. Their decidability is open. These problems are tightly related to the decidability of some quantitative variants of MSO over infinite words.

The technical content of this talk is part of a collaboration with Achim Blumensath and Olivier Carton that will be presented at MFCS '14.

17:0017:15
Break

17:1518:15
Session 8

17:1517:27
Counting Models of Linear-time
Temporal Logic

We investigate the model counting problem for safety specifications expressed in linear-time temporal logic (LTL). Model counting has previously been studied for propositional logic; in planning, for example, propositional model counting is used to compute the plan's robustness in an incomplete domain. Counting the models of an LTL formula opens up new applications in verification and synthesis. We distinguish word and tree models of an LTL formula. Word models are labeled sequences that satisfy the formula. Counting the number of word models can be used in model checking to determine the number of errors in a system. Tree models are labeled trees where every branch satisfies the formula. Counting the number of tree models can be used in synthesis to determine the number of implementations that satisfy a given formula. We present algorithms for the word and tree model counting problems, and compare these direct constructions to an indirect approach based on encodings into propositional logic.

17:2717:39
The Complexity of Counting Models of
Linear-time Temporal Logic

We consider the complexity of counting bounded models of specifications expressed in Linear-time Temporal Logic. Counting word models is #P-complete, if the bound is given in unary, and as hard as counting accepting runs of non-deterministic polynomial-space Turing machines, if the bound is given in binary. Counting tree models is as hard as counting accepting runs of non-deterministic exponential-time Turing machines, if the bound is given in unary. For a binary encoding of the bound, the problem is at least as hard as counting accepting runs of non-deterministic exponential space Turing machines. On the other hand, it is not harder than counting accepting runs of non-deterministic doubly-exponential time Turing machines.

17:3917:51
Decidability of the Interval Temporal
Logic AA̅BB̅ over the Rationals

The
classification of the fragments of Halpern and Shoham's logic
with respect to decidability/undecidability of the satisfiability
problem is now very close to the end. We settle one of the
few remaining questions concerning the fragment AA̅BB̅, which
comprises the Allen's interval relations meets

and
begins

and their symmetric versions. We already proved
that AA̅BB̅ is decidable over the class of all finite linear
orders and undecidable over ordered domains isomorphic to
ℕ.

In this paper, we first show that AABB is undecidable over ℝ and over the class of all Dedekind-complete linear orders. We then prove that the logic is decidable over ℚ and over the class of all linear orders.

17:5118:03
Interval Temporal Logics and
Equivalence Relations

Interval temporal logics provide a general framework for temporal representation and reasoning, where point-based linear temporal logics can be recovered as special cases. In this paper, we study the effects of the addition of one or more equivalence relations to two meaningful fragments of Halpern and Shoham's modal logic of time intervals, namely, AA̅ and AB, interpreted over the class of finite linear orders.

18:0318:15
Checking Interval Properties of
Computations

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g. a Kripke structure, and a formula specifying its expected behavior, one can verify whether the system meets the behavior by checking the formula against the model.

Classically, system behavior is given as a formula
of a temporal logic, such as LTL and the like. These logics are
point-wise

interpreted, as they describe how the system evolves
state-by-state. However, there are relevant properties, such as those
involving temporal aggregations, which are inherently
interval-based

, and thus asking for an interval temporal logic,
such as Halpern and Shoham's modal logic of time intervals (HS, for
short).

In this talk, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of HS formulas over Kripke structures, which makes it possible to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSpace decision procedure for the meaningful fragments HS[AA̅BB̅] and HS[AA̅EE̅].

09:0010:00
Invited talk

09:0010:00
Invited talk: Monadic Second-Order
Definable Problems in Computational Complexity
Theory

Applying problem definitions in terms of monadic-second order (MSO) formulas in conjunction with evaluation procedures for tree-width-bounded graphs and reductions to them is a common approach to design efficient algorithms. Beside simplifying known proofs, this algorithmic paradigm has proven to help develop new efficient algorithms. Just like many problems in algorithmics are MSO-definable, the same is true for a large number of problems studied in the realm of parallel and space complexity classes inside deterministic polynomial time. Thus, understanding the fine-grained complexity-theoretic aspects of evaluating formulas in MSO-logic as well as its restrictions and generalizations has a great potential. The talk first surveys recent developments on approaches for evaluating MSO-formulas on tree-width-bounded graphs in terms of uniform circuits and logarithmic space. Then current and possible future complexity-theoretic applications for MSO-definitions and tree width reductions are discussed.

10:0010:30
Breakfast & coffee

10:3011:45
Session 9

10:3010:42
The Relations between Directed Tree-width
& Co.

We consider the cops and robber
games characterising DAG-width and directed tree-width (up to a
constant factor). For DAG-width games, it is an open question
whether the robber-monotonicity cost (the difference between
the minimal numbers of cops capturing the robber in the general
and in the monotone case) can be bounded by any
function. Examples show that this function (if it exists) is at
least *f*(*k*) > 4*k*/3 [Kreutzer, Ordyniak '08]. We approach a solution
by defining weak monotonicity and showing that if *k* cops win
weakly monotonically, then *O*(*k*^{2}) cops win monotonically. It
follows that bounded Kelly-width implies bounded DAG-width,
which has been open since the definition of Kelly-width
[Hunter, Kreutzer '08]. The game also corresponds to a tree
decomposition whose properties are nicer than those of
DAG-decompositions.

For directed tree-width games we
show that, unexpectedly, the cop-monotonicity cost (the cops
never revisit any vertex) is not bounded by any function. This
also separates directed tree-width from *D*-width defined in
[Safari '05], refuting a conjecture made there.

In the second part of the talk we consider the relative strength of directed width measures: does the boundedness of the values of one measure imply that that the values of the other measure are bounded? So far only some results separating directed width-measures are known. We give an almost complete picture of this relation.

10:4210:54
Logic and Contiguity of Finite-Type
Random Graphs

Finite-type random graphs are a
simple extension of the traditional Erdős-Rényi random graphs,
where each node is assigned a type, and the probability of each edge
in a graph of size *n* is a function of *n* and of the types of the
nodes. This class of random graphs is used as an approximation of more
complex models and is a model of graphs similar to an arbitrary fixed
graph. We investigate the logical laws of some specific finite-type
graphs, i.e. the limit of the probabilities that first-order formulas
are satisfied. The notion of first-order contiguity is introduced to
relate graph models having the same first-order
limits.

10:5411:06
The Propagation Depth of Local
Consistency

We
establish optimal bounds on the number of nested
propagation steps in *k*-consistency tests.

It
is known that local consistency algorithms such as arc-,
path- and *k*-consistency are not efficiently
parallelizable. Their inherent sequential nature is caused
by long chains of nested propagation steps, which cannot
be executed in parallel. This motivates the question
What is the minimum number of nested propagation steps
that have to be performed by

*k*-consistency
algorithms on (binary) constraint networks with *n*
variables and domain size *d*?

The number
of nested propagation steps equals the minimum number of
rounds Spoiler needs to win the existential
*k*-pebble game on two structures with universes of
size *n* and *d*. By applying involved tools
from finite model theory we show that the trivial upper
bound of
*n*^{k-1}*d*^{k-1}
is tight. As a consequence we get optimal lower bounds on
the quantifier rank of existential-positive
*k*-variable first-order sentences and on the
propagation depth of *k*-consistency
tests.

11:0611:18
Interpolation for Guarded Logics

Given a valid implication in the guarded negation fragment of first-order logic, there is an interpolant that also lives in the guarded negation fragment. However, the model-theoretic methods originally used to prove this result were non-constructive.

I will present recent work exploring constructive methods for interpolation in guarded logics. One theme is the exploitation of the tree-like model property for these logics, which enables us to use tools from modal logic and automata theory.

11:1811:30
Decidability of Weak Logics with
Deterministic Transitive Closure

The deterministic transitive closure operator, added to languages containing even only two variables, allows to express many natural properties of a binary relation, including being a linear order, a tree, a forest or a partial function. This makes it a potentially attractive ingredient of computer science formalisms. We consider the extension of the two-variable fragment of first-order logic by the deterministic transitive closure of a single binary relation, and prove that the satisfiability and finite satisfiability problems for the obtained logic are decidable and EXPSPACE-complete. This contrasts with the undecidability of two-variable logic with the deterministic transitive closures of several binary relations, known before. We also consider the class of universal first-order formulas in prenex form. Its various extensions by deterministic closure operations were earlier considered by other authors, leading to both decidability and undecidability results. We examine this scenario in more details.

This is joint work with Witold Charatonik and Emanuel Kieroński.

11:3011:42
Preservation and Decomposition
Theorems for Bounded Degree Structures

This talk
is based on the CSL-LICS '14 paper Preservation
and decomposition theorems for bounded degree
structures

co-authored by Frederik Harwath, Lucas
Heimberg, and Nicole Schweikardt (Goethe-University
Frankfurt am Main) [link].

In
this paper, we provide elementary algorithms for two
preservation theorems for first-order sentences with
modulo *m* counting quantifiers
(FO+mod_{m}) on the class
*C*_{d} of all finite structures of
degree at most *d*: For each
FO+mod_{m}-sentence that is preserved under
extensions (homomorphisms) on *C*_{d},
a *C*_{d}-equivalent existential
(existential-positive) FO-sentence can be constructed in
6-fold (4-fold) exponential time. For FO-sentences, the
algorithm has 5-fold (4-fold) exponential time
complexity. This is complemented by lower bounds showing
that for FO-sentences a 3-fold exponential blow-up of the
computed existential (existential-positive) sentence is
unavoidable.

In this talk, I will focus on a third
contribution of our paper, concerning Feferman-Vaught
decompositions. The classical Feferman-Vaught theorem
states that for certain forms of compositions of
structures (like disjoint unions and cartesian products),
the theory of a structure composed from simpler structures
is determined by the theories of the simpler
structures. Algorithmic versions of such decomposition
theorems are typically of the following form: A given
FO-sentence that shall be evaluated in a composition of
structures can be transformed into a decomposition

,
that is, a Boolean combination of FO-sentences that each
are evaluated in only one component structure. It is known
that even when restricted to disjoint unions of tree
structures, a non-elementary complexity for such an
algorithmen is unavoidable (Dawar, Grohe, Kreutzer,
Schweikardt 2007).

Here, we restrict our attention
to the classes *C*_{d} for
*d* ≥ 2. We provide an algorithm that
computes decompositions, that are equivalent to the input
FO-formula on disjoint unions of a finite number of
structures from *C*_{d} for
*d* ≥ 3 (*d* ≥ 2). The
algorithm’s running time is 3-fold (2-fold) exponential in
the size of the input formula. This is achieved by
employing an elementary construction for Hanf normal forms
(Bollig, Kuske 2012) and decomposing the resulting
Hanf-formulas.

Our algorithm is optimal in the following sense: Even on binary forests (unions of labeled chains), that is, classes of structures of degree at most 3 (respectively, 2), a 3-fold (2-fold) exponential blow-up of the size of decompositions in terms of the size of the input formula is unavoidable.

11:4512:00
Break

12:0013:00
Session 10A

12:0012:12
Tree Games with Regular Objectives

We study tree games developed recently by Matteo Mio as a game interpretation of the probabilistic μ-calculus. With expressive power comes complexity. It was shown that tree games are able to encode the Blackwell games and, consequently, are not determined under deterministic strategies.

First, we will show that tree games with objectives recognisable by so-called game automata are determined under deterministic, finite memory strategies. Then, for the case of arbitrary regular languages of trees, we will present an exponential time algorithm for deciding the determinacy of a finite tree game under deterministic strategies.

12:1212:24
Towards a Regular Theory of
Parameterized Concurrent Systems

We
present parameterized communicating automata (PCAs), where
finite-state processes exchange messages via rendez-vous
or through bounded FIFO channels. Unlike classical
communicating automata, a given PCA can be run on any
network topology of bounded degree. We present various
Büchi-Elgot-Trakhtenbrot theorems for PCAs, which roughly
read as follows: Let *S* be an existential MSO
formula and *T* be any of the following topology
classes: pipelines, ranked trees, grids, or rings. There
is a PCA that is equivalent to *S* on all topologies from
*T*. In the case where each process executes a bounded
number of contexts (each context restricting communication in
a suitable way), we can even show that PCAs are closed
under complementation, are expressively equivalent to
full MSO logic, and have a decidable emptiness problem.

The talk contains results from joint works with Paul Gastin, Akshay Kumar, and Jana Schubert.

12:2412:36
Rewriting Games on Nested Words

In the
paper this talk is based on, we investigate the complexity
of a simple string rewriting game, played by two players,
henceforth called Player 1 and Player 2, on a
string *w*. In each round, Player 1 selects a
substring in the current string and Player 2 replaces
this substring by some other string. Thus, a play of this
game yields a sequence of strings
*w* = *w*_{1},*w*_{2},*w*_{3},... Player 1's
goal is to arrive at some string *w*_{i} in a given
*target language* *L*, while
Player 2's goal is to prevent this. Depending
on the exact setting, there are restrictions on the
substrings that Player 1 can choose and on the
strings by which Player 2 can
replace them.

One form of such games
was introduced by Muscholl, Schwentick and Segoufin
under the name *active
context-free games* to formalise the following framework
studied by Milo et al.: an intensional
*Active XML* document is given, where some
elements consist of functions representing
web services that can be called. The goal is to
rewrite the initial document by a series of web
service calls into a document that matches a
given schema. In Milo et al.'s work, the schema is
represented by an XML document type definition
(DTD), and the substrings to be replaced are XML
elements, i.e. substrings starting with some opening tag
and ending with the corresponding closing tag. It
was argued that, due to the rectricted nature of
DTDs, the problem can be reduced to a rewriting game
as described above, in which the substrings selected
by Player 1 are just singleton symbols, the set
of allowed replacement strings for each symbol is a
regular language and the target language is regular,
as well. In the work of Muscholl et al. the complexity of
the problem to determine the winner in such
games (mainly with finite replacement languages) has
been studied. Whereas this problem is undecidable in
general, there are important cases in which it can
be solved, particularly, if Player 1 choses symbols
to be replaced in a left-to-right fashion.

In our paper we study more
expressive target schemas and consequently focus on
the replacement game not on flat strings

but on
string representations of XML documents, abstracted
as nested words (cf. Alur and Madhusudan), and we
only consider strategies of Player 1 that
proceed from left to right.

As the complexity of determining whether Player 1 has a winning strategy is high in the general case (doubly exponential time), restrictions on the nesting depth of replacements and the target schemas are considered. In the case in which no nesting is allowed and the target language can be specified in (an abstraction of) XML Schema, the problem becomes solvable in polynomial time. Further variants of the setting are studied.

This is joint work with Thomas Schwentick.

12:3612:48
Beyond One-Goal Strategy Logic

Starting from the seminal work introducing Alternating Temporal Logic, formalisms for strategic reasoning have assumed a prominent role in the specification and verification of multi-agent systems. With the aim of describing sophisticate interactions among agents, new and more powerful logics have been recently introduced. Among the others, Strategy Logic allows to formalize important solution concepts by treating agent strategies as first-order objects.

A drawback from the high power of Strategy Logic is that it admits non-behavioral strategies: a choice of an agent, at a given moment of a play, may depend on the choices other agents make in the future or in counterfactual plays. As the latter moves are unpredictable, such strategies cannot be implemented in practice, making the use of the logic problematic.

In this paper, we restrict our attention to powerful fragments of Strategic Logic which admits a behavioral semantics, i.e. formulas can be checked without guessing counterfactual moves of the mentioned players. Specifically, we study the model-checking problem, showing that it is 2-ExpTime-complete.

12:4813:00
Infinite Sequential Games with
Real-Valued Payoffs

This is joint work with Arno Pauly. We investigate the existence of certain types of equilibria (Nash, epsilon-Nash, subgame perfect, epsilon-subgame perfect) in infinite sequential games with real-valued payoff functions depending on the class of payoff functions (continuous, upper semi-continuous, Borel) and whether the game is zero-sum. Our results hold for games with two or up to countably many players.

Several of these results are corollaries of stronger results that we establish about equilibria in infinite sequential games with some weak conditions on the occurring preference relations. We also formulate an abstract equilibrium transfer result about games with compact strategy spaces and open preferences.

12:0013:00
Session 10B

12:0012:12
A 3-State Invertible-Reversible Mealy
Automaton cannot Generate a Burnside Group

Joint work with Matthieu Picantin (Université Paris Diderot) and Dmytro Savchuk (University of South Florida).

The general Burnside problem — whether there exists an infinite finitely generated group whose all elements have finite order — has been introduced in 1902. Automaton groups are a prosperous source of examples to give a negative answer to this question. All the examples of Burnside automaton groups given in the literature are generated by non-reversible invertible automata. In this talk I will show that a 3-state invertible-reversible automaton cannot generate Burnside groups.

12:1212:24
Non-definability of Languages by
Generalized First-order Formulas over (ℕ,+)

We
consider first-order logic with monoidal quantifiers over
words. We show that all languages with a neutral letter,
definable using the addition predicate are also definable
with the order predicate as the only numerical
predicate. Let *S* be a subset of monoids. Let
*L*_{S} be the logic closed under
quantification over the monoids in *S*, and NL be the
class of neutral letter languages. Then we show that
*L*_{S}[<,+] ∩ NL = *L*_{S}[<] ∩ NL. Our
result can be interpreted as the Crane Beach conjecture to
hold for the logic *L*_{S}[<,+]. As
a corollary of our result we get Benedikt and Libkin's
result that FO[<,+] collapses to FO[<] in presence
of a neutral letter, and for solvable monoids, we get the
result of Roy and Straubing that FO+MOD[<,+] collapses
to FO+MOD[<]. For cyclic groups, we answer an open
question of Roy and Straubing, proving that MOD[<,+]
collapses to MOD[<]. Our result also shows that
multiplication as a numerical predicate is necessary for
Barrington's theorem to hold and also to simulate majority
quantifiers. We also show that given a regular language,
it is decidable if it is in
*L*_{S}[<,+] for any
*S*.

12:2412:36
Regular Sensing

The size of deterministic automata required for recognizing regular and omega-regular languages is a well-studied measure for the complexity of languages. We introduce and study a new complexity measure, based on the sensing required for recognizing the language. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read in order to decide its membership in the language.

We show that for finite words, size and sensing are related, and minimal sensing is attained by minimal automata. Thus, a unique minimal-sensing deterministic automaton exists, and is based on the language's right-congruence relation. For infinite words, the minimal sensing may be attained only as a limit, by an infinite sequence of automata. We show that the optimal limit of such sequences can be characterized by the language's right-congruence relation, which enables us to find the sensing cost of omega-regular languages in polynomial time. Also, interestingly, the sensing cost is independent of the acceptance condition. This is in contrast with the size measure, where the size of a minimal deterministic automaton for an omega-regular language depends on the acceptance condition, a unique minimal automaton need not exists, and the problem of finding one is NP-complete. We also study the affect of standard operations (e.g., union, concatenation, etc.) on the sensing cost of automata and languages.

12:3612:48
The Monoid of Queue Actions — A New(?)
Monoid Worth to be Studied(?)

We model the behaviour of a fifo queue as a monoid of transformations that are induced by sequences of writing and reading. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem is NL-complete. Furthermore, we present an algebraic characterization of this monoid's recognizable subsets. Finally, we prove that it is not Thurston-automatic.

These results have been accepted for publication in the proceedings of MFCS.

12:4813:00
Which Comparability Graphs are
Embeddable into Trees?

Recently, we have shown that
satisfiability for CTL* with constraints over the integers is
decidable using a new technique. Our approach reduces the
satisfiability problem of CTL* with constraints over a class of
structures C to the problem whether C has a certain property
EHomDef

. Here we try to apply this approach to concrete domains
that are tree-like and obtain several results.

13:0014:30
Lunch

14:3015:30
Session 11

14:3014:42
Causality-based LTL Model Checking
without Automata

The classical LTL model checking algorithm starts by transforming the negated LTL property into the Büchi automaton. Unfortunately, already that step often takes exponential time and space. For concurrent programs the size of the formula that describes, e.g., fairness assumptions, grows with the size of the program to be verified. Therefore, the exponential translation cost often does not allow the verification process even to start. In the present work we propose an alternative to the automata-based model checking, which is lazy and compositional with respect both to the system and to the LTL property. In our procedure, we characterize the existence of erroneous executions as Mazurkiewicz-style concurrent traces and apply causality-based transformation rules to refine them until a contradiction can be shown. The algorithm operates directly on the level of an LTL formula and a concurrent program description, and lazily pulls from both of them only the parts that are necessary in the current analysis context. We report on experimental results for previously intractable multi-threaded benchmarks.

14:4214:54
Hypergraph Acyclicities and
Propositional Model Counting

We present in this talk structural restrictions of CNF-formulas to find tractable classes for the problem #SAT. We explain why α-acyclicity is not appropriate for this problem. We then introduce β-acyclicity and present a polynomial time algorithm for #SAT on β-acyclic CNF-formulas.

14:5415:06
On Module Checking and Strategies

Two decision problems are very close in spirit: module checking of CTL/CTL* and model checking of ATL/ATL*. The latter appears to be a natural multi-agent extension of the former and, therefore, it is commonly believed that model checking of ATL(*) subsumes module checking of CTL(*).

A more careful look at the known complexity results, however, makes one realize that the relationship is somewhat suspicious: module checking of CTL is Exptime-complete, while model checking of ATL is only Ptime-complete. This suggests that the relationship may not be as simple as believed. In this work, we show that the difference is indeed fundamental. The way in which behavior of the environment is understood in module checking cannot be equivalently characterized in ATL(*). Conversely, if one wants to embed module checking in ATL(*) then its semantics must be extended with two essential features, namely nondeterministic strategies and long-term commitment to strategies.

15:0615:18
First Cycle Games

First cycle games (FCGs) are played
on a finite graph by two players who push a token along the edges of
the graph until a simple cycle is formed. The winner is determined by
some fixed property *Y* of the sequence of nodes forming this cycle. We
are motivated by two questions: Under what conditions on *Y* is every
FCG memoryless determined? What is the connection between FCGs and
traditional winning conditions such as mean-payoff games? Our answers
to these questions take the following form: we generalise the proof by
Ehrenfeucht and Mycielski that mean-payoff games are memoryless
determined and then supply a recipe for proving that a winning
condition is memoryless determined. All memoryless determined infinite
duration games that we are aware of can be proved memoryless
determined using this recipe.

15:1815:30
On Determinization of Good-for-Games
Automata

Good-For-Games (GFG) automata are non-determinitic automata with a semantic condition that gives them some deterministic features: there must exist a strategy to resolve the non-determinism without future look-ahead, while still accepting every word of the language. This notion was introduced in different contexts, and several question about its precise link with determinism were left open. In particular we answer here the blow-up problem: what is the complexity of determinizing a GFG automaton. It turns out this complexity is linear for Büchi automata, and exponential for co-Büchi automata (and so for parity automata in general).

This is a joint work with Denis Kuperberg.

15:3015:45
Coffee Break

15:4516:33
Session 12

15:4515:57
The Linear-Hyper-Branching Spectrum of
Temporal Logics

The family of temporal logics has recently been extended with logics for the specification of hyperproperties, such as noninterference or observational determinism. Hyperproperties relate multiple execution traces of a system by requiring that they satisfy a certain relationship, such as an identical valuation of the low-security outputs. Unlike classic temporal logics like LTL or CTL*, which refer to one execution trace at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL* can express such relationships by explicitly quantifying over multiple execution traces simultaneously. In this talk, we study the extended spectrum of temporal logics by relating the new logics to the linear-branching spectrum of process equivalences.

15:5716:09
Tableau-based Decision Procedure for
ATL+

We present
an extended abstract of the paper entitled Optimal Tableaux-based
Decision Procedure for Testing Satisfiability in the
Alternating-time Temporal Logic ATL+

, co-written with Serenella
Cerrito and Valentin Goranko.

16:0916:21
On the Remarkable Features of Binding
Forms

Hilbert's Entscheidungsproblem has given rise to a broad and productive line of research in mathematical logic, where the classification process of decidable classes of first-order sentences represent only one of the remarkable results. According to the criteria used to identify the particular classes of interest, this process was declined into several research programs, of which some of the most deeply investigated are the ones classifying sentences in prenex normal form in base of their prefix vocabulary.

Unfortunately, almost all of these approaches did not shed any light on the reasons why modal logic is so robustly decidable. Trying to answer to this question, Andreka, van Benthem, and Nemeti introduced the guarded fragment of first-order logic, which generalizes the modal framework by essentially retaining all its fundamental properties. They started, so, a completely new research program based on the way quantifications can be relativized. Although this approach succeeded in its original task, we cannot consider it satisfactory in spotting the reasons why some complex extensions of modal logic are well-behaved. In particular, by just using the related results, we are not able to derive the decidability of multi-agent logics for strategic abilities.

In this paper, aiming to lay the
foundation for a more thorough understanding of some of
these decidability questions, we introduce a new kind of
classification based on the binding forms that are
admitted in a sentence, i.e., on the way the arguments of
a relation can be bound to a variable. We describe a
hierarchy of first-order fragments based on the Boolean
combinations of these forms, showing that the less
expressive one is already incomparable with the guarded
logic and related extensions. We also prove, via a new
model-theoretic technique, that it enjoys the finite-model
property, a Σ_{3}^{P} satisfiability
problem, and a PTime model-checking
problem.

16:2116:33
Logic for Indexed Languages

We define Nested Dyck words and we show that the class of languages recognized by a realtime Nested Stack Automata coincides with the class of languages definable in a first order logic extended by existential quantifications over a matching and a family of unary relations defining a Dyck labeling.