9:00 — 10:30 Session T1: TUTORIAL 1
chair: Ranko Lazic

• 9:00 – 10:30 Uri Zwick: Randomized and deterministic algorithms for 2-player turn-based stochastic and non-stochastic games, part I

  Abstract:

  We describe the fastest known randomized algorithm for solving 2-player 0-sum turn-based stochastic games. The running time of the algorithm is sub-exponential, i.e., roughly of the form 2^{O(n^{1/2})}, where n is the number of states of the games. The algorithm is based on randomized pivoting rules for the simplex algorithm developed by Kalai (1992) and Matousek, Sharir and Welzl (1992). Various versions of such algorithms were developed by Ludwig (1995), Bj\”{o}rklund and Vorobyov (2005), Halman (2007), with slight improvements by Hansen and Zwick (2015).

11:00 — 12:30 Session T2: TUTORIAL 2
chair: Ranko Lazic

• 11:00 – 12:30 Uri Zwick: Randomized and deterministic algorithms for 2-player turn-based stochastic and non-stochastic games, part II

  Abstract:

  We describe the fastest known deterministic algorithms for solving Energy Games (EGs) and Mean Payoff Games (MPGs). For general edge costs the running time is about 2^{n/2}, where n is the number of vertices (states) of the game. When edge costs are integers of absolute value at most M, the running time becomes O(mnM). The algorithms described are based on a paper of Brim et al. (2011), and extensions of results that appeared in a recent paper of Dorfman, Kaplan and Zwick (2019).

14:00 — 15:30 Session T3: TUTORIAL 3
chair: Barbara König

• 14:00 – 15:30 Laure Daviaud: Probabilistic Automata

  Abstract:

  Probabilistic automata were introduced by Rabin in 1963 as an automatic way to map input words with probabilities. They can be viewed as classic non deterministic finite automata, where transitions are labelled with a probability to be taken, given a state and a letter, and words have then a certain probability to be accepted. Probabilistic automata can be seen as a particular case of partially observable Markov decision processes and the natural problems that arise ask whether one can find input words with high probability to be accepted. This tutorial will introduce this model and we will discuss in particular some famous problems related to it, such as emptiness, value 1, approximation, equivalence and containment.

16:00 — 17:30 Session T4: TUTORIAL 4
chair: Barbara König

• 16:00 – 17:30 Laure Daviaud: Probabilistic Automata

  Abstract:

  Probabilistic automata were introduced by Rabin in 1963 as an automatic way to map input words with probabilities. They can be viewed as classic non deterministic finite automata, where transitions are labelled with a probability to be taken, given a state and a letter, and words have then a certain probability to be accepted. Probabilistic automata can be seen as a particular case of partially observable Markov decision processes and the natural problems that arise ask whether one can find input words with high probability to be accepted. This tutorial will introduce this model and we will discuss in particular some famous problems related to it, such as emptiness, value 1, approximation, equivalence and containment.

9:00 — 9:30 Session 0: WELCOME

• 9:00 – 9:30 Welcome

  Abstract:

9:30 — 10:00 Session 1: WELCOME
chair: Nathalie Bertrand

• 9:30 – 10:00 Thomas Schwentick: Climate, Traveling, and (Highlights-) Conferences

  Abstract:

10:15 — 11:11 Session 2A: GAMES I
chair: Christof Löding

• 10:15 – 10:22 Ashwani Anand: Complexity of games with combination of objectives using separating automata

  Poster:

  

  Slides:

  open
  

  Abstract:

  Games on graphs is a crucial theoretical concept in Logic and Automata Theory, and has found many applications in verification and synthesis. Parity games and Mean payoff games have been in the center of this concept. However, for synthesis of reactive systems with multiple resource constraints and functional requirements, these games individually are not sufficient, and we need to consider combination of these objectives. In 2005, Chatterjee et al. introduced the notion of parity mean payoff games to solve synthesis problems with qualitative (Parity) and quantitative (Mean Payoff) objectives. Games with combination of multiple Mean Payoff objectives have also been studied. We provide a different approach to solve such games. We use the concept of separating automata, introduced by Bojańczyk and Czerwiński. The idea of using the separating automata to solve games is not new and have been used in past to solve Parity games. In fact, all the known quasi-polynomial time algorithms solving Parity games come under this umbrella approach. We consider the games with disjunctive combination of Parity (P), Mean payoff with limsup (supMP) and Mean payoff with liminf (infMP) objectives. Using the separating automata for the individual objectives as black boxes, we give two constructions of separating automata; one for PvP, and another for infMP∨infMP, P∨infMP and P∨supMP. We match the complexity of best known algorithms for the respective games with this approach. This is a joint work with Nathanaël Fijalkow and Jérôme Leroux.

• 10:22 – 10:29 Rémi Morvan: A Universal Attractor Decomposition Algorithm for Parity Games

  Poster:

  

  Abstract:

  An attractor decomposition meta-algorithm for solving parity games is given that generalizes the classic McNaughton-Zielonka algorithm and its recent quasi-polynomial variants due to Parys (2019), and to Lehtinen, Schewe, and Wojtczak (2019). The central concepts studied and exploited are attractor decompositions of dominia in parity games and the ordered trees that describe the inductive structure of attractor decompositions. The main technical results include the embeddable decomposition theorem and the dominion separation theorem that together help establish a precise structural condition for the correctness of the universal algorithm: it suffices that the two ordered trees given to the algorithm as inputs embed the trees of some attractor decompositions of the largest dominia for each of the two players, respectively. The universal algorithm yields McNaughton-Zielonka, Parys’s, and Lehtinen-Schewe-Wojtczak algorithms as special cases when suitable universal trees are given to it as inputs. The main technical results provide a unified proof of correctness and deep structural insights into those algorithms. This paper motivates a research program of developing new efficient algorithms for solving parity games by designing new classes of small trees that embed the largest dominia in relevant classes of parity games. An early success story in this research program is the recent development, by Daviaud, Jurdziński, and Thejaswini (2019), of Strahler-universal trees, which embed dominia in games of bounded register number, introduced by Lehtinen (2018). When run on these trees, the universal algorithm can solve games with bounded register number in polynomial time and in quasi-linear space. A symbolic implementation of the universal algorithm is also given that improves the symbolic space complexity of solving parity games in quasi-polynomial time from — achieved by Chatterjee, Dvořák, Henzinger, and Svozil (2018) — down to , where is the number of vertices and is the number of distinct priorities in a parity game. This not only exponentially improves the dependence on , but it also entirely removes the dependence on . Joint work with Marcin Jurdziński.

• 10:29 – 10:36 K. S. Thejaswini: The Strahler Number of a Parity Game

  Poster:

  

  Slides:

  open
  

  Abstract:

  The Strahler number of a rooted tree is the largest height of a perfect binary tree that is its minor. The Strahler number of a parity game is proposed to be defined as the smallest Strahler number of the tree of any of its attractor decompositions. It is proved that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices n and linear in (d/2k)^k, where d is the number of priorities and k is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. The proof is based on a new construction of small Strahler-universal trees. It is shown that the Strahler number of a parity game is a robust, and hence arguably natural, parameter: it coincides with its alternative version based on trees of progress measures and—remarkably—with the register number defined by Lehtinen (2018). It follows that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices and linear in (d/2k)^k, where k is the register number. This significantly improves the running times and space achieved for parity games of bounded register number by Lehtinen (2018) and by Parys(2020). The running time of the algorithm based on small Strahler-universal trees yields a novel trade-off k.log(d/k) = O(log n) between the two natural parameters that measure the structural complexity of a parity game, which allows solving parity games in polynomial time. This includes as special cases the asymptotic settings of those parameters covered by the results of Calude, Jain, Khoussainov, Li, and Stephan (2017), of Jurdzinski and Lazic (2017), and of Lehtinen (2018), and it significantly extends the range of such settings, for example to d = 2^{O(\sqrt{\lg n})} and k = O(\sqrt{\lg n}).

• 10:36 – 10:43 Pranav Ashok: Compact and explainable strategy representations using dtControl

  Poster:

  

  Abstract:

  Strategies or controllers are entities arising out of controller synthesis of cyber-physical systems or model checking of non-deterministic systems. A strategy specifies for every state an action that may be taken to satisfy some specification (e.g., safety). For implementation and debugging purposes, it is beneficial to have concise and human-interpretable representations of strategies. Recent work has shown that decision trees can be used to represent provably-correct strategies concisely. Moreover, they make the strategy explainable and help boost understanding and trust. Compared to representations using lookup tables or binary decision diagrams, decision tree representations are smaller and more explainable. In this talk, I will present the recent advances we have made in decision tree representations of memoryless strategies produced by model checking tools such as PRISM and Storm, as well as controller synthesis tools such as SCOTS and Uppaal Stratego. I will also present a comprehensive evaluation of various decision tree learning algorithms applied to multiple case studies, obtained using our new tool dtControl. The talk is based on our paper published at HSCC 2020, co-authored with Mathias Jackermeier, Pushpak Jagtap, Jan Křetínský, Maximilian Weininger and Majid Zamani.

• 10:43 – 10:50 Maximilian Weininger: Approximating Values of Generalized-Reachability Stochastic Games

  Poster:

  

  Slides:

  open
  

  Abstract:

  Simple stochastic games are turn-based 2.5-player games with a reachability objective. The basic question asks whether one player can ensure reaching a given target with at least a given probability. A natural extension is games with a conjunction of such conditions as objective. Despite a plethora of recent results on the analysis of systems with multiple objectives, the decidability of this basic problem remains open. In the presentation, we present an algorithm approximating the Pareto frontier of the achievable values to a given precision. Moreover, it is an anytime algorithm, meaning it can be stopped at any time returning the current approximation and its error bound.

