9:30–10:00 Registration (room: Forum A)

10:00–11:15 Tutorial 1 (chair: Stefan Kiefer, room: Forum A)

• Antonín Kučera (Masaryk University): Methods and tools for solving infinite-state stochastic games

  Authors:

  Abstract:

  The tutorial focuses on methods and tools for solving turn-based stochastic games with infinitely many states. Typically, such games are obtained as game-theoretic extensions of established computational models, such as pushdown automata, one-counter automata, vector addition systems with states, lossy channel systems, etc. An important step towards solving such games is a detailed understanding of both non-deterministic and fully probabilistic variants of the model, which often requires new concepts and proof techniques, especially in the fully probabilistic subcase. We start with the reachability objective, and identify the main differences between finite-state and infinite-state games. In particular, we show that optimal strategies do not necessarily exist in infinite-state stochastic games, and even if they do, they may require infinite memory. Further, we show that infinite-state stochastic games are not weakly determined in the subclass of memoryless strategies. Then, we show how to solve the reachability objective for some concrete classes of infinite-state stochastic games. In particular, we concentrate on games over stateless pushdown automata and one-counter systems. A useful tool for analyzing infinite-state stochastic systems are martingales. We give a brief introduction to martingales and the associated toolbox (optional stopping theorem, Azuma–Hoeffding inequality), and show how these can be applied to the analysis of one-counter stochastic processes and games. In the end of the tutorial, we present an overview of existing results and mention some open problems. The tutorial does not require any special knowledge beyond the fundamentals of probability theory (in particular, no prelimary knowledge about martingales is assumed).

11:45–12:45 Tutorial 1 (continued)

• Antonín Kučera (Masaryk University): Methods and tools for solving infinite-state stochastic games

  Authors:

  Abstract:

  The tutorial focuses on methods and tools for solving turn-based stochastic games with infinitely many states. Typically, such games are obtained as game-theoretic extensions of established computational models, such as pushdown automata, one-counter automata, vector addition systems with states, lossy channel systems, etc. An important step towards solving such games is a detailed understanding of both non-deterministic and fully probabilistic variants of the model, which often requires new concepts and proof techniques, especially in the fully probabilistic subcase. We start with the reachability objective, and identify the main differences between finite-state and infinite-state games. In particular, we show that optimal strategies do not necessarily exist in infinite-state stochastic games, and even if they do, they may require infinite memory. Further, we show that infinite-state stochastic games are not weakly determined in the subclass of memoryless strategies. Then, we show how to solve the reachability objective for some concrete classes of infinite-state stochastic games. In particular, we concentrate on games over stateless pushdown automata and one-counter systems. A useful tool for analyzing infinite-state stochastic systems are martingales. We give a brief introduction to martingales and the associated toolbox (optional stopping theorem, Azuma–Hoeffding inequality), and show how these can be applied to the analysis of one-counter stochastic processes and games. In the end of the tutorial, we present an overview of existing results and mention some open problems. The tutorial does not require any special knowledge beyond the fundamentals of probability theory (in particular, no prelimary knowledge about martingales is assumed).

14:15–15:30 Tutorial 2 (chair: Thomas Schwentick, room: Forum A)

• Benedikt Bollig (LSV, ENS Cachan): Automata and Logics for Distributed Systems

  Authors:

  Abstract:

  Automata are a popular model of computer systems, making them accessible to formal methods and, in particular, synthesis and model checking. While classical finite-state automata are suitable to model sequential boolean programs, models of distributed and concurrent systems involve several interacting processes and extend finite-state machines in many respects. Roughly, we may classify system models according to their communication paradigm (shared variables, message passing, broadcasting), the type of a process (finite-state, recursive, timed), or the number of processes (static, dynamic, bounded, parameterized). In this tutorial, we survey automata models for several combinations of the above-mentioned characteristics. We also present suitable specification formalisms such as monadic second-order logic, temporal logic, and rational expressions. In particular, we will compare the expressive power of automata and logics, give translations of specifications into automata, and show how to solve the model-checking problem: Does a given automaton satisfy its specification?

16:00–17:00 Tutorial 2 (continued)

• Benedikt Bollig (LSV, ENS Cachan): Automata and Logics for Distributed Systems

  Authors:

  Abstract:

  Automata are a popular model of computer systems, making them accessible to formal methods and, in particular, synthesis and model checking. While classical finite-state automata are suitable to model sequential boolean programs, models of distributed and concurrent systems involve several interacting processes and extend finite-state machines in many respects. Roughly, we may classify system models according to their communication paradigm (shared variables, message passing, broadcasting), the type of a process (finite-state, recursive, timed), or the number of processes (static, dynamic, bounded, parameterized). In this tutorial, we survey automata models for several combinations of the above-mentioned characteristics. We also present suitable specification formalisms such as monadic second-order logic, temporal logic, and rational expressions. In particular, we will compare the expressive power of automata and logics, give translations of specifications into automata, and show how to solve the model-checking problem: Does a given automaton satisfy its specification?

9:00–9:30 Registration (room: Forum A)

9:30–10:30 Keynote 1 (chair: Thomas Schwentick, room: Forum A)

• Marc Zeitoun (Labri, Bordeaux University): From membership to covering via separation

  Authors:

  Abstract:

  The membership problem is the standard mean to investigate the expressive power of fragments of MSO over classical structures, such as words or trees. It asks for an algorithm taking as input a regular language, and deciding whether it can be expressed within the fragment under study. It has been solved successfully for many natural fragments of first-order logic, but for some of them the situation is stuck since the 70s. This is the case for levels of the ‘quantifier alternation hierarchy’, which stratify first-order logic: membership algorithms have been obtained for lower ones only. In view of recent progress for some of these levels, a reason may be that membership is too restrictive as a framework. In this talk, I will introduce two problems called ‘separation’ and ‘covering’, which both generalize membership. Separation takes as input two regular languages rather than just one, while covering takes as input a finite number of regular languages. I will explain the connections between the three problems, and why it is interesting to consider them in order to better understand logical fragments of MSO.

11:00–12:25 Session 1 – Synthesis & Stochastic Systems (chair: Antonín Kučera, room: Forum A)

• Rodica Condurache: The Complexity of Rational Synthesis

  Authors: Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini and Jean-Francois Raskin

  Abstract:

  In this paper, we study the computational complexity of the cooperative and non-cooperative rational synthesis problems, as introduced by Kupferman, Vardi and coauthors in recent papers for general LTL objectives. From the previous papers we get that the cooperative and non-cooperative rational synthesis problems are 2ExpTime-complete for specifications expressed in linear temporal logic (LTL), thus matching exactly the complexity of classical zero-sum two-player LTL synthesis. We investigate these problems on multiplayer turn-based games played on graphs, and provide complexity results for the classical omega-regular objectives, namely reachability, Safety, Buchi, coBuchi, parity, Rabin, Streett and Muller objectives. Most of these complexity results are tight and shed light on how to solve those problems optimally. We also study the computational complexity of solving those games when the number of players is fixed. This parametrized analysis makes sense as the number of components forming the environment may be limited in practical applications. **Work published and presented at ICALP 2016.

• Sven Schewe: A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

  Authors:

  Abstract:

  In this talk, we develop an approach to find strategies that guarantee a property in systems that contain controllable, uncontrollable, and random vertices, resulting in probabilistic games. Such games are a reasonable abstraction of systems that comprise partial control over the system (reflected by controllable transitions), hostile nondeterminism (abstraction of the unknown, such as the behaviour of an attacker or a potentially hostile environment), and probabilistic transitions for the abstraction of unknown behaviour neutral to our goals. We exploit a simple and only mildly adjusted algorithm from the analysis of nonprobabilistic systems, and use it to show that the qualitative analysis of probabilistic games inherits the much celebrated sub-exponential complexity from 2-player games. The simple structure of the exploited algorithm allows us to offer tool support for finding the desired strategy, if it exists, for the given systems and properties. Our experimental evaluation shows that our technique is powerful enough to construct simple strategies that guarantee the specified probabilistic temporal properties. The talk is based on the CAV 2016 paper with the same title. It is joint work with Ernst Moritz Hahn, Andrea Turrini, and Lijun Zhang. The amazing thing about this approach is its simplicity and beauty. Instead of having a gadget based reduction to involved techniques, we use a straight-forward adaptation of a simple technique — and it turns out that 2.5 player games are not that hard to solve.

• Hugo Gimbert: A Class of Zielonka Automata with a Decidable Controller Synthesis Problem

  Authors:

  Abstract:

  The decidability of the distributed version of the Ramadge and Wonham control problem, where both the plant and the controllers are modelled as Zielonka automata is a challenging open problem. There exists three classes of plants for which the existence of a correct controller has been shown decidable in the distributed setting: when the dependency graph of actions is series-parallel, when the processes are connectedly communicating and when the dependency graph of processes is a tree. We generalize these three results by showing that a larger class of plants, called broadcast plants, has a decidable controller synthesis problem. We give new examples of plants for which controller synthesis is decidable.

• Michał Skrzypczak: Deciding the topological complexity of Büchi languages

  Authors: Michał Skrzypczak, Igor Walukiewicz

  Abstract:

  We study the topological complexity of languages of B\”uchi automata on infinite binary trees. We show that such a language is either Borel and WMSO-definable, or -complete and not WMSO-definable; moreover it can be algorithmically decided which of the two cases holds. The proof relies on a direct reduction to deciding the winner in a finite game with a regular winning condition. The paper has been accepted to ICALP 2016.

