Highlights 2014

Abstract

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

1. 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.
2. 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.
3. 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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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

1. the Immerman-Vardi Theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and
2. 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.

Abstract

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 A is the infinite set of possible data values, and k is the number of registers. Checking emptiness of such automata resolves to BFS on the infinite transition graph; similar results hold for other well known algorithms from automata theory, such as minimization. There was also similar research for more complex computation models, such as Turing machines.

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

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

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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₁ + f(n₂ + f(n₃ + 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₁,…,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₁,…,n_k are positive, is equivalent to g'(f) = n₁ + f(m), where m = n₂+⋯+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.

Abstract

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.

Abstract

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 3r 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.

Abstract

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.

Abstract

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.

Abstract

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

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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² n) delay, and can restart enumeration within O(log² 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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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]

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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?

Abstract

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.

Abstract

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⁰ (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⁰ 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.

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

Abstract

MSO+U is an extension of monadic second-order logic, which adds a quantifier U, called the unbounding quantifier. A formula UX.φ(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).

Abstract

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.

Abstract

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.

Abstract

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

Abstract

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).

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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̅].

Abstract

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.

Abstract

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) > 4k/3 [Kreutzer, Ordyniak '08]. We approach a solution by defining weak monotonicity and showing that if k cops win weakly monotonically, then O(k²) 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.

Abstract

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.

Abstract

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-1d^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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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₁,w₂,w₃,... 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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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.

Abstract

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 Σ₃^P satisfiability problem, and a PTime model-checking problem.

Abstract

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.