• 10:50 – 10:57 Tobias Winkler: Stochastic Games with Lexicographic Reachability-Safety Objectives

  Poster:

  

  Slides:

  open
  

  Abstract:

  Simple stochastic games (SGs) are zero-sum turn-based stochastic games played over a finite state space by two adversarial players, Maximizer and Minimizer, along with randomness in the transition function. These games allow to model the interaction of angelic and demonic non-determinism as well as stochastic uncertainty. An objective specifies a desired set of trajectories of the game, and the goal of the Maximizer is to maximize the probability of satisfying the objective against all choices of the Minimizer. The basic decision problem is to determine whether the Maximizer can ensure satisfaction of the objective with a given probability threshold. This problem is among the rare and intriguing combinatorial problems that are in NP ∩ coNP, but are not known to belong to P. SGs are a standard model in control and verification of stochastic reactive systems. In this talk, I consider SGs with multiple reachability and safety objectives with a lexicographic preference order on top. That is, Maximizer must optimize the most important objective and furthermore, among all possible strategies to do so, she must optimize the second most important objective and so on; and each objective can be either reachability or safety. The presentation is based on a joint paper with Krishnendu Chatterjee, Joost-Pieter Katoen and Maximilian Weininger.

• 10:57 – 11:04 Ayrat Khalimov: Register Games on Infinite Ordered Data Domains

  Poster:

  

  Slides:

  open
  

  Abstract:

  We introduce two-player turn-based zero-sum register games on an infinite linearly ordered data domain. Register games have a finite set of registers intended to store data values. At each round, Adam picks some data in the domain, which is tested against the data contained in the registers, using the linear order. Depending on which test holds (exactly one is required), Eve decides to assign the data to some of her registers, and the game deterministically evolves to a successor vertex depending on her assignment choice. Eve wins the game if she has a strategy, which depends only on the tests and not on the concrete data values, such that whichever values Adam provides, the sequence of visited game vertices satisfies a given parity condition. We show the decidability of register games over data domains N and Q. In both data domains, they can be solved in ExpTime and finite-memory strategies suffice to win. We apply these results to solve the synthesis problem of strategies resolving non-determinism in (non-deterministic) register transducers on data words.

• 11:04 – 11:11 Karoliina Lehtinen: Good-for-games omega-pushdown automata

  Abstract:

  We introduce good-for-games ω-pushdown automata (ω-GFG-PDA). These are automata whose nondeterminism can be resolved based on the run constructed thus far. Good-for-gameness enables automata to be composed with games, trees, and other automata, applications which otherwise require deterministic automata. In the setting of regular automata, determinisation is expensive, but always possible. Good-for-gameness is a way of avoiding determinisation, and good-for-games automata can sometimes be exponentially more succinct than any equivalent deterministic automata. In the context-free setting, the gap between nondeterminism and determinism is wider: nondeterministic PDA are more expressive, but deterministic ones have better decidability properties. Our main results show that ω-GFG-PDA are more expressive than deterministic ω-pushdown automata and that solving infinite games with winning conditions specified by ω-GFG-PDA is EXPTIME-complete, i.e., we have identified a new class of ω-contextfree winning conditions for which solving games is decidable. This means in particular that the universality problem is in EXPTIME as well. Moreover, we study closure properties (or lack thereof) of the class of languages recognized by ω-GFG-PDA and undecidability of good-for-gameness of ω-pushdown automata and languages. This talk will present joint work with Martin Zimmermann, published at LICS 2020.

10:15 — 11:11 Session 2B: SEMANTIC & SYNTHESIS
chair: Achim Blumensath

• 10:15 – 10:22 Davide Catta: Towards a Modal Game Semantics

  Abstract:

  We investigate adversarial patrolling where the Defender is an autonomous device with a limited energy resource (e.g., a drone). Every eligible Defender’s policy must prevent draining the energy resource before arriving to a refill station, and this constraint substantially complicates the problem of computing an efficient Defender’s policy. Furthermore, the existing infinite-horizon models assume Attackers with unbounded patience willing to wait arbitrarily long for a good attack opportunity. We show this assumption is inappropriate in the setting with drones because here the expected waiting time for an optimal attack opportunity can be extremely large. To overcome this problem, we introduce and justify a new concept of impatient Attacker, and design a polynomial time algorithm for computing a Defender’s policy achieving protection close to the optimal value against an impatient Attacker. Since our algorithm can quickly evaluate the protection achievable for various topologies of refill stations, we can also optimize their displacement. We implement the algorithm and demonstrate its functionality on instances of realistic size.

• 10:22 – 10:29 Daniela Petrisan: Determinizing Probabilistic Automata via Weak Distributive Laws

  Poster:

  

  Abstract:

  In this talk we present a category-theoretic approach to obtaining a belief-state transformer, that is, a transition system where the state space carries a convex algebra structure, from a probabilistic automaton. We do so by proving the existence of a weak distributive law of the powerset monad over the distribution monad. This is joint work with Alexandre Goy.

• 10:29 – 10:36 Alexandre Goy: Alternating Automata and Up-To Techniques via Weak Distributive Laws

  Poster:

  

  Abstract:

  The coalgebraic determinization of alternating automata has long been obstructed by the absence of distributive law of the powerset monad over it- self [5, 6]. This can be fixed using the framework of weak distributive laws [3], as there is a unique well-behaved weak distributive law of the requested type. In our recent paper [4], we applied a similar strategy to cope with the absence of distributive law between the powerset monad and the distribu- tion monad. Here, we extend the framework of weak distributive laws to the case when one of the monads is only a functor, provide an abstract compo- sitionality result in the style of Cheng [2] and systematic soundness of up-to techniques. Along the way, we apply these results to alternating automata as a mo- tivating example. Another example is given by probabilistic automata, for which our results yield soundness of bisimulation up-to convex hull [1]. This talk is based on a submitted paper jointly written with Daniela Petrisan.

• 10:36 – 10:43 Andrzej Murawski: Leafy automata for higher-order concurrency

  Poster:

  

  Slides:

  open
  

  Abstract:

  Finitary Idealized Concurrent Algol (FICA) is a prototypical programming language combining functional, imperative, and concurrent computation. There exists a fully abstract game model of FICA, which in principle can be used to prove equivalence and safety of FICA programs. Unfortunately, the problems are undecidable for the whole language, and only very rudimentary decidable sub-languages are known. We propose leafy automata as a dedicated automata-theoretic formalism for representing the game semantics of FICA. The automata use an infinite alphabet with a tree structure. To demonstrate suitability of this automata model, we show that: – the game semantics of any FICA term can be represented by traces of a leafy automaton, and – the traces of any leafy automaton can be represented by a FICA term. Because of the close match with FICA, we view leafy automata as a promising starting point for finding decidable subclasses of the language and, more generally, to provide a new perspective on models of higher-order concurrent computation.

• 10:43 – 10:50 Ritam Raha: Revisiting Synthesis for One-Counter Automata

  Poster:

  

  Slides:

  open
  

  Abstract:

  One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables. We revisit the parameter synthesis problem for such automata. That is, we ask whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-regular property. The problem has been shown to be encodable in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment of the logic is unfortunately undecidable. Nevertheless, by reduction to a class of partial observation games, (ii) we prove the synthesis problem is decidable. Finally, (iii) we give a polynomial-space algorithm for the problem if parameters can only be used in tests, and not updates, of the counter.

• 10:50 – 10:57 Catalin Dima: A Hennessy-Milner Theorem for ATL with Imperfect Information

  Slides:

  open
  

  Abstract:

  We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a {\em common knowledge} semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accomodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.

• 10:57 – 11:04 Bastien Maubert: Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

  Poster:

  

  Slides:

  open
  

  Abstract:

  Prompt-LTL extends Linear Temporal Logic with a bounded version of the “eventually” operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete.

• 11:04 – 11:11 Radosław Piórkowski: Timed synthesis games

  Poster:

  

  Abstract:

  We study a generalisation of Büchi-Landweber games to the timed setting with an aim of solving the strategy synthesis problem for Player II. In our setting, that equals to constructing a timed automaton with an output – a timed controller. We show that for fixed number of clocks but *without* specifying the maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. This is an important technical novelty, since the related decidability results found in previous literature required both constants to be fixed. As an application of timed games, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata. This is a novel decision problem about timed automata which has not been studied before. During the presentation, I will briefly introduce our games and show, how our results can be used to solve the separability problem. This presentation is based on a paper by Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski.

11:11 — 12:00 Session 3: POSTER SESSION

14:00 — 15:00 Session 4: INVITED TALK 1
chair: Johanna Bjorklund

• 14:00-15:00 Mehryar Mohri: Playing against Weighed Automata

  Abstract:

15:15 — 16:18 Session 5A: LOGIC
chair: Michal Pilipczuk

• 15:15 – 15:22 Daniel Hausmann: NP Reasoning in the Monotone mu-Calculus

  Poster:

  

  Slides:

  open
  

  Abstract:

  Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone mu-calculus with the universal modality – contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes. This work has been published as joint work with Lutz Schröder at IJCAR 2020 under the title “NP Reasoning in the Monotone mu-Calculus”; an extended preprint of the conference paper can be found at https://arxiv.org/abs/2002.05075.

• 15:22 – 15:29 Jonas Schmidt: Work-sensitive Dynamic Complexity of Formal Languages

  Poster:

  

  Abstract:

  DynFO is the dynamic complexity class of all queries that can be main- tained by first-order dynamic programs with the help of auxiliary relations under insertions and deletions of tuples. If one tries to make the “DynFO approach” to maintaining queries relevant for practical considerations, the work that is needed to carry out the specified updates, hence the work of an algorithm (i.e. the sum of the number of operations of all processors) implementing them, is a crucial factor. In this talk, I will introduce a work-aware version of DynFO and present first results for the question which queries can be maintained in DynFO with little work – in this first investigation restricted to dynamic language membership queries.