• Veronika Loitzenbauer: Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction

  Authors: Krishnendu Chatterjee (IST Austria), Wolfgang Dvorak (University of Vienna), Monika Henzinger (University of Vienna), and Veronika Loitzenbauer (University of Vienna)

  Abstract:

  Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental ω-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as reachability/safety (for disjunctive questions) and Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical ω-regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. The result was presented at LICS 2016 and a full version is available at http://arxiv.org/abs/1602.02670.

• Stefan Kiefer: Distinguishing Hidden Markov Chains

  Authors: Stefan Kiefer and A. Prasad Sistla

  Abstract:

  Hidden Markov Chains (HMCs) are commonly used mathematical models of probabilistic systems. They are employed in various fields such as speech recognition, signal processing, and biological sequence analysis. Motivated by applications in stochastic runtime verification, we consider the problem of distinguishing two given HMCs based on a single observation sequence that one of the HMCs generates. More precisely, given two HMCs and an observation sequence, a distinguishing algorithm is expected to identify the HMC that generates the observation sequence. Two HMCs are called distinguishable if for every epsilon > 0 there is a distinguishing algorithm whose error probability is less than epsilon. We show that one can decide in polynomial time whether two HMCs are distinguishable. Further, we present and analyze two distinguishing algorithms for distinguishable HMCs. The first algorithm makes a decision after processing a fixed number of observations, and it exhibits two-sided error. The second algorithm processes an unbounded number of observations, but the algorithm has only one-sided error. The error probability, for both algorithms, decays exponentially with the number of processed observations. We also provide an algorithm for distinguishing multiple HMCs. We apply our results to stochastic runtime verification, where a monitor should distinguish correct and faulty behaviour of a stochastic system.