• 15:29 – 15:36 Thomas Zeume: Teaching Logic with Iltis: an Interactive, Web-Based System

  Poster:

  

  Abstract:

  The Iltis project provides an interactive, web-based system for teaching logic, which is designed to provide immediate and comprehensive feedback for exercises covering various aspects of the reasoning workflow of propositional logic, modal logic, and first-order logic. In this talk I will provide an update on the status of the project.

• 15:36 – 15:43 Antoine Amarilli: A Dichotomy for Homomorphism-Closed Queries on Probabilistic Graphs

  Poster:

  

  Slides:

  open
  

  Abstract:

  We study the evaluation of queries over relational databases containing uncertain information. We represent these as tuple-independent probabilistic databases (TIDs): this is a model where the data consists of a relational database where each tuple is annotated with a probability of existence, and the semantics is that each tuple is present with the indicated probability, assuming independent across all tuples. In this context, the probabilistic query evaluation (PQE) problem for a Boolean query Q is to compute, given such a TID instance, the total probability of its possible worlds that satisfy Q. We study this task in data complexity, i.e., the query is fixed and the input is the probabilistic database. A foundational result in this context is the dichotomy of Dalvi and Suciu [2] on unions of conjunctive queries (UCQs). A UCQ is a finite disjunction of conjunctive queries, which are existentially quantified conjunctions of atoms. Dalvi and Suciu show that the UCQs can be partitioned between the safe UCQs, for which the PQE problem can be solved in polynomial time; and the unsafe UCQs, for which it is #P-hard. In this work, we extend this dichotomy to the more general class UCQ ∞ of queries that are closed under homomorphisms: a query Q is in UCQ ∞ iff, for any databases I and I 0 , if I satisfies Q and I has a homomorphism to I 0 , then I 0 also satisfies Q. This natural class contains all UCQs, and also includes recursive query languages studied in database theory, e.g., Regular Path Queries (RPQs), Datalog queries (without negation or inequalities), and a large class of ontology-mediated queries. Equivalently, the queries in UCQ ∞ can be characterized as possibly infinite disjunctions of conjunctive queries, hence the notation. For technical reasons, we restrict our study to arity-two signatures, i.e., probabilistic graphs. Our contribution is to show that, in this context, for any UCQ ∞ query Q which is unbounded, i.e., not equivalent to a UCQ, then the PQE problem is #P-hard. This implies an extension of the dichotomy of Dalvi and Suciu to all UCQ ∞ queries in the arity-two case: the queries that are equivalent to a safe UCQ enjoy tractable PQE, and the task is #P-hard for all other queries. Our result is shown by reducing from counting the valuations of positive partitioned 2-DNF formulae (#PP2DNF) for some queries, or from the source-to-target reliability problem in an undirected graph (#U-ST-CON) for other queries, depending on properties of minimal models. Talk. The talk will briefly present the context of the work as above, state the result, and say a few words about the proof. Joint wor with İsmail İlkan Ceylan that will be presented at ICDT’2020. See https://av.tib.eu/media/46843.

• 15:43 – 15:50 Andreas Pieris: The Limits of Efficiency for Open- and Closed-World Query Evaluation Under Guarded TGDs

  Poster:

  

  Abstract:

  Ontology-mediated querying and querying in the presence of constraints are two key database problems where tuple-generating dependencies (TGDs) play a central role. In ontology-mediated querying, TGDs can formalize the ontology and thus derive additional facts from the given data, while in querying in the presence of constraints, they restrict the set of admissible databases. In this work, we study the limits of efficient query evaluation in the context of the above two problems, focusing on guarded and frontier-guarded TGDs and on UCQs as the actual queries.

• 15:50 – 15:57 Sam M. Thompson: Dynamic Complexity of Document Spanners

  Poster:

  

  Abstract:

  This talk is on the dynamic complexity of document spanners. Document spanners are a formal framework for information extraction which allows us to query text like we would a relational database. The question we investigate is, what is the complexity of computing the results of these queries if the text is subject to updates? To investigate this question, we use the dynamic complexity framework, which defines complexity classes based on the logic needed to write update formulas for a given query. Update formulas are used to keep the result of a query correct when updates to a database occur. If we can write such update formulas, then we can “maintain” that query. In our work, we show that the class of regular spanners can be maintained by the dynamic complexity class DynPROP (update formulas are in quantifier-free first-order logic), that the class DynCQ (update formulas are conjunctive queries) is more expressive than the class of core spanners, and that the class DynFO (update formulas are in first-order logic) is more expressive than generalized core spanners. This talk is based on a paper presented in ICDT 2020 and is joint work with Dominik Freydenberger.

• 15:57 – 16:04 Denis Kuperberg: Positive first-order logic on words

  Poster:

  

  Abstract:

  In this ongoing work, we investigate a fragment of first-order logic (FO) on words, called positive first-order logic (FO+). This fragment is designed to define only upwards-closed languages with respect to a given partial order on letters, by restricting the letter symbols to appear positively in the formula. It is not clear whether the converse holds: can any FO-definable upwards-closed language be defined in FO+ ? We show that this is not the case, by giving a counter-example. This example can be used to show that Lyndon’s theorem fails on finite words. Lyndon’s theorem states that on general structures, any FO formula defining a class of structures closed under surjective morphisms is equivalent to a FO+ formula. This theorem was known to fail on finite structures, but our proof strenghtens this result and simplifies its proof, using only finite words instead of a more complex signature. This is joint work with Thomas Colcombet, Amina Doumane, and Sam Van Gool.

• 16:04 – 16:11 Gregory Wilsenach: Symmetric Arithmetic Circuits

  Poster:

  

  Abstract:

  We introduce symmetric arithmetic circuits, i.e. arithmetic circuits with a natural symmetry restriction. In the context of circuits computing polynomials defined on a matrix of variables, such as the determinant or the permanent, the restriction amounts to requiring that the shape of the circuit is invariant under row and column permutations of the matrix. We establish unconditional, nearly exponential, lower bounds on the size of any symmetric circuit for computing the permanent over any field of characteristic other than 2. In contrast, we show that there are polynomial-size symmetric circuits for computing the determinant over fields of characterisitic zero.

• 16:11 – 16:18 Eugenia Ternovska: Hilbert’s Choice Operator and a Linear Dynamic Logic

  Abstract:

  We connect a version of Hilbert’s Epsilon (Choice) operator to a path semantics of a linear dynamic logic. The logic is a part of a family of logics that allow fine control of the complexity of order-independent computations. The approach is based on adding the ability to reason about information propagations in first-order logic with fixed points, FO(FP). Two parameters are used to control expressiveness and complexity: the set of logical connectives and the expressiveness of atomic units. We restrict the connectives to their deterministic counterparts, and we use output-monadic unions of conjunctive queries to represent the atomic units. We show that choice among query outcomes can be modelled dynamically by considering paths as sequences of choices. We demonstrate the equivalence of a semantics defined via binary relations and the path semantics. We show that data complexity for this logic is polynomial for a fixed path and give examples of counting and reachability properties expressible in this logic.

15:15 — 16:18 Session 5B: ARITHMETIC & PROBABILITIES
chair: Dmitry Chistikov

• 15:15 – 15:22 Matthew Hague: Monadic Decomposition in Integer Linear Arithmetic

  Poster:

  

  Abstract:

  Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a Boolean combination of monadic predicates in the theory. Recently, Veanes et al. showed the usefulness of monadic decomposability in the context of SMT (i.e. the input formula is quantifier-free), and found various interesting applications including string analysis. However, checking monadic decomposability is undecidable in general. Decidablity for certain theories is known (e.g. Presburger Arithmetic, Tarski’s Real-Closed Field), but there are very few results regarding their computational complexity. In this paper, we study monadic decomposability of integer linear arithmetic in the setting of SMT. We show that this decision problem is coNP-complete and, when monadically decomposable, a formula admits a decomposition of exponential size in the worst case. We provide a new application of our results to string constraint solving with length constraints. We then extend our results to variadic decomposability, where predicates could admit multiple free variables (in contrast to monadic decomposability). Finally, we give an application to quantifier elimination in integer linear arithmetic where the variables in a block of quantifiers, if independent, could be eliminated with an exponential (instead of the standard doubly exponential) blow-up.

• 15:22 – 15:29 Jonathan Tanner: On the Size of Finite Rational Matrix Semigroups

  Poster:

  

  Abstract:

  Let n be a positive integer and M a set of rational -matrices such that M generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in M whose length is at most , where is the maximum order of finite groups over rational -matrices. This result implies algorithms with an elementary running time for deciding finiteness of weighted automata over the rationals and for deciding reachability in affine integer vector addition systems with states with the finite monoid property.

• 15:29 – 15:36 Edon Kelmendi: Asymptotic omega-Regular Properties of Linear Recurrence Sequences

  Poster:

  

  Abstract:

  We consider the sign descriptions of linear recurrence sequences. This is the infinite word that results by replacing positive elements with the letter +, negative elements with the letter −, and leaving 0 as is. We prove that it is decidable whether the sign description of a simple linear recurrence sequence has a given prefix-independent omega-regular property. This is achieved by showing that such sequences are almost-periodic. To complement this result, we prove that sign descriptions of general linear recurrence sequences need not be almost-periodic.

• 15:36 – 15:43 Raphaël Berthon: Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes

  Poster:

  

  Slides:

  open
  

  Abstract:

  We consider algorithms to decide the existence of strategies in MDPs for Boolean combinations of objectives. These objectives are omega-regular properties that need to be enforced either almost surely or with non-zero probability, as usual in MDPs, surely as in games, or existentially as in automata. In this setting, relevant strategies are randomized infinite memory strategies: both infinite memory and randomization may be needed to play optimally. We provide algorithms to solve the general case of Boolean combinations and we also investigate relevant subcases. We further report on complexity bounds for these problems.