• Mahsa Shirmohammadi: Minimal probabilistic automata have to make irrational choices

  Authors: Mahsa Shirmohammadi, Dmitry Chistikov, Stefan Kiefer, Ines Marusic and James Worrell

  Abstract:

  In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities. We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). NMF is the problem of decomposing a given nonnegative n*m matrix M into a product of a nonnegative n*d matrix W and a nonnegative d*m matrix H. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata. This talk is based on the paper titled “On Restricted Nonnegative Matrix Factorization”, that will be presented in ICALP 2016, and the unpublished manuscript titled “Nonnegative Matrix Factorization Requires Irrationality”, that is now online on Arxiv (https://arxiv.org/abs/1605.06848v1).

14:00–15:00 Session 2a – Database Theory (chair: Victor Vianu, room: Forum A)

• Dominik D. Freydenberger: Document Spanners: From Expressive Power to Decision Problems

  Authors: Dominik D. Freydenberger and Mario Holldack

  Abstract:

  We examine document spanners, a formal framework for information extraction that was introduced by Fagin, Kimelfeld, Reiss, and Vansummeren (PODS 2013, JACM 2015). A document spanner is a function that maps an input string to a relation over spans (intervals of positions of the string). We focus on document spanners that are defined by regex formulas, which are basically regular expressions with capture groups that map matched subexpressions to corresponding spans, and on core spanners, which extend regex formulas by a relational algebra. The main results are matching upper and lower bounds on the complexity of query evaluation and various aspects of static analysis. Most of these proofs require only little effort, as it is possible to use existing results on three different models from formal language theory and combinatorics on words: Pattern languages, word equations, and regular expressions with back references. This also illustrates how these models can be used as a general toolkit for query languages with string equality operators. This talk is based on the paper with the same name that appeared at ICDT 2016, which is a joint work with Mario Holldack, available at http://ddfy.de/publications/FH-DSFEPtDP.html

• Martin Schuster: Transducer-based Rewriting Games for Active XML

  Authors: Martin Schuster

  Abstract:

  Context-free games are two-player rewriting games that are played on nested strings representing XML documents with embedded function symbols. These games were introduced to model rewriting processes for intensional documents in the Active XML framework, where input documents are to be rewritten into a given target schema by calls to external services. This talk is based on a paper which studies the setting where dependencies between inputs and outputs of service calls are modelled by transducers. The paper defines transducer models operating on nested words and studies their properties, as well as the computational complexity of the winning problem for transducer-based context-free games in several scenarios. While the complexity of this problem is quite high in most settings (ranging from NP-complete to undecidable), some tractable restrictions are also identified. The paper corresponding to this talk has been accepted for MFCS 2016.

• Matthias Niewerth: Minimization of Tree Pattern Queries

  Authors:

  Abstract:

  We investigate minimization of tree pattern queries that use the child relation, descendant relation, node labels, and wildcards. We prove that minimization for such tree patterns is complete for the second level of the polynomial hierarchy and thus solve a problem first attacked by Flesca, Furfaro, and Masciari in 2003. We first provide an example that shows that tree patterns cannot be minimized by deleting nodes. This example shows that the M-NR conjecture, which states that minimality of tree patterns is equivalent to their nonredundancy, is false. We then show how the example can be turned into a gadget that allows us to prove hardness. The paper will be presented at PODS 2016.

• Jan Van den Bussche: On the satisfiability problem for SPARQL patterns

  Authors: Jan Van den Bussche, Xiaowang Zhang and François Picalausa

  Abstract:

  Introduction SPARQL is the standard query language for data in RDF, in turn the standard data format for the Semantic Web. There are some significant differences between SPARQL and the relational algebra for the classical relational data model. First, queries do not access relations directly but rather perform pattern matching on RDF triples. Patterns may match only partially, so that the result of a query is a heterogeneous relation; different tuples in the result may be defined on different sets of variables. Such partial matching is made possible by the OPTIONAL operator. Relationally, OPTIONAL may be viewed as an outer join operator. The classical natural join operator is present in SPARQL as well. In contrast, set difference, or another explicit form of negation, was absent in the original design of SPARQL. The only feature that comes close to negation are negated bound constraints: the ability to express the condition that a certain variable from the pattern is not matched. Whereas an explicit difference operator (MINUS) was later added in version 1.1 of SPARQL, researchers have been interested in investigating the theoretical foundations of the original SPARQL language [PAG09, AP11, AFK+16, KK16]. We are intrigued by this language as a new, heterogeneous variant of the classical relational algebra that gives equal weight to outer join and natural join. Indeed, while there already existed studies focusing on outer join in the relational setting [GLR97], the expressive power of outer join in interplay with other query operators has only become a research topic thanks to the new SPARQL context. Results We have investigated the decidability of the satisfiability problem for SPARQL patterns. Our starting point is the known observation that MINUS can already be expressed in basic SPARQL by exploiting negated bound constraints [AP11]. So, the addition of MINUS in SPARQL 1.1 is just syntactic sugar. As a consequence, basic SPARQL has the full power of relational algebra and satisfiability if undecidable. We want to understand what happens when the use of constraints in patterns is restricted. We distinguish six kinds of constraints: equalities, constant-equalities, bound constraints, and their respective negations. Our main result is that as soon as inconsistent constraints can be formulated, satisfiability becomes undecidable. So, not only negated bound constraints, but also conjunctions of equalities and inequalities, or just constant equalities by themselves, already cause undecidability. Indeed, we show that MINUS can also be expressed using these constraints instead of negated bound constraints. Conversely, when inconsistent constraints cannot be formulated, satisfiability is shown to be decidable, and a finite model property is observed. The problem is NP-complete, even in the simple case of OPTIONAL-free patterns that use only bound constraints. In the special case of well-designed SPARQL patterns [PAG09], satisfiability is also decidable and in polynomial time. This is joint work with Xiaowang Zhang and François Picalausa. A full article on this research has recently been accepted (pending minor revisions) in the Journal of Artificial Intelligence Research. References [AFK+16] S. Ahmetaj, W. Fischl, M. Kr ̈oll, R. Pichler, M. Sˇimkus, and S. Skritek. The challenge of optional matching in SPARQL. In M. Gyssens and G. Simari, editors, Proceedings 9th International Symposium on Foundations of Information and Knowledge Systems, volume 9616 of Lecture Notes in Computer Science, pages 169–190, 2016. [AP11] M. Arenas and J. P ́erez. Querying semantic web data with SPARQL. In Proceedings 30st ACM Symposium on Principles of Databases, pages 305–316. ACM, 2011. [GLR97] C. Galindo-Legaria and A. Rosenthal. Outerjoin simplification and reordering for query optimization. ACM Transactions on Database Systems, 22(1):43–74, 1997. [KK16] M. Kaminski and E.V. Kostylev. Beyond well-designed SPARQL. In Proceedings 19th International Conference on Database Theory, 2016. [PAG09] J. P ́erez, M. Arenas, and C. Gutierrez. Semantics and complexity of SPARQL. ACM Transactions on Database Systems, 34(3):article 16, 2009.

• Antoine Amarilli: Probabilities and Provenance on Trees and Treelike Instances

  Authors: Antoine Amarilli, Pierre Bourhis, Pierre Senellart

  Abstract:

  We present our recent results at PODS 2016 and ICALP 2015 about the evaluation of queries on probabilistic databases and graphs. Our upper bound result shows that this task can be efficiently performed (in data complexity, i.e., for a fixed query) for Boolean Monadic Second-Order (MSO) queries, on databases of treewidth bounded by a constant. We do so using Courcelle’s method of compiling MSO to tree automata, and extend it to compute probabilities, via a provenance representation that describes which possible worlds satisfy the query. Our lower bound shows that, on graphs, there is a first-order query which is always intractable to evaluate on database families of unbounded treewidth (under a constructibility assumption), no matter which other restrictions we impose on the databases.

14:00–15:00 Session 2b – Topology & Linear Systems (chair: Jacques Duparc, room: Forum B)

• Benedikt Brütsch: Playing Games in the Baire Space

  Authors: Benedikt Brütsch and Wolfgang Thomas

  Abstract:

  We solve a generalized version of Church’s synthesis problem where the alphabet is not a finite set like {0,1} but the set of natural numbers. This amounts to solving a Gale-Stewart game where a play is a sequence of natural numbers (chosen in alternation by two players Input and Output) rather than a sequence of bits; so a play is an element of the Baire space rather than of the Cantor space. To represent the winning condition L ⊆ ℕ^ω for player Output, we present a natural model of automata (“ℕ-memory automata”) equipped with the parity acceptance condition, and we introduce also the corresponding model of “ℕ-memory transducers”. We show that for games specified by ℕ-memory automata, it is decidable whether player Output has a winning strategy, and that in this case an ℕ-memory transducer can be constructed that implements a winning strategy for player Output. This talk is based on the following paper: Benedikt Brütsch and Wolfgang Thomas: Playing Games in the Baire Space. To appear in Proceedings of the Cassting Workshop on Games for the Synthesis of Complex Systems (Cassting 2016).

• Louis Vuilleumier: Towards a better Understanding of the Scott Domain

  Authors:

  Abstract:

  The Scott domain — P(N) endowed with the topology generated by the basis {{X ⊆ N | F ⊆ X} | F finite subset of N} — is fundamental for several reasons. First, from a descriptive set theoretical point of view, Matthew de Brecht showed in [dB13] that it is a counterpart of the Baire space in a generalization of descriptive set theory to the more general class of second countable complete quasi-metrizable spaces. As it is a domain, it is also strongly connected to both logic and computer science (see the introduction of the recent book of Jean Goubault-Larrecq [GL13]). On a more practical side, it is well known that the Scott domain is a standard model of λ-calculus, as Dana Scott showed in [Sco76]. We propose a game characterization of the notion of continuous reductions in the Scott domain. It allows us to investigate the topological complexity of the subsets of the Scott domain. In particular, the game characterization provides arbitrarily large finite antichains with respect to the quasi-order induced by continuous reducibility. [This talk does not correspond to an accepted or published paper]

• Michaël Cadilhac: Continuity: a study of transduction composability

  Authors: Olivier Carton and Charles Paperman

  Abstract:

  A function is continuous for a class of languages V if its inverse maps elements of V back to V. Semantically, this means that if we are provided a circuit for a language L in V, then putting the function at the input level results in a language that is still in V. This notion has been used with different values of V to characterize the transductions computable in classes of low complexity. Here, we report on problems focusing only on this notion over transductions; we provide decidability properties and characterize continuity through some natural algebraic properties. Unpublished joint work with Olivier Carton and Charles Paperman.

• Ventsislav Chonev: On Recurrent Reachability for Continuous Linear Dynamical Systems

  Authors:

  Abstract:

  The continuous evolution of a wide variety of systems, including continuous-time Markov chains and linear hybrid automata, can be described in terms of linear differential equations. In this presentation we focus on the decision problem of whether the solution of a system of linear differential equations reaches a target halfspace infinitely often. This recurrent reachability problem can equivalently be formulated as the following Infinite Zeros Problem: does a real-valued function satisfying a given linear differential equation have infinitely many zeros on the non-negative reals? In our publication at LICS’16, we establish decidability in the case of a differential equation of order at most 7. On the other hand, in the same paper we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision. In this presentation, we will offer a high-level overview of the problem, followed by an outline of the techniques from model theory and transcendental number theory which proved most useful in establishing our results.

• Vladimir Gusev: Primitive sets of nonnegative matrices and synchronizing automata

  Authors: Balázs Gerencsér, Vladimir V. Gusev, Raphaël M. Jungers

  Abstract:

  A set of nonnegative matrices M={M_1, M_2, …, M_k} is called PRIMITIVE if there exist indices i_1, i_2, …, i_m such that the product M_{i_1} M_{i_2} … M_{i_m} is positive (i.e. has all its entries >0). The length of the shortest such product is called the EXPONENT of M. The concept of primitive sets of matrices comes up in a number of problems within control theory, non-homogeneous Markov chains etc. In my talk I will speak about the recently discovered connections between synchronizing automata and primitive sets of matrices. An automaton is called SYNCHRONIZING if there exist a word w and a state f such that the action of w brings all states to f. On one hand, the properties of synchronizing automata are relatively well studied due to their applications to industrial automation, coding theory, group theory, etc. On the other hand, there is still a persisting interest of the research community to the topic due to one of the most famous open problems in automata theory. Namely, the CERNY CONJECTURE states that the length of the shortest synchronizing word of an n-state automaton is at most (n-1)^2. In my talk I will explain how the aforementioned connections lead to a relatively large number of results about primitive sets of matrices. Namely, we will see that the maximal exponent among all primitive sets of n by n matrices is roughly equal to 3^(n/3). Furthermore, the problem of deciding whether a given set of matrices is primitive is PSPACE-complete. In my talk the set of matrices with no zero rows and columns, denoted by NZ, will receive a special attention due to its intriguing connections to the Cerny conjecture and the recent generalization of Perron-Frobenius theory for this class. I will characterize the computational complexity of different problems related to the exponent of NZ matrix sets, and present a quadratic bound on the exponents of sets belonging to a special subclass. Namely, we will see that the exponent of a set of matrices having total support is bounded by 2n^2 -5n +5. These results are not published. The preprint is available on http://arxiv.org/abs/1602.07556.

15:30–16:30 Session 3a – Synthesis & Timed Systems (chair: Véronique Bruyère, room: Forum A)

• Romain Brenguier: Optimal Assumptions for Synthesis

  Authors:

  Abstract:

  Synthesis is the process of constructing a correct system automatically from its specification. For reactive systems, this often requires assumptions about the behaviour of the environment. It is difficult for the designer to identify the assumptions that ensures the existence of a correct controller, and doing so manually can lead to assumptions that are stronger than necessary. As a consequence the generated controllers are sub-optimal in terms of generality and robustness. In this work, given a specification, we identify the weakest assumptions that ensures the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that speaks only about inputs of the systems. We show that optimal assumptions correspond to strongly winning strategies, admissible strategies and remorse-free strategies respectively. Based on this correspondence, we propose an algorithm for computing optimal assumptions that can be ensured by the environment.

• Dietmar Berwanger: Recovering Incomplete Information

  Authors: Dietmar Berwanger and R. Ramanujam

  Abstract:

  Coordination problems at the crux of distributed systems are highly sensitive to the information that agents have about the game and the actual play. There is abundant literature on the challenge of imperfect information, that is, the situation when agents are not perfectly informed about the play history — in the setting, however, that the structure of the game is common knowledge among them. In this talk, we discuss the situation where players are uncertain about the structure of the game that is being played: the actual winning condition and the choices available to the players are drawn by Nature from a finite set of alternatives. In classical game theory, this is called incomplete information — in contrast to imperfect information; in the computing literature, the terms have been thoroughly confused. Of course, the combination of incomplete with imperfect information in games of infinite duration leaves little hope for computational tractability in general. We show that it is decidable whether the players have a joint strategy to recover the incomplete information about the game structure, for a significant particular case where each player is perfectly informed about the global state, but not about the actions of the other players. As a prominent application, we prove that it is decidable whether the grand coalition has a joint strategy that allows to detect unilateral deviations in the setting of infinite games with private monitoring of moves. This is joint work with R. Ramanujam (IMSc Chennai). Unpublished.

• Benjamin Monmege: Real-Time Synthesis is Hard!

  Authors: Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege and Nathalie Sznajder

  Abstract:

  We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D’Souza et al. and Bouyer et al.). During this talk, we precise the decidability border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it. This is joint work (submitted at FORMATS 2016) with Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho, and Nathalie Sznajder.

• Engel Lefaucheux: Simple Priced Timed Games are not That Simple

  Authors: Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, Benjamin Monmege

  Abstract:

  Article published in FSTTCS 2015. Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).

• Ocan Sankur: An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP

  Authors:

  Abstract:

  We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization proto- cols. We develop abstraction techniques for parameterized model check- ing of such protocols under arbitrary network topologies, where nodes have independently evolving clocks. We apply our technique for model checking the root election part of the flooding time synchronisation pro- tocol (FTSP), and obtain improved results compared to previous work. We model check the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter.

15:30–16:30 Sessions 3b – Logic & Automata (chair: Szymon Torunczyk, room: Forum B)

• Christopher Hahn: Deciding Hyperproperties

  Authors: Bernd Finkbeiner and Christopher Hahn

  Abstract:

  This talk is based on the paper “Deciding Hyperproperties” by Bernd Finkbeiner and Christopher Hahn, which appeared on the 27th International Conference on Concurrency Theory (CONCUR 2016). Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. We study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall formulas, and undecidable for forall-exists formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.

• Martin Jonas: Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

  Authors:

  Abstract:

  We described a new approach to deciding satisfiability of quantified bit-vector formulas using binary decision diagrams and approximations. The approach is motivated by the observation that the binary decision diagram for a quantified formula is typically significantly smaller than the diagram for the subformula within the quantifier scope. The approach relies on the combination of syntactic formula simplifications, tailored initial ordering of BDD variables, and using underapproximations and overapproximations, all of which help to reduce the size of the BDDs during the computation of the BDD corresponding to the input formula. The suggested approach has been implemented in the experimental open-source SMT solver called Q3B. The experimental results show that it decides more benchmarks from the SMT-LIB repository than state-of-the-art SMT solvers for this theory, namely Z3 and CVC4, which solve quantified bit-vector formulas using the quantifier instantiation. Furthermore, we compared the implemented solver with the mentioned state-of-the art solvers on the quantified formulas produced by the symbolic model checker SymDIVINE. Again, the BDD based solver was able to decide more queries than Z3 and CVC4. Moreover, according to the preliminary results of the SMT competition 2016, Q3B is the best solver in the category of quantified bit-vectors, outperforming Z3, CVC4 and Boolector. Underapproximations used in the approach are performed by reducing the bit-width of all existentially quantified variables. Similarly, overapproximations are performed by reducing the bit-width of all existentially quantified variables. We describe several ways of reducing bit-width of a variable and we evaluate the effect of each of these on the performance of the solver. The publication with the detailed description of the approach, experimental results, and the evaluation of all three components used in the approach was accepted to SAT 2016.

• Markus L. Schmid: On the Complexity of Grammar-Based Compression over Fixed Alphabets

  Authors: Katrin Casel, Henning Fernau, Serge Gaspers, Benjamin Gras, Markus L. Schmid

  Abstract:

  This talk is based on the following paper: Katrin Casel, Henning Fernau, Serge Gaspers, Benjamin Gras, Markus L. Schmid. On the Complexity of Grammar-Based Compression over Fixed Alphabets. 43rd International Colloquium on Automata, Languages, and Programming 2016, ICALP 2016. We investigate the complexity of grammar-based compression, i.e., to compress a word by a context-free grammar. It is shown that the shortest-grammar problem remains NP-complete if the alphabet is fixed and has a size of at least 24 (which settles an open question). On the other hand, this problem can be solved in polynomial-time, if the number of nonterminals is bounded, which is shown by encoding the problem as a problem on graphs with interval structure. Furthermore, we present an O(3^n) exact exponential-time algorithm, based on dynamic programming. Similar results are also given for 1-level grammars, i.e., grammars for which only the start rule contains nonterminals on the right side (thus, investigating the impact of the “hierarchical depth” on the complexity of the shortest-grammar problem).

• Wojciech Czerwiński: Separability of Reachability Sets of Vector Addition Systems

  Authors:

  Abstract:

  The separability problem of sets from a class G by a set from a class F asks whether for two given sets U, V in G there exists a set S in F such that U is included in S and V has an empty intersection with S. We show that separability problem of reachability sets of Vector Addition Systems by both modular and unary sets is decidable.

• Karin Quaas: Synchronizing Data Words for Register Automata

  Authors: Karin Quaas, Parvaneh Babari and Mahsa Shirmohammadi

  Abstract:

  Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with only 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and it is in NLOGSPACE for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is coNEXTPTIME-complete. This is joint work with Parvaneh Babari (University of Leipzig) and Mahsa Shirmohammadi (University of Oxford), accepted at MFCS 2016.

16:30–16:45 Break

16:45–18:15 Invited Session 1 – Transducers (Organizer: Anca Muscholl, room: Forum A)

• Emmanuel Filiot: Automata, Logic and Algebra for Word Transductions

  Authors:

  Abstract:

  This talk will survey old and recent results about word transductions, i.e. functions mapping (finite) words to words. Connections between automata models (transducers), logic and algebra will be presented. Starting with rational functions, defined by (one-way) finite transducers, and the canonical model of bimachines introduced by Reutenauer and Schützenberger, the talk will also target the more expressive class of functions defined by two-way transducers and their equivalent MSO-based formalism.

• Helmut Seidl: Equivalence of Deterministic Tree-to-String Transducers is Decidable

  Authors: Joint work with Sebastian Maneth (Edinburgh) and Gregor Kemper (München)

  Abstract:

  Top-down tree-to-string transducers recursively process their structured input data while producing output in an unstructured way, namely as a string. Let yDT denote the class of all deterministic top-down tree-to-string transducers. In the presentation, we show that equivalence of two such transducers is decidable – a problem which has been open for more than 30 years. As non-equivalence can be witnessed by an input on which the two transducers differ, decidability of equivalence follows if only an effective proof system can be provided for certifying equivalence whenever it holds. We indicate how such a proof system can be constructed using powerful techniques from commutative algebra. While in general not much is known about the complexity of the decision problem, we also present special cases where polynomial upper bounds can be obtained.

9:00–10:00 KEYNOTE 2 (chair: Paul Gastin, room: Forum A)

• Meena Mahajan (CIT Chennai): Arithmetic Circuits: Classes, Structure, Completeness …

  Authors:

  Abstract:

  In this talk I will review recent developments in algebraic complexity theory. I will outline some major results concerning structure, completeness and closure. I will describe some techniques that have been central to obtaining these results, including extreme depth reduction, partial derivatives, and padding.

10:30–11:45 Sessions 5 – (Finite) Model Theory (chair: Jan van den Bussche, room: Forum A)

• Lucas Heimberg: Hanf normal form for first-order logic with unary counting quantifiers

  Authors: Lucas Heimberg, Dietrich Kuske, and Nicole Schweikardt

  Abstract:

  This talk is based on the paper “Hanf normal form for first-order logic with unary counting quantifiers” co-authored by Lucas Heimberg (Humboldt-Universität zu Berlin), Dietrich Kuske (Technische Universität Ilmenau), and Nicole Schweikardt (Humboldt-Universität zu Berlin), which got accepted for LICS 2016. The paper can be downloaded under http://www2.informatik.hu-berlin.de/logik/research/HKS-LICS16.pdf . We study the existence of Hanf normal forms for extensions FO(Qs) of first-order logic by sets Qs of unary counting quantifiers, i.e., sets of subsets of the natural numbers. A formula is in Hanf normal form if it is a Boolean combination of formulas zeta describing the isomorphism type of a local neighbourhood around its free variables and statements of the form “the number of witnesses y of psi(y) belongs to (Q+k)” where Q in Qs, k is a natural number, and psi describes the isomorphism type of a local neighbourhood around its unique free variable y. We show that a formula from FO(Qs) can be transformed into a formula in Hanf normal form that is equivalent on all structures of degree at most d if, and only if, all counting quantifiers occurring in the formula are ultimately periodic. This transformation can be carried out in worst-case optimal 3-fold exponential time. In particular, this yields an algorithmic version of Nurmonen’s extension of Hanf’s theorem for first-order logic with modulo-counting quantifiers. As an immediate consequence, we obtain that on finite structures of degree at most d, model checking of first-order logic with modulo-counting quantifiers is fixed-parameter tractable.

• Marlin Frickenschmidt: Order Invariance on Decomposable Structures

  Authors: Michael Elberfeld, Marlin Frickenschmidt and Martin Grohe

  Abstract:

  Order-invariant formulas access an ordering on a structure’s universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic second-order (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of bounded width). While order-invariant MSO is more expressive than MSO and, even, CMSO (MSO with modulo-counting predicates), we show that order-invariant MSO and CMSO are equally expressive on graphs of bounded tree width and on planar graphs. This extends an earlier result for trees due to Courcelle. Moreover, we show that all properties definable in order-invariant FO are also definable in MSO on these classes. These results are applications of a theorem that shows how to lift up definability results for order-invariant logics from the bags of a graph’s tree decomposition to the graph itself. This is joint work with Michael Elberfeld and Martin Grohe. It was accepted to LICS 2016.

• Nils Vortmeier: Dynamic descriptive complexity of FO-definable modifications

  Authors: Thomas Schwentick, Nils Vortmeier and Thomas Zeume

  Abstract:

  A dynamic program, as introduced by Dong, Su and Topor and Patnaik and Immerman, maintains the result of a fixed query for an input database which is subject to modifications. It can use an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. In the original setting, only insertions and deletions of single tuples are considered. In this talk, which is based on joint work with Thomas Schwentick and Thomas Zeume, we will allow modifications defined by (restricted) first-order formulas and review which queries can still be maintained. This talk is based on so far unpublished work.

• Paweł Parys: The MSO+U Theory of (N, <) Is Undecidable

  Authors: Mikołaj Bojańczyk, Paweł Parys and Szymon Toruńczyk

  Abstract:

  We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N, <) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory. This work was published on STACS 2016.

• Michał Pilipczuk: Definability equals recognizability for graphs of bounded treewidth

  Authors: Mikołaj Bojańczyk and Michał Pilipczuk

  Abstract:

  We prove a conjecture of Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the following sense: constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. While the forward implication is a classic fact known as Courcelle’s theorem, the converse direction remained open. The talk will be based on a joint work with Mikołaj Bojańczyk, presented at LICS 2016. The preprint is available on arxiv: http://arxiv.org/abs/1605.03045