• 15:43 – 15:50 Debraj Chakraborty: Monte Carlo Tree Search guided by Symbolic Advice for MDPs

  Poster:

  

  Slides:

  open
  

  Abstract:

  I will talk about online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). The MCTS algorithm is augmented with the notion of symbolic advice. Symbolic advice are used to bias the selection and simulation strategies of MCTS while still maintaining its classical theoretical guarantees. I will describe how to use QBF and SAT solvers and BDD-based model checkers to implement symbolic advice in an efficient way. Our algorithm will be illustrated using the popular game Pac-Man where its performance exceed those of plain MCTS as well as the performances of human players. This talk is based on the joint work with Damien Busatto-Gaston, Gilles Geeraerts and Jean-Francois Raskin. Preprint of the paper based on the work can be found here: https://arxiv.org/abs/2006.04712

• 15:50 – 15:57 Kush Grover: An Anytime Algorithm for Reachability on Uncountable MDP

  Poster:

  

  Slides:

  open
  

  Abstract:

  We provide an algorithm for reachability on Markov decision processes with uncountable state and action spaces, which, under mild assumptions, approximates the optimal value to any desired precision. It is the first such anytime algorithm, meaning that at any point in time it can return the current approximation with its precision. Moreover, it simultaneously is the first algorithm able to utilize learning approaches without sacrificing guarantees and it further allows for combination with existing heuristics.

• 15:57 – 16:04 Tobias Meggendorfer: The Core of Markov Decision Processes

  Poster:

  

  Slides:

  open
  

  Abstract:

  We present the novel notion of cores, a simple yet versatile idea for the analysis of Markov chains and decision processes. In essence, a core comprises all relevant states of a system, omitting hardly reachable areas, since they only provide a miniscule contribution to any objective. As such, cores can be viewed as a pre-processing step, trading speed for precision in subsequent analysis. We sketch the computational complexity of identifying cores, introduce an efficient best-effort approach to practically solve this problem, and derive several additional applications going far beyond the pre-processing perspective.

• 16:04 – 16:11 Emanuel Martinov: Multi-Objective Reachability for context-free MDPs

  Poster:

  

  Abstract:

  We study qualitative multi-objective reachability problems for context-free MDPs, or equivalently Ordered Branching Markov Decision Processes (OBMDPs), building on prior results on single-target reachability for Branching Markov Decision Processes (BMDPs). We provide two separate algorithms for “almost-sure” and “limit-sure” multi-target reachability for OBMDPs.

• 16:11- 16:18 Simon Jantsch: Farkas certificates and minimal witnesses for probabilistic reachability constraints

  Poster:

  

  Abstract:

  We introduce Farkas certificates for upper and lower bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP). Farkas certificates are solutions of linear inequation systems that we derive from the transition matrix of the MDP using a variant of Farkas Lemma. We show that the inequation system is satisfiable if and only if the corresponding reachability constraint is satisfied in the MDP, and hence a satisfying vector indeed constitutes a certificate. Besides certification, we show that Farkas certificates can be related to “witnessing subsystems”, which are a standard notion of witness to lower-bounded thresholds on reachability probabilities. The idea is that if the reachability probability is above a certain threshold, this can be witnessed by a (possibly small) subsystem that by itself carries enough probability to reach the target (where all states that are not in the subsystem are assumed to have reachability probability zero). We show that a Farkas certificate with K non-zero entries can be translated into a witnessing subsystem with K states, and vice versa. This yields novel mixed integer linear programming formulations for computing minimal witnessing subsystems, and a heuristic approach that works by finding Farkas certificates with many zero-entries. The heuristic uses iterative calls to an LP-solver and is competitive when compared with existing methods. We also establish NP-completeness of deciding whether a witnessing subsystem with more than K states exists already for acyclic Markov chains. This presentation is based on joint work with Christel Baier and Florian Funke published at TACAS’20.

16:18 — 17:00 Session 6: POSTER SESSION

9:00 — 10:00 Session 7: INVITED TALK 2
chair: Szymon Torunczyk

• 9:00 – 10:00 Michael Benedikt: Nested Data, Interpolation, and Synthesis

  Abstract:

  This talk will be about nested sets — basically, finite levels of the cumulative hierarchy in set theory. The first part of the presentation will review some languages proposed for defining transformations on nested sets from a few decades ago. The next part will go into some connections of these languages with interpretations, interpolation, and intuitionistic logic, based on joint work with Pierre Pradic.

10:15 — 11:18 Session 8A: VERIFICATION & TEMPORAL LOGICS
chair: Cyriac Aiswarya

• 10:15 – 10:22 Chris Köcher: Reachability Problems in Multi-Queue Automata

  Poster:

  

  Abstract:

  In this talk, we will focus on automata having multiple reliable queues which are partially synchronized. This means, whenever we write or read some letter we do this operation on a specified subset of these queues at the same time. For example, with the help of these machines we can easily simulate networks of finite automata which communicate through some reliable channels, so-called communicating automata. However, these partially synchronized multi-queue automata are more general since we are able to synchronize the contents of two specified channels while other channels can be handled asynchronously. Note that this model also covers automata having one or more queues without any synchronization. Obviously, the reachability problem of these machines is undecidable. Hence, we need some approximation of this problem. This can be done step by step by computation of all configurations after application of n atomic queue operations for some increasing natural number n. Using this approach we obtain an algorithm which semi-decides the reachability problem. However, this approximation is very inefficient since we always explore only a finite space of reachable configurations. Boigelot et al. improved this approximation by introduction of so-called meta-transformations. These are special sets of transformation sequences such that we can easily compute the set of reachable configurations. Boigelot et al. focused on single- and (asynchronous) multi-queue automata looping through a single sequence of transformations t. In other words, given a recognizable set C of configurations and some special transformation sequence t, the authors have proven that the set configurations reachable from C via t^* is effectively recognizable. Here, we generalize this result to our partially synchronized multi-queue automata. We also consider some special recognizable sets T of transformation sequences such that we can compute a recognizable set of configurations which are reachable via the transformation sequences in T^*. Concretely, we consider such recognizable sets of transformation sequences which are alternating between two sets of write actions and read actions. For these sets we prove that, starting from a given recognizable set of configurations we will end up in an effectively recognizable set of configurations after application of these transformation sequences.

• 10:22 – 10:29 Pascal Baumann: The complexity of bounded context switching with dynamic thread creation

  Poster:

  

  Slides:

  open
  

  Abstract:

  Dynamic networks of concurrent pushdown systems (DCPS) are a theoretical model for multi-threaded recursive programs with shared global state and dynamical creation of threads. The reachability problem for DCPS is undecidable in general, but Atig et al. (2009) showed that it becomes decidable, and is in 2EXPSPACE, when each thread is restricted to a fixed number of context switches. The best known lower bound for the problem is EXPSPACE-hard and this lower bound follows already when each thread is a finite-state machine and runs atomically to completion (i.e., does not switch contexts). In our paper, we close the gap by showing that reachability is 2EXPSPACE-hard already with only one context switch. Interestingly, reachability analysis is in EXPSPACE both for pushdown threads without context switches as well as for finite-state threads with arbitrary context switches. Thus, recursive threads together with a single context switch provides an exponential advantage. Our proof techniques are of independent interest for 2EXPSPACE-hardness results. We introduce transducer-defined Petri nets, a succinct form for Petri nets, and show coverability is 2EXPSPACE-hard for this model. To show 2EXPSPACE-hardness, we present a modified version of Lipton’s simulation of counter machines by Petri nets, where the net programs can make explicit recursive procedure calls up to a bounded depth.

• 10:29 – 10:36 Stefanie Mühlberger: Neural Network Abstraction for Accelerating Verification

  Poster:

  

  Abstract:

  While abstraction is a classic tool of verification, it is not often in use for verification of neural networks. We introduce an abstraction framework applicable to feed-forward networks. For the particular case of ReLU, we can provide error bounds incurred by the abstraction. We show how the abstraction reduces the size of the network, while preserving its accuracy and how verification results on the abstract network can be transferred back to the original network.

• 10:36 – 10:43 Quentin Peyras: Expressive and Decidable Fragments of Many-Sorted First-Order Linear Temporal Logic

  Abstract:

  First-Order Linear Temporal Logic (FOLTL) provides a natural way of specifying infinite-state systems with both a rich structure and dynamic aspects. However, formally verifying properties of such specifications is challenging since (MS)FOLTL is not even semi-decidable. We address this situation by exhibiting decidable fragments of FOLTL that are rather expressive. However, some limitations remain that prevent the expression of some behaviors of infinite-state transition systems. Therefore, we devise some additional syntactic transformations that allow formulas to fall in one of our fragments. These techniques have been applied to various specifications to prove safety and liveness properties.

• 10:43 – 10:50 Rajarshi Roy: Learning Interpretable Models in the Property Specification Language

  Poster:

  

  Abstract:

  We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of the recent work in this area, which focuses on descriptions expressed in Linear Temporal Logic (LTL), we develop a learning algorithm for formulas in the IEEE standard temporal logic: Property Specification Language (PSL). Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in LTL, whereas it is easy to express such properties in PSL. Moreover, formulas in PSL can be more succinct and easier to interpret (due to the use of regular expressions in PSL formulas) than formulas in LTL. The learning algorithm we designed builds on %top of an existing algorithm for learning LTL formulas. a framework recently proposed for learning LTL formulas. Roughly speaking, our algorithm reduces the learning task to a constraint satisfaction problem in propositional logic and uses a SAT solver to search for a solution. We have implemented our algorithm and performed a comparative study between the proposed method and the existing LTL learning algorithm. Our results illustrate the effectiveness of the proposed approach to provide succinct human-interpretable descriptions from examples.