• Mikolaj Bojanczyk: A Proof of Courcelle’s Conjecture on Recognisable Graph Classes

  Authors: Mikolaj Bojanczyk

  Abstract:

  Courcelle’s conjecture says that for classes of bounded treewidth, definability in MSO is the same as recognisability. More precisely, consider the following notions: (D) a class of graphs is called MSO definable if it can be defined in monadic second-order logic (with counting quantifiers). (R) a class of graphs is called recognisable if for each k there is a tree automaton which recognises width k tree decompositions of graphs satisfying the property. Many natural graph classes are easily seen to satisfy (D), e.g. graphs with Hamiltonian (or Euler) paths, or 3-colourable graphs. Courcelle’s Theorem says that (D) implies (R). Courcelle’s Conjecture says that (R) implies (D) for classes of bounded tree width. In the talk, I will discuss a proof of this conjecture. Slides https://www.mimuw.edu.pl/~bojan/slides/graph-reco/ (Joint work with Michał Pilipczuk)

  Download presentation

10:45–12:00 Break

12:00–12:50 Sessions 6 – Verification (chair: Ranko Lazic, room: Forum A)

• Martin Zimmermann: Visibly Linear Dynamic Logic

  Authors:

  Abstract:

• Laurent Doyen: Computation Tree Logic for Synchronization Properties

  Authors: Krishnendu Chatterjee and Laurent Doyen

  Abstract:

  We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. The talk is based on a joint work with Krishnendu Chatterjee (accepted at ICALP 2016)

• Marie Fortin: On parametrized verification of asynchronous, shared-memory pushdown systems

  Authors: joint work with Anca Muscholl and Igor Walukiewicz

  Abstract:

  We consider here parametrized asynchronous shared-memory pushdown systems, as introduced by Hague. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Hague’11], [Esparza, Ganty, Majumdar’13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar’15]. We show that the liveness problem is PSPACE-complete. We also consider the universal reachability problem, and show that it is decidable, moreover coNEXPTIME-complete. These results imply that verification of regular properties of traces, satisfying some stuttering condition, is also decidable in NEXPTIME.

• Victor Vianu: Verification of Hierarchical Artifact Systems

  Authors: Alin Deutsch, Yuliang Li and Victor Vianu

  Abstract:

  The proposed talk will present results from a PODS 2016 paper with the same title, co-authored with Alin Deutsch and Yuliang Li (UC San Diego). The past decade has witnessed the evolution of workflow specification frameworks from the traditional process-centric approach towards data-awareness. Process-centric formalisms focus on control flow while under-specifying the underlying data and its manipulations by the process tasks, often abstracting them away completely. In contrast, data-aware formalisms treat data as first-class citizens. A notable exponent of this class is IBM’s business artifact model which has been successfully deployed in practice and adopted in industrial standards. In a nutshell, artifacts consist of data that is updated by a set of services that implement business process tasks, specified declaratively by pre-and-post conditions. IBM has developed several variants of artifacts, of which the most recent is Guard-Stage-Milestone (GSM). The GSM approach provides rich structuring mechanisms for services, including parallelism, concurrency and hierarchy, and has been incorporated in the OMG standard for Case Management Model and Notation (CMMN). The artifact approach has spawned a rich body of research in academia, focused primarily on verification. The present work represents a significant advance on the artifact verification problem on several fronts. We consider a much richer and more realistic model, called Hierarchical Artifact System (HAS), abstracting core elements of the GSM model. In particular, the model features task hierarchy, concurrency, and richer artifact data (including updatable artifact relations). We consider properties expressed in a novel hierarchical temporal logic, HLTL-FO, that is well-suited to the model. Our main results establish the complexity of checking HLTL-FO properties for various classes of HAS, highlighting the impact of various features on verification. The results require qualitatively new techniques, because the reduction to finite-state model checking used in previous work is no longer possible. Instead, the richer model requires the use of a hierarchy of Vector Addition Systems with States (VASS). The arithmetic constraints are handled using quantifier elimination techniques, adapted to our setting. The talk will present some of the mathematical intuition behind the results, focusing on two of my favorite aspects: (i) the use of Vector Addition Systems to handle unbounded evolving data, and (ii) the new hierarchical variant of LTL-FO.

14:15–15:15 Session 7a – Vector Addition Systems & Petri Nets (chair: Marc Zeitoun, room: Forum A)

• Ranko Lazic: Reachability in two-dimensional unary vector addition systems with states is NL-complete

  Authors: Matthias Englert, Ranko Lazic and Patrick Totzke

  Abstract:

  Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space. Joint work with Matthias Englert and Patrick Totzke, to appear in LICS 2016. Available from: http://arxiv.org/abs/1602.00477

• Patrick Totzke: A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

  Authors: with Stefan Göller, Christoph Haase and Ranko Lazic

  Abstract:

  I propose to present recent and ongoing work on Branching Vector Addition System (BVASS), that extend Vector Addition Systems with special branching transitions like in tree automata. When performing a branching step, the counter values are distributed non-deterministically between two successor processes. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. Our recent result is that the reachability, coverability and boundedness problems are polynomial-time complete for BVASS in dimension one. Regarding the reachability problem, this is the first decidability result in a subclass of BVASS known so far. This is joint work with Stefan G\”oller, Christoph Haase and Ranko Lazi\’c, to be published at ICALP’16 under the same name and also available here: http://arxiv.org/abs/1602.05547

• Reino Niskanen: Undecidability of Two-dimensional Robot Games

  Authors: joint with Igor Potapov (Liverpool) and Julien Reichert

  Abstract:

  Robot game is a two-player vector addition game played on the integer lattice . Both players have sets of vectors and in each turn the vector chosen by a player is added to the current configuration vector of the game. One of the players, called Eve, tries to play the game from the initial configuration to the origin while the other player, Adam, tries to avoid the origin. The problem is to decide whether or not Eve has a winning strategy. In this talk we prove undecidability of the robot game in dimension two answering the question formulated by Doyen and Rabinovich in 2011 and closing the gap between undecidable and decidable cases. The talk is based on joint work with Igor Potapov (Liverpool) and Julien Reichert (Cachan) and has been accepted to MFCS 2016.

• Sylvain Schmitz: The Complexity of Coverability in ν-Petri Nets

  Authors: with R. Lazić

  Abstract:

  We show that the coverability problem in ν-Petri nets is complete for ‘double Ackermann’ time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes ν-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals. Joint work with R. Lazić presented at LICS’16; preprint available from https://hal.inria.fr/hal-01265302.

• Sławomir Lasota: Decidability border for Petri nets with data: WQO dichotomy conjecture

  Authors:

  Abstract:

  In Petri nets with data, every token carries a data value, and executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems for Petri nets with data may depend on the structure of data domain. For instance, if data values are only tested for equality, decidability status of the reachability problem is unknown (but decidability is conjectured). On the other hand, the reachability problem is undecidable if data values are additionally equipped with a total ordering. We investigate the frontiers of decidability for Petri nets with various data, and formulate the WQO Dichotomy Conjecture: under a mild assumption, either a data domain exhibits a well quasi-order (in which case one can apply the general setting of well-structured transition systems to solve problems like coverability or boundedness), or essentially all the decision problems are undecidable for Petri nets over that data domain. This topic is to be presented as an invited talk at PN’16 (37th INTERNATIONAL CONFERENCE ON APPLICATIONS AND THEORY OF PETRI NETS AND CONCURRENCY).

14:15–15:15 Session 7b – ("Non-quantitative") Games (chair: Dietmar Berwanger, room: Forum B)

• Karoliina Lehtinen: The non-deterministic fragment of modal mu

  Authors:

  Abstract:

  The modal calculus and parity automata are closely related. However, modal operates on arbitrary labelled transition systems while automata are usually defined only on infinite trees with one successor per label. This seemingly harmless difference has suprising consequences. Non-deterministic automata for example can be generalised to arbitrary labelling systems and used to define the non-deterministic fragment of modal . I argue that this fragment is less powerful than disjunctive modal mu, the fragment of modal mu originally conceived in order to mimic non-determinism in automata. It also has unique properties which suggest that this might be a rare example of a non-trivial fragment of modal for which deciding the alternation hierarchy might be within reach. In any case, its index-problem is distinct from the index-problem for non-deterministic automata. The take-away of this talk is that the relationship between automata theory and the modal mu calculus has its pitfalls and we have to take adequate care when moving between the two theories.

• Antonio Di Stasio: Solving Parity Games Using An Automata-Based Algorithm

  Authors: joint with Aniello Murano, Giuseppe Perelli and Moshe Vardi

  Abstract:

  Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime \cap CoUPTime and deciding whether a polynomial time solution exists is a long-standing open question. In the last two decades, a variety of algorithms have been proposed. Many of them have been also implemented in a platform named PGSolver. This has enabled an empirical evaluation of these algorithms and a better understanding of their relative merits. In this paper, we further contribute to this subject by implementing, for the first time, an algorithm based on alternating automata. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games where the number of priorities is relatively small. This makes the new algorithm quite useful in practice. This is joint work with Aniello Murano, Giuseppe Perelli and Moshe Vardi. The paper has been accepted in the 21° International Conference on Implementation and Application of Automata, CIAA 2016.

• Stephane Le Roux: Extending finite-memory determinacy by boolean combination of winning conditions

  Authors: Stephane Le Roux and Arno Pauly

  Abstract:

  This talk considers turn-based, infinite duration, two-player, win/lose games played on finite graphs. In the literature, who wins a play is defined via winning conditions such as Muller, energy, reachability, mean-payoff, etc. The usual winning conditions guarantee the existence of winning strategies that are simple enough to be implemented via finite automata. This guarantee is called finite-memory determinacy. Advanced modeling may involve combinations of the usual winning conditions mentioned above. Finite-memory determinacy may or may not be preserved by such combinations. I will describe a criterion for boolean combinations of winning conditions to preserve this determinacy. The criterion is general enough to imply finite-memory determinacy of energy Muller games, multi-dimensional bounded energy games, etc.

• Denis Kuperberg: Soundness in Negotiations

  Authors: Javier Esparza, Denis Kuperberg, Anca Muscholl, Igor Walukiewicz

  Abstract:

  Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of a negotiation is PSPACE-complete, and in PTIME if the negotiation is deterministic. They have also provided an algorithm for an intermediate class of acyclic, non-deterministic negotiations, but left the complexity of the soundness problem open. In the first part of this paper we study two further analysis problems for sound acyclic deterministic negotiations, called the race and the omission problem, and give polynomial algorithms. We use these results to provide the first polynomial algorithm for some analysis problems of workflow nets with data previously studied by Trcka, van der Aalst, and Sidorova. In the second part we solve the open question of Esparza and Desel’s paper. We show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes.

• Quentin Hautem: Window parity games: an alternative approach toward parity games with time bounds

  Authors: joint work with Véronique Bruyère and Mickael Randour

  Abstract:

  Classical objectives in two-player zero-sum games played on graphs often deal with limit behaviors of infinite plays: e.g., mean-payoff and total-payoff in the quantitative setting, or parity in the qualitative one (a canonical way to encode w-regular properties). Those objectives offer powerful abstraction mechanisms and often yield nice properties such as memoryless determinacy. However, their very nature provides no guarantee on time bounds within which something good can be witnessed. In this work, we consider two approaches toward inclusion of time bounds in parity games. The first one, parity-response games, is based on the notion of finitary parity games and parity games with costs. The second one, window parity games, is inspired by window mean-payoff games. We compare the two approaches and show that while they prove to be equivalent in some contexts, window parity games offer a more tractable alternative when the time bound is given as a parameter (P vs PSPACE). In particular, it provides a conservative approximation of parity games computable in polynomial time. Furthermore, we extend both approaches to the multi-dimension setting. We give the full picture for both types of games with regard to complexity and memory bounds.

15:45–16:45 Session 8a – Stochastic Systems & Games (chair: Hugo Gimbert, room: Forum A)

• Marco Faella: Average Controllability Measures for One-player Games

  Authors:

  Abstract:

  In this talk, I will discuss several ways to measure the extent to which a player can exert control over a one-player stochastic game, relating them to the existing literature on the “skill vs chance” dichotomy. I will focus on measures that depend only on the rules of the games, and not on how people actually play them. After outlining a set of desirable properties, I will observe that two statistical measures of effect size, known as “percentage of standard deviation explained” and “percentage of absolute deviation explained”, satisfy them but give rise to two different orders between games. Finally, I will present numerical estimates of these measures for several well-known games and a sport. The reason for targeting average controllability, rather than minimum or maximum controllability, stems from the observation that the first may more accurately approximate the behavior of a population of players of various skill levels. After all, min, average, and max are the three canonical points in the spectrum of rationality, with bounded rationality à la Simon and actual human players arguably positioned somewhere between the second and the third point. This talk is based on a paper presented at AAMAS 2016.

• Lubos Korenciak: Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration

  Authors:

  Abstract:

  We consider the fixed-delay synthesis problem for continuous-time Markov chains extended with fixed-delay transitions (fdCTMC). The goal is to synthesize concrete values of the fixed-delays (timeouts) that minimize the expected total cost incurred before reaching a given set of target states. The same problem has been considered and solved in previous works by computing an optimal policy in a certain discrete-time Markov decision process with a huge number of actions that correspond to suitably discretized values of the timeouts. In this paper, we design a symbolic fixed-delay synthesis algorithm which avoids the explicit construction of large action spaces. Instead, the algorithm computes a small sets of “promising” candidate actions on demand. The candidate actions are selected by minimizing a certain objective function by computing its symbolic derivative and extracting a univariate polynomial whose roots are precisely the points where the derivative takes zero value. Since roots of high degree univariate polynomials can be isolated very efficiently using modern mathematical software, we achieve not only drastic memory savings but also speedup by three orders of magnitude compared to the previous methods. This work was submitted to the MASCOTS 2016 conference.

• Thomas Brihaye: Decisive stochastic processes

  Authors: with Nathalie Bertrand, Patricia Bouyer and Pierre Carlier

  Abstract:

  In 2007, Abdulla et al. introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov processes and stochastic timed automata. The results presented in this abstract are issued from a joint paper with Nathalie Bertrand, Patricia Bouyer and Pierre Carlier entitled Analysing decisive stochastic processes accepted to ICALP 2016.

• Marcin Przybyłko: On the Complexity of Branching Games with Regular Conditions

  Authors: This is a joint work with with Michał Skrzypczak from University of Warsaw.

  Abstract:

  Infinite duration games are one of the crucial tools in the areas of verification and synthesis. Introduced by M. Mio, branching games (aka. tree games) are a variant of infinite duration games and extend the “standard” definition by adding so-called branching vertices. Branching vertices split the flow of the game into independent sub-games, rendering the outcome of the game — the play — to be an infinite tree and not simply an infinite word. Therefore, the winner of the play is determined by a winning condition specified as a property of a tree, as opposed to being specified as a property of a single path. In this talk, I will address the question of determinacy of a branching game and the problem of computing the optimal game value for each of the players when the winning conditions are regular, i.e. the set of winning plays is a regular language of trees. I will consider both: the stochastic and non-stochastic variants of the games and allow for the use of randomised strategies. The results can be summarised as follows. In general, branching games are not determined under mixed strategies. This holds even for topologically simple winning conditions (differences of two open sets) and non-stochastic arenas. Nevertheless, the games become determined under mixed strategies if we restrict the winning conditions to open sets of trees. The problem of comparing the game value to a rational threshold is undecidable for branching games with regular conditions in all non-trivial stochastic cases. In the non-stochastic cases the problem is decidable and we provide exact bounds on the complexity of the problem. The only case left open is the 0-player stochastic case, i.e. the problem of computing the measure of a given regular language of infinite trees. The underlying paper is accepted for MFCS 2016.

• Edon Kelmendi: Deciding Maxmin Reachability in Half-Blind Stochastic Games

  Authors: Edon Kelmendi and Hugo Gimbert

  Abstract:

  Two-player, turn-based, stochastic games with reachability conditions are considered, where the maximizer has no information (he is blind) and is restricted to deterministic strategies whereas the minimizer is perfectly informed. We ask the question of whether the game has maxmin , in other words we ask whether for all there exists a deterministic strategy for the (blind) maximizer such that against all the strategies of the minimizer, it is possible to reach the set of final states with probability larger than . This problem is undecidable in general, but we define a class of games, called leaktight half-blind games where the problem becomes decidable. We also show that mixed strategies in general are stronger for both players and that optimal strategies for the minimizer might require infinite-memory.

15:45–16:45 Session 8b – (Finite) Model Theory (chair: Luc Segoufin, room: Forum B)

• Jan Obdrzalek: A New Perspective on FO Model Checking of Dense Graph Classes

  Authors: Joint work with Jakub Gajarsky, Petr Hlineny, Daniel Lokshtanov and M. S. Ramanujan.

  Abstract:

  We study the FO model checking problem of dense graph classes, namely those which are FO-interpretable in some sparse graph class. Note that if an input dense graph is given together with the corresponding FO interpretation in a sparse graph, one can easily solve the model checking problem using the existing algorithms for sparse graph classes. However, if the assumed interpretation is not given, then the situation is markedly harder. In this talk I will give a structural characterization of graph classes which are FO interpretable in graph classes of bounded degree. This characterization allows us to efficiently compute such an interpretation for an input graph. As a consequence, we obtain an FPT algorithm for FO model checking of graph classes FO interpretable in graph classes of bounded degree. The approach used to obtain these results may also be of independent interest. Based on a paper accepted to LICS 2016.

• Paul Brunet: A Kleene Theorem for Petri automata

  Authors:

  Abstract:

  Petri Automata are automata based on Petri nets, whose operational semantics is designed to recognise sets of graphs. We introduced them in a recent paper [1] with Pous to study Kleene Allegory (KAl) expressions: terms built from a finite alphabet of variables, with the constants 0 and 1, the unary operators converse and Kleene star, and the binary operators union, composition and intersection. To any such expression, one can associate a set of graphs such that two expressions are universally equivalent when interpreted as binary relations if and only if their associated sets of graphs are equal. In [1] we gave a method to build from any Kleene Allegory expression a Petri automaton recognising the appropriate set of series parallel graphs. It is then natural to wonder what is the class of graph languages recognised by Petri automata. For the usual notion of finite state automata, the well known Kleene Theorem states that the languages recognisable by automata are exactly those specifiable by regular expressions. This year we provided a similar theorem for Petri automata and Kleene Allegory expressions [2]. Indeed the graph languages specified by Petri automata are precisely the languages denoted by KAl. Moreover, this entails that decidability of the equational theory of Kleene Allegories is equivalent to that of language equivalence for Petri automata. This decidability problem is still open. It is worth mentioning that the technical part of the proof in [2] actually uses a smaller syntax than Kleene Allegories, without converse nor identity. In this fragment the considered graphs are series-parallel, so that the key technical result is actually a Kleene theorem for series-parallel regular expressions and languages. References: [1] Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on, pages 68–79, July 2015. [2] Paul Brunet. A Kleene theorem for Petri automata. Submitted in Foundations of Software Technology and Theoretical Computer Science, 36th IARCS Annual Conference on, December 2016.