• 10:50 – 10:57 Yehia Abd Alrahman: Reconfigurable Interaction for MAS Modelling

  Poster:

  

  Abstract:

  In this talk, I will present a formalism to model and reason about multi-agent systems. The formalism allows agents to interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. The formalism defines a local behaviour based on shared variables and a global one based on message passing. I will also present an extension to LTL for reasoning explicitly about the intentions of the different agents and their interaction protocols. Finally, I will present a complexity result on satisfiability and model-checking of this extension. This talk is based on a recent paper accepted for AAMAS 2020 and co-authored with Giuseppe Perelli and Nir Piterman.

• 10:57 – 11:04 Marco Sälzer: On Finite Convergence of Fixpoints in the Modal Mu-Calculus

  Poster:

  

  Abstract:

  We investigate a word-structure with infinite bisimulation quotient that guarantees finite convergence of all fixpoints definable in the modal mu-calculus. To underline that this result is caused by the logic and not the specific structure we show that an extension of the modal mu-calculus, called the higher-order fixpoint logic, achieves non-finite convergence over the same word-structure.

• 11:04 – 11:11 Nicola Gigante: One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+P

  Poster:

  

  Abstract:

• 11:11 – 11:18 Yury Savateev: Deciding FO-Rewritability Of Ontology-Mediated Queries In Linear Temporal Logic

  Poster:

  

  Abstract:

  We investigate the computational complexity of deciding whether an ontology-mediated query formulated in linear temporal logic LTL is rewritable to an FO(<)-sentence. This problem originates in ontology-based data access to temporal data. We show that, for various fragments of LTL, deciding FO(<)-rewritability can be ExpSpace-, PSpace-, \Pi_2^p- and coNP-complete.

10:15 — 11:18 Session 8B: WEIGHTS & TRANSDUCERS
chair: Laure Daviaud

• 10:15 – 10:22 Rajit Datta: Equivalence Testing of Weighted Automata over Partially Commutative Monoids

  Poster:

  

  Slides:

  open
  

  Abstract:

  We study the equivalence testing of automata over partially commutative monoids (pc monoids) and show efficient algorithms in special cases, exploiting the structure of the underlying non-commutation graph of the monoid. Specifically, if the clique edge cover number of the non-commutation graph of the pc monoid is a constant, we obtain a deterministic quasi-polynomial time algorithm. As a consequence, we also obtain the first deterministic quasi-polynomial time algorithms for equivalence testing of k-tape weighted automata and for equivalence testing of deterministic k-tape automata for constant k. Prior to this, a randomized polynomial-time algorithm for the above problems was shown by Worrell [ICALP 2013]. We also consider pc monoids for which the non-commutation graphs have cover consisting of at most k cliques and star graphs for any constant k. We obtain randomized polynomial-time algorithm for equivalence testing of weighted automata over such monoids. Our results are obtained by designing efficient zero testing algorithms for weighted automata over such pc monoids.

• 10:22 – 10:29 Nicolas Waldburger: Path search with weight constraints

  Poster:

  

  Abstract:

  Path search in weighted directed graphs is a fundamental and widely studied algorithmic problem. While it is typical to consider the problem of optimizing the weight of a path between two given points, in practical applications such paths may be subjected to some weight constraints to model resource bounds or broken links in networks. In this talk we consider path problems subject to: (1) Lower-bound constraints requiring that the accumulated weight along a path is always above a bound. As an example, one might require that the energy level along the path is always nonnegative. (2) Equality constraints that allow some vertices to be used only if the accumulated weight is equal to a guard. For instance, an equality constraint on a target point allows to control the exact amount of energy used. (3) Disequality constraints that forbid access to some vertices if the accumulated weight is equal to a guard. This type of constraints helps modeling broken links or flooded paths. The complexity of a path search problem in weighted graphs depends on the combination of constraints that is allowed. The problem is in NC if only lower-bound constraints are allowed(i.e., as in the counters of a VASS) [Almagoretall, 2019]. It becomes NP-complete if in addition equality constraints are allowed [Haaseetall, 2009], and PSPACE-complete if arbitrary inequality constraints are allowed. The reachability problem with inequality constraints has indeed been related to timed automata and used to resolve a longstanding open question about reachability in that setting [Fearnleyetall, 2013]. An outstanding open problem is the case of path search with lower-bound, equality and disequality constraints. In this case the problem is known to lie between NP and PSPACE. In this talk we show that the problem remains in NP in the case of a single disequality constraint. We conjecture that the problem is in NP in the case of a fixed number k of disequality tests and are working to generalize the above-mentioned proof. This undergoing work is in collaboration with Mahsa Shirmohammadi.

• 10:29 – 10:36 Sarah Winter: Synthesis from Weighted Specifications over Finite Words

  Poster:

  

  Abstract:

  A (Boolean) finite word specification S is a binary relation of finite words. The domain of S, which is all words u such that (u,v) belongs to S for some v, may be a strict subset of the set of all words. The (Boolean) synthesis problem on finite words, asks, given such a specification S, whether there exists a function f from the domain of S into words such that (i) for all words u in the domain of S, (u,f(u)) belongs to S, and (ii) f is computable by some finite-state machine (a transducer). In this paper, we consider three quantitative extensions of this synthesis problem, through weighted specifications S which maps pairs of words to a rational value or -infinity, in which requirement (i) of the Boolean synthesis problem is respectively replaced by the following conditions: — threshold synthesis — S(u,f(u))>=t for some rational threshold t, — best-value synthesis — S(u,f(u)) is the best-value which can be achieved knowing u, i.e. f picks the output that maximizes the value, and — approximate synthesis — S(u,f(u)) is r-close from the best-value, for a given rational threshold r. We establish a landscape of decidability results for these three extensions and (synchronous) weighted specifications given by deterministic weighted automata equipped with sum, discounted sum and average measures. Such specifications are not regular in general and we develop an infinite game framework to solve the corresponding synthesis problems, namely the class of (weighted) critical prefix games, which are tailored to handle specifications with partial domain. Our decidability results entail decidability of quantitative extensions of the Church synthesis problem over infinite words, for some classes of weighted safety specifications. Finally, we also address several decidable and undecidable extensions of our setting, when the specification is given by an unambiguous weighted automaton and when the relation between input and output words is automatic.

• 10:36 – 10:43 Pierre Ohlmann: On the complexity of the sequential flow problem

  Poster:

  

  Abstract:

  A flow system over a finite set Q of states is given by a finite set C of actions, which are directed graphs over Q with arcs labelled by capacities, that is, either a non-negative number or ∞. When the controller plays an given action, any number of token which is in q and below the capacity of an arc from q to q’ may be moved to q’. The sequential flow problem (SFP) is a control problem in such a system which considers arbitrary number of tokens: is it the case that for any number n of tokens in a designated source state s, the controller may find a sequence of actions that leads all tokens to a designated target state t? The SFP was introduced in the context of stochastic control problems of arbitrary numbers of agents, and its complexity remains open. In this talk, I will present an existing EXPSPACE algorithm, and present ongoing work towards a PSPACE upper bound. This is the result of joint ongoing works with Thomas Colcombet, Nathanaël Fijalkow, Mahsa Shirmohammadi and Arnaud Sangnier.

• 10:43 – 10:50 Suguman Bansal: Automata-Based Quantitative Reasoning

  Abstract:

  Existing solution approaches for problems in {\em quantitative analysis} suffer from two challenges that adversely impact their theoretical understanding, and large-scale applicability due to limitations on scalability. These are the {\em lack of generalizability}, and {\em separation-of-techniques}. Lack of generalizability refers to the issue that solution approaches are often specialized to the underlying {\em cost model} that evaluates the quantitative property. Different cost models deploy such disparate algorithms that there is no transfer of knowledge from one cost model to another. Separation-of-techniques refers to the inherent dichotomy in solving problems in quantitative analysis. Most algorithms comprise of two phases: A {\em structural phase}, which reasons about the structure of the quantitative system(s) using techniques from automata or graphs; and a {\em numerical phase}, which reasons about the quantitative dimension/cost model using numerical methods. The techniques used in both phases are so unlike each other that they are difficult to combine, forcing the phases to be performed sequentially, thereby impacting scalability. This abstract summarizes my thesis work~\cite{PhDThesis}, which contributes towards a novel framework that addresses the aforementioned challenges. The introduced framework, called {\em comparator automata} or {\em comparators} in short, builds on automata-theoretic foundations to generalize across a variety of cost models. The crux of comparators is that they enable automata-based methods in the numerical phase, hence eradicating the dependence on numerical methods. In doing so, comparators are able to integrate the structural and numerical phases. On the theoretical front, we demonstrate that comparator-based solutions have the advantage of generalizable results, and yield complexity-theoretic improvements over a range of problems in quantitative analysis. On the practical front, we demonstrate through empirical analysis that comparator-based solutions render more efficient, scalable, and robust performance, and hold the ability to integrate quantitative with qualitative objectives.

• 10:50 – 10:57 Janusz Schmude: Some remarks on deciding equivalence for graph-to-graph transducers

  Poster:

  

  Slides:

  open
  

  Abstract:

  We study the following decision problem: given two mso transductions that input and output graphs of bounded treewidth, decide if they are equivalent, i.e. isomorphic inputs give isomorphic outputs. We do not know if this problem is decidable, but we propose an approach to deciding the problem which uses algebra. We show how the approach can be successful for a variant of the problem, where instead of isomorphism on output graphs, we consider certain relaxation of isomorphism. Our solution uses a variant of polynomial transducers, extended with a division operation. This is joint work with Mikołaj Bojańczyk.

• 10:57 – 11:04 Sandra Kiefer: String-to-String Interpretations with Polynomial-Size Output

  Abstract:

  String-to-string MSO interpretations are like Courcelle’s MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial in the input length, as opposed to MSO transductions, which have output of linear length. We show that string-to-string MSO interpretations are exactly the polyregular functions. The latter class has various characterizations, one of which is that it consists of the string-to-string functions recognized by pebble transducers. Our main result implies the surprising fact that string-to-string MSO interpretations are closed under composition. This is joint work with Mikołaj Bojańczyk and Nathan Lhote and the corresponding paper was published at ICALP 2019. (It has not yet been presented at Highlights.)