• Stefan Mengel: A Dual to a Classical Graph Homomorphism Theorem of Lovász

  Authors: Hubie Chen and Stefan Mengel

  Abstract:

  Homomorphism between finite structures are a classical object of study considered in many areas including structural graph theory, constraint satisfaction and database theory. A classical result by Lovász states that every structure B is uniquely characterized (up to isomorphism) by the number of homomorphisms from other structures to B. In this talk I will I will give a dual version of this result that roughly says that every structure is uniquely described by the number of homomorphisms it has to other graphs.

• Valentin Goranko: Game-Theoretic Semantics for Alternating-Time Temporal Logic

  Authors:

  Abstract:

  We introduce several versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level, in the standard semantics of the strategic operators, and on the meta-level, where game-theoretic logical semantics can be applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL, based on limiting the time resources available to the verifier and falsier in the semantic evaluation game. We introduce and analyse unbounded and bounded GTS and prove these to be equivalent to the standard (Tarski style) compositional semantics. We also introduce a non-equivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

16:45–17:00 Break

17:00–18:30 Invited Session 2 – Sets with Atoms (organizer: SŁAWOMIR LASOTA, room: Forum A)

• Szymon Toruńczyk: Towards complexity theory with atoms

  Authors:

  Abstract:

  I will discuss various classical computational problems, generalized to the setting where the instances are potentially infinite sets with atoms. In particular, we will focus on constraint satisfaction problems, such as 3-colorability, unreachability, Horn-SAT, solvability of systems of linear equations, where the instance is an infinite structure (graph, formula) built out of atoms, with a finite description. It turns out that tight classical complexity results lift to the infinite setting. Moreover, many classical algorithms can be lifted to this setting in a natural way.

• Eryk Kopczyński and Michał Szynwelski: Programming with atoms (tool demonstration)

  Authors:

  Abstract:

  A demo presentation of two simple programming languages designed to manipulate infinite, but first-order definable structures, such as the set of all intervals with rational endpoints. One of the languages is implemented as a C++ library, LOIS, by Eryk Kopczyński and Szymon Toruńczyk, while the other as a Haskell module, NLambda, by Bartek Klin and Michał Szynwelski. Internally, infinite sets are represented by logical formulas that define them, whereas an external SMT solver is invoked to check their basic properties.

• Murdoch James Gabbay: Consistency of Quine’s NF using nominal techniques

  Authors:

  Abstract:

  Naive set theory has one rule; naive sets comprehension: If φ is a predicate, then {a | φ(a)} is a set. This is inconsistent by Bertrand Russell’s famous observation of 1901 that {a | a ∉ a} ∈ {a | a ∉ a} if and only if {a | a ∉ a} ∉ {a | a ∉ a}. Solutions proposed included Zermelo-Fraenkel set theory, simple type theory, and Quine’s New Foundations (NF). NF works by restricting comprehension to stratifiable formulae; those in which variables can be assigned ‘levels’, which are natural numbers, such that if a ∈ b occurs and a has level n, then b must have level n+1. Russell’s example is ruled out because a ∉ a cannot be stratified. Consistency of NF has been an open problem since it was proposed by Quine in 1937. I will present a claimed proof of consistency for Quine’s NF (paper available on my webpage and on arXiv from www.gabbay.org.uk/papers.html#conqnf), exhibiting it as a corollary of a new view of the foundations of logic and computation based on nominal techniques which I have been developing now for several years.

20:00- Informal picnic (every participant brings smthg to eat or drink). Location: Park of "Abbaye de la Cambre" (see section "venue" for a map).

9:00–10:00 KEYNOTE 3 (chair: Mikołaj Bojańczyk, room: Forum A)

• Andreas Maletti (Universität Stuttgart): Tree Automata in Parsing and Machine Translation

  Authors:

  Abstract:

  We will discuss how tree automata were rediscovered in the area of statistical parsing of natural language sentences and demonstrate that some techniques developed in that area might also be beneficial in automata theory. On the example of syntax-based machine translation, we will demonstrate the other direction showing how automata theory can provide solutions to problems in natural language processing. With the identification of the exact expressive power in terms of standard models and known closure properties for them, we developed a syntax-based translation system that can translate not only a single parse, but rather the full parse forest delivered by the parser.

10:30–11:45 Sessions 10a – (Quantitative) Games (chair: Sven Schewe, room: Forum A)

• Mickael Randour: Average-energy games

  Authors: Joint work with Patricia Bouyer, Nicolas Markey, Kim G. Larsen and Simon Laursen

  Abstract:

  Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements. This talk is based on joint work with Patricia Bouyer, Nicolas Markey, Kim G. Larsen and Simon Laursen, published in GandALF 2015 [1]. An extended version can be found on arXiv [2]. [1] P. Bouyer, N. Markey, M. Randour, K.G. Larsen, and S. Laursen. Average-energy games. In Proc. of GandALF, EPTCS 193, pages 1–15, 2015. [2] P. Bouyer, N. Markey, M. Randour, K.G. Larsen, and S. Laursen. Average-energy games (full version). CoRR, abs/1512.08106, 2015.

• Gilles Geeraerts (2016): To Reach Or Not To Reach? Efficient Algorithms for Total-Payoff Games

  Authors:

  Abstract:

  Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games (that can be seen as a refinement of the well- studied mean-payoff games) are the variant where the payoff of a play is computed as the sum of the weights. We present the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. This work has been published in the Proceedings of FSTTCS 2015 and an extended journal version has been accepted for publication in the special issue of the conference.

• Alexander Weinert: Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs

  Authors:

  Abstract:

  The winning condition of a parity game with costs requires an arbitrary, but fixed bound on the distance between occurrences of odd colors and the next occurrence of a larger even one. Such games quantitatively extend parity games while retaining most of their attractive properties, i.e, determining the winner is in NP and co-NP and one player has positional winning strategies. We show that the characteristics of parity games with costs are vastly different when asking for strategies realizing the minimal such bound: the solution problem becomes PSPACE-complete and exponential memory is both necessary in general and always sufficient. Thus, playing parity games with costs optimally is harder than just winning them. Moreover, we show that the tradeoff between the memory size and the realized bound is continuous in general.

• Arno Pauly: Bounded versus unbounded energy parity games

  Authors: Joint work with Stephane Le Roux

  Abstract:

  We introduce bounded energy parity games, where the energy level is capped at some bound. We show that given a sufficiently large bound (2nW, n the number of vertices, W the largest weight), they are equivalent to the usual unbounded energy parity games. This enables a new proof of finite memory determinacy for the latter, yielding better (and optimal!) bounds on the memory required. Work based on http://arxiv.org/abs/1602.08912.

• Youssouf Oualhadj: Rational verification in Iterated Electric Boolean Games

  Authors: With Nicolas Troquard

  Abstract:

  Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational elimination and rational construction of Nash equilibria by a supervising authority are PSPACE-complete problems. The proposed talk is based on the paper “Rational verification in Iterated Electric Boolean Games” accepted at the 4th International Workshop on Strategic Reasoning (SR 2016).

10:30–11:45 Sessions 10b – Automata & Transducer (chair: Emmanuel Filiot, room: Forum B)

• Nathan Lhote: A logic for transductions and its decision through data words

  Authors: Joint with Luc Dartois and Emmanuel Filiot

  Abstract:

  *this talk does not correspond to an accepted or published paper* In the model of graph transductions from Courcelle, an output structure is obtained from several copies of the input structure and the predicates are defined by MSO formulas interpreted over the input structure. This formalism is asymmetric in the sense that one cannot speak of the output structure independently from the input one. In contrast we introduce a logical description of word to word transductions which allows one to both speak about the input and output structures independently, but also to express dependencies between the two structures through an origin predicate. Both the input and output words are seen as a single compound graph structure, with an origin predicate that relate output positions to input positions. When considering the full power of MSO over these compound structures, the satisfiability problem is, unsurprisingly, undecidable. To overcome this we consider the logical fragment of first-order logic with two variables, enriched with arbitrary binary MSO-definable predicates with quantification restricted to the input positions. We show that this logic is decidable yet expressive enough to encompass MSO transductions à la Courcelle. The decidability is obtained through a reduction to data word logic. Intuitively the datum of a position corresponds to its origin position in the input word. Following [Schwentick & Zeume 2012] we see a data word as a structure with one linear order and one total pre-order, and extending their result we show the decidability (over data words) of first-order logic with two variables enriched with arbitrary binary MSO-definable relations that use only the pre-order predicate (and unary predicates).

• Luc Dartois: Two-Way Visibly Pushdown Automata and Transducers

  Authors:

  Abstract:

• Didier Villevalois: A twinning property for minimisation of k-subsequentiality

  Authors: Joint work with Laure Daviaud, Ismaël Jecker and Pierre-Alain Reynier

  Abstract:

  Weighted automata (WA) extend finite-state automata by associating with transitions weights from a semiring S, defining functions from words to S. An important subclass is that of multi-subsequential functions, that can be realized as a finite union of subsequential transducers. For this class, a natural open problem consists in minimizing the size of this union. In the present work, our objective is to adapt a recent work of Daviaud, Reynier and Talbot in order to solve this problem. We exhibit an original branching twinning property parameterized by k in order to characterize the definability of an unambiguous weighted automaton as a union of k sub-sequential weighted automata. Alongside, comes a Lipshitz property also parametrized by k, which at order 1 corresponds to the characterization of sequential finite state transducers. Given an unambiguous weighted automaton W over an infinitary group (G,⊗) realizing some function f, we conjecture that the following three properties are equivalent: (i) W satisfies the branching twinning property of order k, (ii) f satisfies the Lipshitz property of order k, (iii) f can be described as a union of k sub-sequential weighted automata. We can show that one can decide whether a weighted automaton satisfies the branching twinning property. As a corollary, this allows to decide the minimisation problem defined above for multi-sequential functions. Last, this result can be lifted to finite-valued finite-state transducers. This is a joint work with Laure Daviaud, Ismaël Jecker and Pierre-Alain Reynier, that is still in progress.

• Godin Thibault: Connected reversible Mealy automata of prime size cannot generate infinite Burnside groups

  Authors:

  Abstract:

  The simplest example of an infinite Burnside group arises in the class of automaton groups. However there is no known example of such a group generated by a reversible Mealy automaton. It has been proved that, for a connected automaton of size at most~3, or when the automaton is not bireversible, the generated group cannot be Burnside infinite. In this paper, we extend these results to automata with bigger stateset, proving that, if a connected reversible automaton has a prime number of states, it cannot generate an infinite Burnside group. This talk is based on a paper accepted for MFCS 2016.

• Dietrich Kuske and Olena Prianychnykova: The trace monoids in the queue monoid and in the direct product of two free monoids

  Authors:

  Abstract:

  We prove that a trace monoid embeds into the queue monoid if and only if it embeds into the direct product of two free monoids. We also give a decidable characterization of these trace monoids. The results to be reported in this talk are accepted for DLT 2016.

• Tony Tan: Reasoning with difference on roles in description logic ALC

  Authors: Tony Tan, Jan Van den Bussche, Xiaowang Zhang

  Abstract:

  We present an algebra

11:45–12:00 Break

12:00–13:15 Session 11 – Formal Languages & Databases (chair: Claire David, room: Forum A)

• Jef Wijsen: Certain Query Answering for Primary Keys in First-Order Logic

  Authors: Paraschos Koutris and Jef Wijsen

  Abstract:

  This talk presents work that was first published in ACM PODS 2015, and that was recently awarded the “ACM SIGMOD Research Highlight Award 2015”. To capture uncertainty in the relational data model, we allow relations to violate their primary key. A block is defined as a maximal set of tuples from the same relation with the same primary key value, and a repair (or possible world) of a database instance is obtained by selecting exactly one tuple from each block. For a fixed Boolean first-order query q, the problem CERTAINTY(q) takes a database instance I as input and asks whether q evaluates to true on every repair of I. It has been known for several years that there exist Boolean conjunctive queries q1, q2, and q3 such that CERTAINTY(q1) is coNP-complete, CERTAINTY(q2) is in FO, and CERTAINTY(q3) is in PTIME but not in FO. This raises the question whether we can determine the complexity of CERTAINTY(q) for every Boolean conjunctive query q. In our work, we solved this question for Boolean conjunctive queries that are self-join-free (i.e., in which no relation name occurs more than once). In a talk of ten minutes, we will give the intuition of an algorithm that takes a self-join-free Boolean conjunctive query as input, and decides whether CERTAINTY(q) is in FO. Moreover, we will show that if CERTAINTY(q) is in FO, there is an elegant construction that builds a first-order formula for solving CERTAINTY(q).

• Gaetano Geck: Containment for Conjunctive Queries with Negation

  Authors: With Bas Ketsman, Frank Neven and Thomas Schwentick

  Abstract:

  A query Q is contained in a query Q’ if, for every database D, the result Q(D) is contained in Q'(D). Deciding containment is an interesting and often used sub-problem for minimisation of queries, verification of dependencies and other tasks. It was shown that the containment of conjunctive queries is intimately related to the existence of a homomorphism between the queries and that deciding containment in this case is NP-complete [1]. We have shown that deciding containment for conjunctive queries _with negation_ is coNEXPTIME-complete in general [2]. Previously the problem seems only to have been studied for queries over schemas of bounded arity, where it was known to be Pi^p_2-complete [3]. PUBLICATION: This result has been published in [2] for the 19th International Conference on Database Theory, ICDT 2016, Bordeaux, France, March 15-18, 2016. REFERENCES [1] Ashok K. Chandra, Philip M. Merlin: Optimal Implementation of Conjunctive Queries in Relational Data Bases. STOC 1977: 77-90 [2] Gaetano Geck, Bas Ketsman, Frank Neven, Thomas Schwentick: Parallel-Correctness and Containment for Conjunctive Queries with Union and Negation. ICDT 2016: 9:1-9:17 [3] Marie-Laure Mugnier, Geneviève Simonet, Michaël Thomazo: On the complexity of entailment in existential conjunctive first-order logic with atomic negation. Inf. Comput. 215: 8-31 (2012)

• Charles Paperman: Schema validation via streaming circuits

  Authors:

  Abstract:

  XML schema validation can be performed in constant memory in the streaming model if and only if the schema admits only trees of bounded depth—an acceptable assumption from the practical view-point. In this talk I will present a refinement of the streaming model that take into account that data can be streamed block-by-block, rather then letter-by-letter. Therefore, it provides opportunities to speed up the computation by parallelizing the processing of each block. For this purpose I will introduce a new fine-grained parallel model of computation: the *streaming circuits*. This model process words of arbitrary length in blocks of fixed size, passing constant amount of information between blocks. It allows us to transfer fundamental results about the circuit complexity of regular languages to the setting of streaming schema validation, which leads to effective constructions of streaming circuits of depth logarithmic in the block size, or even constant under certain assumptions on the input schema.

• Eryk Kopczynski: Invisible Pushdown Languages

  Authors:

  Abstract:

  Context-free languages allow one to express data with hierarchical structure, at the cost of losing some of the useful properties of languages recognized by finite automata on words. However, it is possible to restore some of these properties by making the structure of the tree visible, such as is done by visibly pushdown languages, or finite automata on trees. In this paper, we show that the structure given by such approaches remains invisible when it is read by a finite automaton (on word). In particular, we show that separability with a regular language is undecidable for visibly pushdown languages, just as it is undecidable for general context-free languages.

• Ismaël Jecker: On Equivalence and Uniformisation Problems for Finite Transducers

  Authors: With Emmanuel Filiot, Christof Löding and Sarah Winter

  Abstract:

  Transductions are binary relations of finite words. For rational transductions, i.e., transductions defined by finite transducers, the inclusion, equivalence and sequential uniformisation problems are known to be undecidable. In this talk, I investigate stronger variants of inclusion, equivalence and sequential uniformisation, based on a general notion of transducer resynchronisation, and show their decidability. I also investigate the classes of finite-valued rational transductions and deterministic rational transductions, which are known to have a decidable equivalence problem, and show that sequential uniformisation is also decidable for them.

• František Blahoudek: Complementing Semi-Deterministic Büchi Automata

  Authors: Joint with Matthias Heizmann, Sven Schewe, Jan Strejček, and Ming-Hsien Tsai.

  Abstract:

  We introduce an efficient complementation technique for semi-deterministic Büchi automata, which are Büchi automata that are deterministic in the limit: from every accepting state onward, their behaviour is deterministic. It is interesting to study semi-deterministic automata, because they play a role in practical applications of automata theory, such as the analysis of Markov decision processes. Our motivation to study their complementation comes from the termination analysis implemented in Ultimate Büchi Automizer, where these automata represent checked runs and have to be complemented to identify runs to be checked. We show that semi-determinism leads to a simpler complementation procedure. Our complementation is based on an extended breakpoint construction that allows for symbolic implementation. It also leads to significantly improved bounds as the complement of a semi-deterministic automaton with states has less than states. Moreover, the resulting automaton is unambiguous, which again offers new applications, like the analysis of Markov chains. We also motivate and present an on-the-fly modification of our complementation, which does not need to know the whole automaton before the complementation starts, which is a crucial property for Ultimate Büchi Automizer that uses implicitly encoded automata. The price for the on-the-fly approach is a slightly worse upper bound on the size of the produced automaton for the complement: it has less than 5^n states. We have evaluated our construction against the semi-deterministic automata produced by Ultimate Büchi Automizer applied to programs of the Termination category of the software verification competition SV-COMP 2015. We complemented these automata by our algorithm and by four standard complementation constructions and compare the resulting automata. The evaluation confirms that our algorithm outperforms the known complementation techniques that work for general nondeterministic Büchi automata. The presentation is based on the identically titled paper published at TACAS 2016.