• 11:04 – 11:11 Rafał Stefański: Single-use automata and transducers for infinite alphabets

  Poster:

  

  Abstract:

  Our starting point are register automata for data words, in the style of Kaminski and Francez. We study the effects of the single-use restriction, which says that a register is emptied immediately after being used. We show that under the single-use restriction, the theory of automata for data words becomes much more robust. The main results are: (a) five different machine models are equivalent as language acceptors, including one-way and two-way single-use register automata; (b) one can recover some of the algebraic theory of languages over finite alphabets, including a version of the Krohn-Rhodes Theorem; (c) there is also a robust theory of transducers, with four equivalent models, including two-way single use transducers and a variant of streaming string transducers for data words. These results are in contrast with automata for data words without the single-use restriction, where essentially all models are pairwise non-equivalent This is a joint work with Mikołaj Bojańczyk.

• 11:11 – 11:18 Léo Exibard: On Computability of Data Word Functions Defined by Transducers

  Poster:

  

  Abstract:

  In this paper, we investigate the problem of synthesizing computable functions of infinite words over an infinite alphabet (data omega-words). The notion of computability is defined through Turing machines with infinite inputs which can produce the corresponding infinite outputs in the limit. We use non-deterministic transducers equipped with registers, an extension of register automata with outputs, to specify functions. Such transducers may not define functions but more generally relations of data omega-words, and we show that it is PSpace-complete to test whether a given transducer defines a function. Then, given a function defined by some register transducer, we show that it is decidable (and again, PSpace-complete) whether such function is computable. As for the known finite alphabet case, we show that computability and continuity coincide for functions defined by register transducers, and show how to decide continuity. We also define a subclass for which those problems are PTime.

11:18 — 12:00 Session 9: POSTER SESSION

14:00 — 15:00 Session 10: INVITED TALK 3
chair: Gabriele Puppis

• 14:00 – 15:00 Anca Muscholl: On word transducers with origins

  Abstract:

  The origin semantics for transducers has been proposed 2014 by M. Bojanczyk, and shown to provide a machine independent characterization of regular word-to-word functions. Another nice feature of this semantics is that it helps to recover decidability for some basic problems. In this talk I will review various results about the decidability problem under the origin semantics and the resynchronisation formalism for regular word-to-word functions.

15:15 — 16:11 Session 11A: GAMES II
chair: Tony Kucera

• 15:15 – 15:22 Dmitry Chistikov: Globe-hopping

  Poster:

  

  Abstract:

  In the first part of this talk, I will introduce and briefly discuss a geometric puzzle, based on recent joint work with Goulko, Kent, and Paterson (in press). I will then pose questions in computational logics that this puzzle presents, more generally. In this second and main part of the talk, I will not offer answers and just ask questions.

• 15:22 – 15:29 Martin Zimmermann: Optimally Resilient Strategies in Pushdown Safety Games

  Poster:

  

  Abstract:

  Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic disturbances, i.e., unmodeled situations in which the actual controller action differs from the intended one. For games played on finite arenas it is known that computing optimally resilient strategies only incurs a polynomial overhead over solving classical games. This paper studies safety games with disturbances played on infinite arenas induced by pushdown systems. We show how to compute optimally resilient strategies in triply-exponential time. For the subclass of safety games played on one-counter configuration graphs, we show that determining the degree of resilience of the initial configuration is PSPACE-complete and that optimally resilient strategies can be computed in doubly-exponential time.

• 15:29 – 15:36 Guy Avni: Infinite-Duration All-Pay Bidding Games

  Poster:

  

  Abstract:

  A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In “bidding games”, in each turn, we hold an ‘auction’ (bidding) to determine which player moves the token. The players simultaneously submit bids and the higher bidder moves the token. Several different payment schemes have been considered. In “first-price” bidding, only the higher bidder pays his bid, while in “all-pay” bidding, both players pay their bids. Bidding games were largely studied with variants of first-price bidding. In this work, we study, for the first time, infinite-duration all-pay bidding games, and show that they exhibit elegant mathematical properties similar to their first-price counterparts; namely, an equivalence with “random-turn games”, which is a subclass of stochastic games. This is in stark contrast with reachability all-pay bidding games, which were recently shown to be technically much more complicated than reachability first-price bidding games. Another orthogonal distinction between the bidding rules is in the recipient of the payments: in “Richman” bidding, the bids are paid to the other player, and in “poorman” bidding, the bids are paid to the ‘bank’. We show a complete picture for the four bidding mechanisms. We focus on strongly-connected games. We first address Richman bidding. A simple argument shows that deterministic strategies cannot guarantee anything with this bidding mechanism. The main technical challenge is showing that with probabilistic strategies and mean-payoff objectives, the optimal expected payoff under all-pay bidding equals the optimal (deterministic) payoff under first-price bidding. We also construct almost-sure winning strategies for parity games. We find the properties of poorman bidding surprising in light of these results. First, in contrast to Richman bidding, deterministic strategies are useful and guarantee a payoff that is only slightly lower than the optimal payoff under first-price poorman bidding. This gives rise to winning strategies in parity games. Second, we show that under probabilistic strategies, the optimal expected payoff for the player with the larger budget is higher than the optimal payoff under first-price poorman bidding. Our proofs are constructive. In addition, for both Richman and poorman bidding we revisit the constructions for first-price bidding and significantly simplify them. Joint work with Ismael Jecker and Djordje Zikelic. The full version can be found online: https://arxiv.org/abs/2005.06636

• 15:36 – 15:43 Alexander Kozachinskiy: Positionality and strategy improvement for continuous payoffs

  Slides:

  open
  

  Abstract:

  A fundamental question for two-player antagonistic games on finite directed graphs is to characterize positional payoffs, i.e., payoffs that always have optimal positional strategies. We investigate this question in a special case of continuous payoffs, both for deterministic and for stochastic games. A well-studied example of a continuous positional payoff is the (multi)discounted payoff. We show that in case of stochastic games the multidiscounted payoff is, in fact, the only continuous payoff which is positional. In contrast, the class of continuous deterministically positional payoffs turns out to be wider. Thus, we answer negatively to a question of Gimbert (STACS 2007), who conjectured that all deterministically positional payoffs are stochastically positional. We then obtain a simple characterization of the class of deterministically positional continuous payoffs. Namely, we introduce a property that we call prefix-monotonocity and show that this property is necessary and sufficient for a continuous payoff to be (deterministically) positional. The machinery of our proofs has some further consequences. Namely, it turns out that any game with a continuous positional payoff can be solved by strategy improvement (in fact, we use strategy improvement in the proof of sufficiency of prefix-monotonocity). From that we also derive that any such game can formulated as an LP-type problem and thus can be solved in randomized sub-exponential time. Finally, we address the question of showing strong bounds on strategy improvement for continuous payoffs. We generalize edge eliminating technique which was originally developed to show strong bounds on strategy improvement for the multidiscounted payoff. We show that some results obtained with this technique can be applied to other continuous payoffs too, including one that we call non-linear discounted payoff.

• 15:43 – 15:50 Shibashis Guha: Stackelberg mean-payoff games with one epsilon-optimal adversarial follower

  Poster:

  

  Slides:

  open
  

  Abstract:

  Two-player Stackelberg games are non-zero sum strategic games comprising of a leader (Player 0) and a follower (Player 1). The leader announces her strategy, and the follower responds by playing an optimal response (or an epsilon-optimal response) to maximise his own payoff. The follower, while maximising his own payoff, can either be co-operative, that is, he chooses a response that maximises the payoff of the leader, or he can be adversarial, thus choosing a response that also minimises the payoff of the leader. In this work, we study Stackelberg games for two-player non-zero sum mean-payoff setting where the follower is adversarial and epsilon-optimal, for a fixed epsilon. The ASV-epsilon of Player 0 is the supremum of the values that Player 0 can obtain by announcing her strategy to Player 1 who in turn responds with an epsilon-optimal strategy. We prove that the ASV-epsilon is always achievable, possibly with an infinite memory strategy. This is in contrast with the framework of two-player Adversarial Stackelberg mean-payoff games where the epsilon is not fixed. We show that the threshold problem, i.e. given a rational constant c, deciding whether ASV-epsilon > c, is in NP, and a finite memory strategy for Player 0 suffices to achieve the threshold. We also give an EXPTime algorithm to compute the ASV-epsilon. Furthermore, we study the effect on ASV-epsilon when Player 0 is restricted to only finite memory strategies. Finally, we improve upon some of the results obtained earlier in the framework of two-player Adversarial Stackelberg mean-payoff games where the epsilon is not fixed. This is a joint work with Mrudula Balachander and Jean-François Raskin.

• 15:50 – 15:57 Soumyajit Paul: A Bridge between Polynomial Optimization and Games with Imperfect Recall

  Poster:

  

  Abstract:

  In games with Imperfect information players have only partial knowledge about their position in the game. This makes it difficult to compute optimal strategies. We consider two player zero-sum games with imperfect information modeled in the extensive form and provide several complexity results on computing maxmin values. We work with complexity classes involving computation over reals, more precisely fragments of the First Order Theory of Reals. In the process we draw connections between some multivariate polynomial optimization problems and the maxmin computation in imperfect information games. This is joint work with Hugo Gimbert and B. Srivathsan that was presented at AAMAS’20.

• 15:57 – 16:04 Julia Eisentraut: Expected Cost Analysis of Attack-Defense Trees using Stochastic Games

  Poster:

  

  Abstract:

  Joint work with Jan Křetínský (published at QEST 2019) Attack-defense trees (ADT) are an established formalism for assessing system security. In this talk, I present an extension of ADT with costs and success probabilities and present a framework to analyze the probability of a successful attack/defense, its expected cost, and its probability for a given maximum cost. Analysis requires to model the problem using sequential decision-making and non-tree structures, in contrast to classical ADT analysis. On the technical side, I show three algorithms: (i) reduction to PRISM-games, (ii) dedicated game solution utilizing the structure of the problem, and (iii) direct analysis of ADT for certain settings.

• 16:04 – 16:11 David Klaška: Adversarial Patrolling with Drones

  Abstract:

  We investigate adversarial patrolling where the Defender is an autonomous device with a limited energy resource (e.g., a drone). Every eligible Defender’s policy must prevent draining the energy resource before arriving to a refill station, and this constraint substantially complicates the problem of computing an efficient Defender’s policy. Furthermore, the existing infinite-horizon models assume Attackers with unbounded patience willing to wait arbitrarily long for a good attack opportunity. We show this assumption is inappropriate in the setting with drones because here the expected waiting time for an optimal attack opportunity can be extremely large. To overcome this problem, we introduce and justify a new concept of impatient Attacker, and design a polynomial time algorithm for computing a Defender’s policy achieving protection close to the optimal value against an impatient Attacker. Since our algorithm can quickly evaluate the protection achievable for various topologies of refill stations, we can also optimize their displacement. We implement the algorithm and demonstrate its functionality on instances of realistic size.

15:15 — 16:04 Session 11B: ALGEBRA
chair: Anuj Dawar

• 15:15 – 15:22 Ismaël Jecker: A Ramsey Theorem for Finite Monoids

  Poster:

  

  Abstract:

  Repeated idempotent elements are commonly used to characterise iterable behaviours in abstract models of computation. Therefore, given a monoid M, it is natural to ask how long a sequence of elements of M needs to be to ensure the presence of consecutive idempotent factors. This question is formalised through the notion of the Ramsey function R of a finite monoid M, obtained by mapping every integer t to the minimal integer R(t) such that every sequence of elements of M of size R(t) admits t consecutive non-empty factors that correspond to the same idempotent element of M. In this talk, we study the behaviour of the Ramsey function R of a finite monoid M by investigating the regular D-length of M, defined as the size L(M) of the largest submonoid of M isomorphic to the set of natural numbers {1,2, …, L(M)} equipped with the Max operation. We will see that the regular D-length of M determines the degree of R, as t^L(M) ≤ R(t) ≤ (t|M|^4)^L(M). For some monoids, the regular D-length is considerably smaller than other parameters. For instance, the full monoid of transformations over n elements, which is used to express the transition monoids of deterministic automata, has a regular D-length of n+1, which is exponentially smaller than its size. Moreover, the full monoid of n x n Boolean matrices, which is used to express the transition monoids of non-deterministic automata, has a regular D-length of (n^2+n+2)/2, which is exponentially smaller than its largest chain of D-classes.

• 15:22 – 15:29 Florin Manea: Efficiently Testing Simon’s Congruence

  Poster:

  

  Slides:

  open
  

  Abstract:

  Simon’s congruence is defined as follows: two words are -equivalent if they have the same set of subsequences of length at most . We propose an algorithm which computes, given two words and , the largest for which . Our algorithm runs in linear time when the input words are over the integer alphabet (or other alphabets which can be sorted in linear time). This approach leads to an optimal algorithm in the case of general alphabets as well. Our results are based on a novel combinatorial approach and a series of efficient data structures.

• 15:29 – 15:36 Olivier Stietel: A categorical approach to regular cost functions

  Abstract:

  In this talk, we will explain how the objects studied for regular cost functions over words can be interpreted in a categorical framework. More precisely, we will describe a category in which the natural notions of recognizability via algebras coincide with the known notion of stabilization monoids, the central algebraic object in the study of regular cost functions over words. This is a joint work with Thomas Colcombet and Daniela Petrisan.

• 15:36 – 15:43 Moses Ganardi: The knapsack problem and the power word problem over wreath products

  Poster:

  

  Abstract:

  For a finitely generated group we study the power word problem and the knapsack problem. The power word problem asks whether a given equation holds where are group elements and are binary encoded integers. The knapsack problem asks whether a given equation has a solution in the natural numbers where are group elements. We prove that the power word problem for wreath products of the form with nilpotent and iterated wreath products of free abelian groups belongs to TC. As an application of the latter, the power word problem for free solvable groups is in TC. On the other hand we show that for wreath products , where is a so called uniformly strongly efficiently non-solvable group (which form a large subclass of non-solvable groups), the power word problem is coNP-hard. For the knapsack problem we show NP-completeness for iterated wreath products of free abelian groups and hence free solvable groups. Moreover, the knapsack problem for every wreath product , where is uniformly efficiently non-solvable, is -hard.

• 15:43 – 15:50 Achim Blumensath: Regular Tree Algebras

  Poster:

  

  Slides:

  open
  

  Abstract:

  We introduce a class of algebras that can be used as recognisers for regular tree languages. We show that it is the only such class that forms a pseudo-variety and we prove the existence of syntactic algebras.

• 15:50 – 15:57 Arthur Jaquard: Characterisation of a class of algebraically-defined languages of infinite trees

  Abstract:

  We use an algebraic structure based on preclones, and similar to those used by Blumensath, to describe languages of regular infinite trees, and we study the classes of languages that can be naturally defined using this framework. We give an exact characterisation of the class of languages whose syntactic algebra have bounded sorts, this result is also new in the case of finite trees. This is joint work with Thomas Colcombet.

• 15:57 – 16:04 Michaël Cadilhac: Rational subsets of Baumslag-Solitar groups

  Poster:

  

  Abstract:

  We consider the rational subset membership problem for Baumslag-Solitar groups. These groups form a prominent class in the area of algorithmic group theory, and they were recently identified as an obstacle for understanding the rational subsets of GL(2, Q). We show that rational subset membership for Baumslag-Solitar groups BS(1, q) with q ≥ 2 is decidable and PSPACE-complete. To this end, we introduce a word representation of the elements of BS(1, q): their pointed expansion (PE), an annotated q-ary expansion. Seeing subsets of BS(1, q) as word languages, this leads to a natural notion of PE-regular subsets of BS(1, q): these are the subsets of BS(1, q) whose sets of PE are regular languages. Our proof shows that every rational subset of BS(1, q) is PE-regular. Since the class of PE-regular subsets of BS(1, q) is well-equipped with closure properties, we obtain further applications of these results. Our results imply that (i) emptiness of Boolean combinations of rational subsets is decidable, (ii) membership to each fixed rational subset of BS(1, q) is decidable in logarithmic space, and (iii) it is decidable whether a given rational subset is recognizable. In particular, it is decidable whether a given finitely generated subgroup of BS(1, q) has finite index.

16:04 — 17:00 Session 12: POSTER SESSION

9:00 — 10:00 Session 13: INVITED TALK 4
chair: Karin Quaas

• 9:00 – 10:00 Stéphane Demri: Modal Logics for Updating, Sharing or Composing

  Abstract:

  Non-classical logics having a syntactical mechanism to update models are ubiquitous and include dynamic logics, separation logics or ambient logics to quote a few of them. More specifically, modal logics for updating models have been quite studied, see e.g. second-order modal logics, and more recently logics of public announcements, sabotage modal logics and modal separation logics. In this talk, recent developments on modal logics with built-in update mechanisms based on composition are presented as well as their relationships with other logical formalisms. Recent results about decidability status, computational complexity and expressive power are presented. Part of the talk is based on joint works with B. Bednarczyk, M. Deters, R. Fervari and A. Mansutti.

10:15 — 11:11 Session 14A: AUTOMATA & FORMAL LANGUAGES
chair: Denis Kuperberg

• 10:15 – 10:22 Salomon Sickert: An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata

  Poster:

  

  Abstract:

  In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form , where and contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata. This is joint work with Javier Esparza. The paper has been accepted at LICS’20 and an extended version is already available.

• 10:22 – 10:29 Jan Strejček: Advances in Emerson-Lei Automata

  Poster:

  

  Abstract:

  The talk presents two new results on Emerson-Lei automata. One is a new LTL to automata translator called ltl3tela. The tool produces nondeterministic or deterministic transition-based Emerson-Lei automata that are (on average) smaller than automata produced by state-of-the art translators. The second result is a new algorithm checking emptiness of Emerson-Lei automata. The algorithm has been implemented in Spot and PRISM and our experiments exhibit great performance improvements over previous solutions.

• 10:29 – 10:36 Kyveli Doveri: Inclusion Checking Algorithms for ω-Languages

  Poster:

  

  Abstract:

  We consider the inclusion problem for ω-languages. In particular we are interested in the cases such as the inclusion between two ω-regular languages or the inclusion problem of ω-context free languages into ω-regular languages. We built on an abstract interpretation based framework solving the inclusion problem for languages of finite words [Ganty et al., SAS, 2019] that was first presented at Highlights’18. Our approach can be summarised in two parts: first the reduction of the inclusion problem to an inclusion between the ultimate periodic subsets of the languages we consider. The ultimately periodic subset of an ω-language L is the subset of L containing all the words of the form uv^ω, where u and v are finite words referred to as the prefix and period, respectively. The advantage is that it admits a least fixed point characterisation. Second, the definition of abstractions build upon pairs of quasiorders on finite words that we derive from the language we want to check inclusion into. Intuitively, the first quasiorder of such a pair is used to reason on the prefixes of words uv^ω while the second one is used to reason on the periods. We obtain complete abstract interpretations, from which we derive sound and complete algorithms to decide the inclusion. This is joint work with Pierre Ganty.

• 10:36 – 10:43 Georg Zetzsche: Extensions of -Regular Languages

  Abstract:

  We consider extensions of monadic second-order logic over -words, which are obtained by adding one language that is not -regular. We show that if the added language has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the -regular languages are the only decidable Boolean-closed full trio over -words.

• 10:43 – 10:50 Doron Tiferet: Ambiguity Hierarchy of Regular Infinite Tree Languages

  Poster:

  

  Abstract:

  An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some k ∈ N. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. For automata over finite words (and over finite trees), on every input there are at most finitely many accepting computations. Hence, every automaton on finite words and on finite trees is finitely ambiguous. However, over ω-words and over infinite trees there are nondeterministic automata with uncountably many accepting computations. Over ω-words and over infinite trees, finitely ambiguous automata are a proper subclass of the class of countably ambiguous automata, which is a proper subclass of nondeterministic automata. The cardinality of the set of accepting computations of an automaton over an infinite tree t is bounded by the cardinality of the set of functions from the nodes of t to the state of the automaton, and therefore, it is at most continuum. The set of accepting computations on t is definable in Monadic Second-Order Logic (MSO). B´ar´any et al. showed that the continuum hypothesis holds for MSO-definable families of sets. Therefore, if the set of accepting computations of an automaton on a tree t is uncountable, then its cardinality is continuum. Hence, there are exactly two infinite degrees of ambiguity. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous if it is accepted by a k-ambiguous automaton. A language is boundedly ambiguous if it is k-ambiguous for some k; it is finitely (respectively, countably) ambiguous if it is accepted by a finitely (respectively, countably) ambiguous automaton. Over finite words, every regular language is accepted by a deterministic automaton. Over finite trees, every regular language is accepted by a deterministic bottom-up tree automaton and by an unambiguous top-down tree automaton. Over ω-words every regular language is accepted by an unambiguous B¨uchi automaton and by a deterministic parity automaton. Hence, the regular languages over finite words, over finite trees and over ω-words are unambiguous. Our main result states that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages which are not (k − 1)-ambiguous; there are finitely ambiguous languages which are not boundedly ambiguous; there are countably ambiguous languages which are not finitely ambiguous; there are uncountably ambiguous languages which are not countably ambiguous. A natural question is whether the ambiguity degree is decidable. We have not solved this question. However, relying on Niwi´nski’s characterization of countable regular languages we proved that every countable language is unambiguous. Joint work with Alexander Rabinovich.

• 10:50 – 10:57 Corentin Barloy: Multidimensional linear recursive sequences and universality of unambiguous register automata

  Poster:

  

  Abstract:

  In this work, we study the universality problem for \emph{unambiguous register automata} (URA) over equality atoms without guessing. Register automata are a generalisation of finite automata over infinite alphabets (called atoms) with the possibility of storing input data values in registers and check them for equality. A register automaton is unambiguous if, for every input word, it has at most one accepting run. The universality problem asks whether a given automaton recognizes every data word. For this model, it is known that inclusion, equivalence and universality problems are equivalent. The universality problem for nondeterministic register automata is undecidable, by a result of Kaminski and Francez. In the special case of URA, it has recently been proven to be in 2EXPSPACE by Mottet and Quaas by analysing the infinite-state system obtained by determinising the automaton. We provide an alternative approach to this problem, which goes back in spirit to the seminal work of Stearns and Hunt on unambiguous finite automata. Namely, we propose to count the number of orbits of data words accepted by the automaton, for fixed word length and number of distinct data values appearing therein. We show that the orbit counting function of a URA is \emph{bidimensional linear recursive}, i.e., it satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec). In the prototypical case of the counting function of the universal language over equality atoms, one gets the equation

     

  which, together with the initial conditions and for , yields the well-known Stirling numbers of the second kind. Since a URA is universal iff its counting function equals and linrec sequences are closed under difference, we reduce the URA universality problem to the zeroness problem of a linrec sequence. To solve the latter problem, we use tools from non-commutative algebra and elimination theory, and provide a detailed complexity analysis of the obtained algorithm. As a consequence, we provide an elementary bound on the number of terms that need to be checked in order conclude that a linrec sequence is identically zero. In turn, this yields an elementary bound on the shortest witness of non-universality for a URA language (if any). While this does not improve on the known 2EXPSPACE bound for the URA universality problem, we also show that for other atom structures such as the homogeneous total order, homogeneous equivalence relation, and the random graph we can similarly characterise the orbit counting function with a natural set of recursive equations. It is currently not known whether the URA universality problem is decidable for those more expressive atoms. However, for those more expressive classes the equations are not linrec and deciding their zeroness problem is left for future work. This is joint work with Lorenzo Clemente.

• 10:57 – 11:04 Joshua Moerman: Residuality and Learning for Register Automata

  Poster:

  

  Abstract:

  In this research we consider the problem of inferring a register automaton from observations. This has been done before for deterministic RA, but is still open for nondeterministic RA. To see why nondeterminism is interesting, consider the well-known learning algorithms L* and NL* for respectively deterministic and nondeterministic automata. Although the representation is different, they operate on the same class of languages (i.e., regular languages). This is not the case for RA, where nondeterminism gives a strictly bigger class of languages than determinism. So not only does the representation changes, so does the class of languages. Our contributions are as follows. This is joint work with Matteo Sammartino. – We consider \emph{residual automata} for data languages. We show that their languages form a proper subclass of all languages accepted by nondeterministic RA. – we give a \emph{machine-independent characterisation} of this class of languages. For this, we also develop some new results in nominal lattice theory. – We show that for this class of languages, L*-style algorithms exist. – The natural generalisation of NL* does not always terminate, surprisingly. Fortunately, the algorithm can be fixed to always terminate.

• 11:04 – 11:11 Jan Kretinsky: Automata Tutor v3

  Poster:

  

  Abstract:

  We present the third version of Automata Tutor, an online tool for helping teachers and students in large courses on automata and formal languages. It extends massively the functionality of the previous version, which has already been used by thousands of users in dozens of countries. This work will appear in CAV 2020. Although a non-research paper, it targets exactly the Highlights audience, aiming to help in the courses held by many of the attendees.

10:15 — 11:04 Session 14B: PETRI
chair: Christoph Haase

• 10:15 – 10:22 Ekanshdeep Gupta: The Well Structured Problem for Presburger Counter Machines

  Poster:

  

  Abstract:

  We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS. Joint work with Alain Finkel.

• 10:22 – 10:29 A. R. Balasubramanian: Complexity of controlled bad sequences over finite sets of N^d

  Poster:

  

  Abstract:

  We provide upper and lower bounds for the length of controlled bad sequences over the majoring and the minoring orderings of finite sets of . The results are obtained by bounding the length of such sequences by functions from the Cichon hierarchy. This allows us to translate these results to bounds over the fast-growing complexity classes. The obtained bounds are proven to be tight for the majoring ordering, which solves a problem left open by Abriola, Figueira and Senno (Theor. Comp. Sci, Vol. 603). Finally, we use the results on controlled bad sequences to prove upper bounds for the emptiness problem of some classes of automata.

• 10:29 – 10:36 Wojciech Czerwiński: Universality Problem for Unambiguous VASS

  Poster:

  

  Abstract:

  We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in dimension 1. When the dimension d ∈ N is fixed, the universality problem is PSpace-complete if d ≥ 2, and coNP-hard for 1-dimensional VASSes (also known as One Counter Nets).

• 10:36 – 10:43 Patrick Totzke: Parametrized Universality Problems for One-Counter Nets

  Poster:

  

  Slides:

  open
  

  Abstract:

  We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural decision problems: 1. does there exist an initial counter value that makes the language universal? 2. does there exist a sufficiently high ceiling so that the bounded language is universal? Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized variants seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet. This is joint work with Shaull Almagor, Udi Boker, and Piotr Hofman. The paper will be presented at CONCUR’20 and a full version is available on the arXiv: https://arxiv.org/abs/2005.03435.

• 10:43 – 10:50 Sławomir Lasota: Reachability in Fixed Dimension Vector Addition Systems with States

  Poster:

  

  Slides:

  open
  

  Abstract:

  The reachability problem is a central decision problem in verification of vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We discuss three recent results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We construct a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes -dimensional flat VASS from 2-dimensional ones. The third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14. The discussed results have been obtained in a joint work with Wojciech Czerwinski, Ranko Lazic, Jerome Leroux and Filip Mazowiecki.

• 10:50 – 10:57 Alex Dixon: KReach: A Tool for Reachability in Petri Nets

  Poster:

  

  Slides:

  open
  

  Abstract:

  We present KReach, a tool for deciding reachability in general Petri nets. The tool is a full implementation of Kosaraju’s original 1982 decision procedure for reachability in VASSs. We believe this to be the first implementation of its kind. KReach serves as a practical tool, and acts as an effective teaching aid for the theory behind the algorithm. Preliminary tests suggest that there are some classes of nets where we can quickly show unreachability. In particular, using KReach for coverability problems, by reduction to reachability, is highly competitive even against state-of-the-art coverability checkers. This is joint work with Ranko Lazic. The conference paper is available at http://wrap.warwick.ac.uk/134045/ .

• 10:57 – 11:04 Chana Weil-Kennedy: Flatness of Branching Immediate Observation Petri Nets

  Poster:

  

  Abstract:

  This presentation is based on joint work with Mikhail Raskin and Javier Esparza, on a paper submitted to CONCUR 2020 (repository link: https://arxiv.org/abs/2001.09966). In previous work we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. We showed that the reachability problem for these nets is PSPACE-complete, far simpler that the non-elementary complexity of this central problem for general Petri nets. Now we show that IO nets are flat, so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. We extend IO nets to a new class, Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer flat, and their sets of reachable markings may be non-semilinear, they are still locally flat (pre^* flat to be precise). As a consequence, the coverability and reachability problem for BIO nets, and even a certain parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relations for which the reachability problem is provably simpler than for general Petri nets.

10:59 — 12:00 Session 15: POSTER SESSION