17–20 SEPTEMBER 2019
10 June: Submission deadline
20 June: Notification
31 August: Early registration deadline
17 September: Tutorial day
18–20 September: Conference
10 June: Submission deadline
20 June: Notification
31 August: Early registration deadline
17 September: Tutorial day
18–20 September: Conference
The goal of Highlights conferences is to integrate the community working on logic, games and automata.
10 June AoE: Submission deadline
20 June: Notification
31 August: Early registration deadline
17 September 2019: Tutorial day
18–20 September 2019: Conference
There are no proceedings. You present your best work, be it published elsewhere or yet unpublished.
The conference is three days long. The contributed talks are around ten minutes.
The participation costs are modest. Warsaw is easy to reach.
Let's use the conference model that is so successful in other fields, like mathematics.
The early registration deadline is August 31; later registration will incur additional cost.
All lectures will take place at the Warsaw University Library, which is located here. The address is:
Dobra 55/56, 00-312 Warsaw
The library is in walking distance from Warsaw University’s main Campus. The bus stop “Uniwersytet” at Krakowskie Przedmieście Street is frequented by multiple buses, including the bus line 175 connecting directly with Chopin Airport and the Central Railway Station. Also, the library is in walking distance from the metro station “Centrum Nauki Kopernik” on line M2.
An informal picnic will take place on Thursday, September 19 at 7pm, on Vistula’s river banks, near the library. The participants are asked to bring something to drink and eat with them.
Registration
Tutorial 1 (Part 1)
Sebastian Siebertz: Nowhere dense graph classes and algorithmic applications
Abstract:
The notion of nowhere denseness was introduced by Nešetřil and Ossona de Mendez and provides a robust concept of uniform sparseness of graph classes. Nowhere dense graph classes generalize many familiar classes of sparse graphs such as the class of planar graphs and classes that exclude a fixed minor or topological minor. They admit several seemingly unrelated natural characterisations that lead to strong algorithmic applications. In particular, the model-checking problem for first-order logic is fixed-parameter tractable over these classes. In this tutorial I will give an introduction to the theory of nowhere dense graph classes with a focus on different characterisations and algorithmic applications.coffee
Tutorial 1 (Part 2)
Sebastian Siebertz: Nowhere dense graph classes and algorithmic applications
Abstract:
The notion of nowhere denseness was introduced by Nešetřil and Ossona de Mendez and provides a robust concept of uniform sparseness of graph classes. Nowhere dense graph classes generalize many familiar classes of sparse graphs such as the class of planar graphs and classes that exclude a fixed minor or topological minor. They admit several seemingly unrelated natural characterisations that lead to strong algorithmic applications. In particular, the model-checking problem for first-order logic is fixed-parameter tractable over these classes. In this tutorial I will give an introduction to the theory of nowhere dense graph classes with a focus on different characterisations and algorithmic applications.lunch break
Tutorial 2 (Part 1)
Guy Avni: Formal Methods Meets Algorithmic Game Theory
Abstract:
Many problems in computer science, math, and economics can naturally be described as a game. As a result, various sub-fields in these disciplines study different types of games. The tutorial describes useful and interesting recent connections between formal methods and algorithmic game theory (AGT, for short). The goal in formal methods is to formally reason about systems. The traditional games that are studied in formal methods are called graph games and they model the interaction between a reactive system and its hostile environment. These are typically ongoing two-player zero-sum games of infinite duration. On the other hand, AGT lies in the intersection between computer science and economics. The games studied in AGT are typically multi-player, non-zero-sum, and one-shot games. We will focus on two meeting points between the two fields. The first is “bidding games”, which are graph games in which in each turn, an auction is held in order to determine which player moves next. We study the effect of using different bidding mechanisms on the properties of the game, and reveal an intriguing connection between bidding games and a fragment of stochastic games called “random-turn games”. In the the second meeting point, we will focus on “network games” (sometimes called “congestion games”), and describe various ways of enriching studies of network games in the AGT community by practical considerations that are well-studied in the formal-method community. This includes, for example, network games with rich specifications, ones with real-time and ongoing behaviors, as well as algorithms for handling network games with huge state spaces.coffee
Tutorial 2 (Part 2)
Guy Avni: Formal Methods Meets Algorithmic Game Theory
Abstract:
Many problems in computer science, math, and economics can naturally be described as a game. As a result, various sub-fields in these disciplines study different types of games. The tutorial describes useful and interesting recent connections between formal methods and algorithmic game theory (AGT, for short). The goal in formal methods is to formally reason about systems. The traditional games that are studied in formal methods are called graph games and they model the interaction between a reactive system and its hostile environment. These are typically ongoing two-player zero-sum games of infinite duration. On the other hand, AGT lies in the intersection between computer science and economics. The games studied in AGT are typically multi-player, non-zero-sum, and one-shot games. We will focus on two meeting points between the two fields. The first is “bidding games”, which are graph games in which in each turn, an auction is held in order to determine which player moves next. We study the effect of using different bidding mechanisms on the properties of the game, and reveal an intriguing connection between bidding games and a fragment of stochastic games called “random-turn games”. In the the second meeting point, we will focus on “network games” (sometimes called “congestion games”), and describe various ways of enriching studies of network games in the AGT community by practical considerations that are well-studied in the formal-method community. This includes, for example, network games with rich specifications, ones with real-time and ongoing behaviors, as well as algorithms for handling network games with huge state spaces.Registration
Invited Talk 1
Dmitry Chistikov: On the complexity of logics over the integers
Abstract:
Given a system of linear Diophantine equations, how difficult is it to determine whether it has a solution? What changes if equations are replaced with inequalities? If some of the variables are quantified universally? These and similar questions relate to the computational complexity of deciding the truth value of statements in various logics. This includes in particular Presburger arithmetic, the first-order logic over the integers with addition and order.coffee
Session 1: LOGICS
Laureline Pinault. Undecidability of MSO with Path-Measure Quantifier via Probabilistic Automata
Abstract:
We consider monadic second-order logic extended with the qualitative path-measure quantifier that is interpreted over the infinite binary tree. This quantifier says that the set of infinite paths in the tree satisfying a formula has Lebesgue-measure one. We prove that this logic is undecidable. Towards this we first show that the emptiness problem of qualitative universal parity tree automata is undecidable, where qualitative means that a run of a tree automaton is accepting if the set of paths in the run that satisfies the acceptance condition has Lebesgue-measure equal to one. This result also implies the undecidability of the emptiness problem of a recently introduced model of alternating probabilistic tree automata.Szymon Toruńczyk. Aggregation, Enumeration, and Updates on Sparse Databases via Circuits
Abstract:
We propose an algebraic framework for studying efficient algorithms for query evaluation, aggregation, enumeration, and maintenance under updates, on sparse databases. Our framework allows to treat those problems in a unified way, by considering various semirings, depending on the considered problem. We propose two query languages extending first-order logic by forms of semiring aggregation. In the first language, a query is evaluated in a fixed semiring. For various considered semirings, we obtain efficient algorithms for the evaluation and maintenance of query outputs. By employing the provenance semiring, we obtain as an application a linear-time algorithm which inputs a first-order query and a sparse database, and computes a dynamic data structure which allows to enumerate the answers to the query with constant delay. The data structure can be updated in constant time, upon updates to the database that do not modify its Gaifman graph. Our second query language extends the first one by allowing aggregates from multiple semirings simultaneously. We show that such queries can be evaluated in linear time on sparse databases.Stanislav Kikot. On Monotone Determinacy of Recursive Queries over Disjunctive Views
Abstract:
I’m going to talk about new results on monotone determinacy ofSteffen van Bergerem. Learning Concepts Definable in First-Order Logic with Counting
Abstract:
We study classification problems over relational background structures for hypotheses that are defined using logics with counting. The aim of this paper is to find learning algorithms that run in time sublinear in the size of the background structure. We show that hypotheses defined by FOCN(P)-formulas over structures of polylogarithmic degree can be learned in sublinear time. Furthermore, we show that for structures of unbounded degree there is no sublinear learning algorithm for first-order formulas.Gabriel Istrate. Proof complexity of Kneser-Lovasz formulas and other combinatorial principles: the role of kernelization
Abstract:
The work presented here combines two different sets of results:Benjamin Lucien Kaminski. Quantitative Separation Logic – A Logic for Reasoning about Probabilistic Pointer Programs
Abstract:
We present quantitative separation logic (QSL). In contrast to classical separation logic, QSL employs quantities which evaluate to non-negative real numbers instead of predicates which evaluate to boolean values. The characteristic connectives of classical separation logic, separating conjunction (*) and separating implication (–*), are both lifted from predicates to quantities. This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, e.g. modus ponens, adjointness of * and –*, etc.Eugenia Ternovska. A Logic of Information Flows
Abstract:
A challenge in descriptive complexity is to identify logics with low complexity that simultaneously express both fundamental reachability properties and counting properties on unordered structures. We present 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. Two parameters may be used to control expressiveness and complexity: the set of definable connectives, and the expressiveness of atomic units.Arthur Milchior. MightyL: From Metric Interval Temporal Logic to Timed/Signal automata
Abstract:
Metric Interval Temporal Logic (MITL) was first proposed in thelunch break
Session 2a: POPULATION PROTOCOLS AND PROBABILISTIC SYSTEMS
Stefan Jaax. Succinct Population Protocols
Abstract:
Population models are a model of distributed computation by finite-state, anonymous and identical agents. Population protocols compute predicates in a population by reaching a lasting consensus through random pairwise interactions.Chana Weil-Kennedy. The Complexity of Verifying Observation Population Protocols.
Abstract:
Population protocols [Angluin et al., PODC, 2004] are a theoretical model of interactions between identical, limited-means, mobile devices. The model postulates a “soup” of indistinguishable finite-state agents that interact and change their states according to a joint transition function. Computations are infinite sequences of interactions satisfying a strong fairness constraint. Together, the agents of a population protocol compute information over their initial configuration, i.e. the number of agents in each state initially. In the general population protocol model, agents interact in pairs and this model was extensively studied [e.g. see survey in Bulletin of EATCS 2018]. Angluin et al. studied its expressiveness, and showed that any Presburger predicate can be calculated by such a protocol. Esparza et al. studied associated verification questions, such as the correctness problem: given a protocol and a predicate, does the protocol compute the predicate ? They showed that this problem is TOWER-hard.Antonin Kucera. Termination complexity of Parameterized Population Protocols
Abstract:
Population protocols form a model where identical finite-state agents interact to collectively decide whether their initial configuration, given by the initial number of agents in each state, satisfies a given property, e.g., . A protocol is correct if the agents correctly decide the property for all of the infinitely many initial configurations. This makes automatic formal analysis challenging. Furthermore, the literature often describes \emph{parameterized families} of protocols, e.g., a family of protocols for the predicates . We describe a methodology for the automatic analysis of asymptotic running time of such families, based on abstraction techniques, and report on an implementation on top of a constraint-solver. Our results show that it is possible to check properties of \emph{infinitely many} protocols in finite time.Catalin Dima. Model Checking Strategic Abilities in Information-sharing Agents
Abstract:
We study the formalism of visibly CGS (vCGS) which contains an explicit expression of private-data sharing in Multi-Agent System. In vCGS, each agent “a” has a syntactic/semantic endowment to temporarily allow som other agent “b” to see the value of some of a’s variables.Jan Kretinsky. Semi-Quantitative Abstraction and Analysis of Stochastic Population Models
Abstract:
Analysis of large continuous-time stochastic systems is a computationally intensive task. In this work, we focus on population models arising from chemical reaction networks (CRNs), which play a fundamental role in the analysis and design of biochemical systems. Many relevant CRNs are particularly challenging for existing techniques due to complex dynamics including stochasticity, stiffness or multimodal population distributions. We propose a novel approach allowing not only to predict, but also to explain both the transient and steady-state behaviour. It focuses on qualitative description of the behaviour and aims at quantitative precision only in orders of magnitude. Firstly, we abstract the CRN into a compact model preserving rough timing information, distinguishing only significantly different populations, but capturing relevant sequences of behaviour. Secondly, we approximately analyse the most probable temporal behaviours of the model through the most probable transitions. As demonstrated on complex CRNs from literature, our approach reproduces the known results, but in contrast to the state-of-the-art methods, it runs with virtually no computational cost and thus offers unprecedented scalability.Edoardo Pirovano. A Counter Abstraction Technique for the Verification of Probabilistic Swarm Systems
Abstract:
In my talk, I will be presenting joint work with Alessio Lomuscio, which hasJulia Eisentraut. Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Games
Abstract:
In this talk, I will present joint work with Jan Křetínský & Alexej Rotar on stopping criteria for value iteration and strategy iteration on concurrent stochastic games (CSG) played on graphs with reachability and safety objectives.Session 2b: PROGRAM VERIFICATION AND TREE AUTOMATA
Pierre Clairambault and Andrzej Murawski. On the expressivity of linear recursion schemes
Abstract:
We investigate the expressive power of higher-order recursion schemes (HORS)Peter Chini, Roland Meyer and Prakash Saivasan. Parameterized Complexity of Program Verification Tasks
Abstract:
Program verification is hard. Decision problems arising from verification tasks usually do not admit satisfying worst-case complexities. On the other hand, program verification can be efficient. Verification tools developed in recent years perform well even on large systems. To resolve this discrepancy between theory and practice, we picked up a recent trend in complexity theory: Parameterized Complexity. Unlike classical complexity theory that relates the complexity to the size of the instance, Parameterized Complexity measures the influence of several parameters on a problem’s complexity. This offers a more fine-grained view. We can separate those parameters of a problem that allow for the construction of efficient algorithms from those that cause the hardness.Mehran Hosseini, Joel Ouaknine and James Worrell. Termination of Affine Loops over the Integers
Abstract:
We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable,Paul Brunet. Pomsets with boxes: towards Atomic CKA.
Abstract:
Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a compositional framework to reason about concurrent programs. Their free model is given by series(-parallel) rational pomset languages, a standard true concurrency semantics. A key feature of CKA is provided by the weak exchange law, allowing one to partially interleave threads. For instance this enables one to consider that a specification that allows for three parallel threads can be refined in an implementation on two processors, provided all the dependencies required in the specification are satisfied.Patrick Landwehr. Tree Automata with Global Constraints for Infinite Trees
Abstract:
We study an extension of standard tree automata on infinite trees that allows for the use of global constraints.David Barozzini. Cost Logics, Safe Schemes, and Downward Closures
Abstract:
Higher order recursion schemes are a powerful formalism used to de- fine languages of possibly infinite ranked trees. They extend regular and context-free grammars, and are equivalent to simply typed λY-calculus and collapsible pushdown automata.Alexander Rabinovich and Doron Tiferet. Degrees of Ambiguity of Büchi Tree Automata
Abstract:
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is bounded ambiguous if there is k ∈ N, such that for every input it has at most k accepting computations. In this presentation we consider nondeterministic Büchi automata (NBA) over infinite trees, and prove that it is decidable in polynomial time whether an automaton is unambiguous, bounded ambiguous, finitely ambiguous, or countable ambiguous.coffee
Session 3: Transducers
Mikolaj Bojanczyk. Polyregular functions
Abstract:
I will describe a class of string-to-string functions, called the polyregular functions.Sougata Bose. Origin-equivalence and resynchronizers for two-way transducers
Abstract:
In the origin semantics the output symbols produced by a transducer are annotated with information about the input position responsible for producing those symbols. We show first that the origin semantics allows to recover decidability of equivalence and containment for non-deterministic two-way transducers — whereas these problems are known to be undecidable in the classical semantics. We consider a variant of the containment problem where two two-way transducers are compared under the origin semantics, but the origins can be modified by some given resynchronization relation. Resynchronizations for one-way transducers were proposed by Filiot et al. in 2016. We introduce MSO-resynchronizations, and show that they capture resynchronizations for one-way transducers. Containment of two-way transducers up to bounded MSO-resynchronizations turns out to be reducible to containment under origin semantics, so it is decidable. We also consider the problem of synthesizing a resynchronization which makes two classically equivalent transducers origin-equivalent. We show that this problem is undecidable in general, but decidable for functional transducers.Jan Martens. Resynchronizability of one-way transducers is undecidable
Abstract:
Origin semantics introduced by Bojańczyk are a fine grained semantics for transducers, that not only expresses the relation on input and output words, but also includes a function that given an output position returns the input position where it was produced: the origin. Two transducers that are equivalent with respect to the classical semantics may differ in the origin semantics, if they produce their output in different ways. Considering this finer origin semantics instead of the classical one allows to recover the decidability of equivalence, as well as machine-independent characterizations of regular transductions, among other properties. Resynchronizations as discussed in [1] express a similarity for different origin semantics that have the same underlying relation. This corresponds to a relaxation of the strict origin semantics, allowing a MSO-definable distortion. In [1], it is shown that containment up to a fixed resynchronization is decidable in PSPACE. We study the notion of containment up to some unknown resynchronization. We show that this relation forms a preorder, and that it is undecidable already in the case of one-way non-deterministic transducers. To do so we introduce the notion of desynchronized blocks, witnessing the absence of resynchronization.Anca Muscholl. Equivalence of finite-valued streaming string transducers is decidable
Abstract:
We show that the equivalence problem for finite-valued streaming string transducers is decidable, thus solving a question left open in an ICALP’11 paper by Alur and Deshmukh. We follow a proof idea due to Culik and Karhumäki, that uses Ehrenfeucht’s conjecture. Our proof is much more involved, because streaming string transducers produce their outputs piecewise, in contrast to one-way or two-way transducers, that produce their output linearly while reading the input. The solution is to come up with a suitable normalization procedure for SST, based on some (mild) word combinatorics and word equations.Janusz Schmude. Deciding Transducer Equivalence via Simulating an Algebra With a Ring of Polynomials
Abstract:
Register automata (RA) over a given algebra is an expressive class of transducers; it covers Streaming String Transducers (SST) in case of free monoid and Streaming Tree Transducers (STT) in case of ordered forest algebra. It is well known that equivalence is decidable for both SST and STT. In this talk we present a proof of decidability of equivalence of register automata over other algebras by simulating those algebras with a ring of polynomials (see Hilbert Method). We conclude with an undecidability result in case of ring of polynomials additionally equipped with substitution operation.Amina Doumane. First-order tree-to-tree functions
Abstract:
We define a class of functions, called first-order tree-to-tree functions,Adrien Boiret. Deciding equivalence on symbolic DTop with lookahead
Abstract:
Symbolic tree transducers are programs that transform data trees with an infinite signature.Ramanathan Thinniyam Srinivasan. Regular Separability and Intersection Emptiness are Independent Problems
Abstract:
The problem of regular separability asks, given two languages and , whether there exists a regular language with and . This problem has recently been studied for various classes of languages. All the results on regular separability obtained so far exhibited a noteworthy correspondence with the intersection emptiness problem: In each case, regular separability is decidable if and only if intersection emptiness is decidable. This raises the question whether under mild assumptions, regular separability can be reduced to intersection emptiness and vice-versa. We present counterexamples showing that none of the two problems can be reduced to the other. More specifically, we describe language classes , , , such that (i) intersection emptiness is decidable for and , but regular separability is undecidable for and and (ii) regular separability is decidable for and , but intersection emptiness is undecidable for and .Break
Session 4: PARITY GAMES AND GAMES WITH FINITE MEMORY
Mickael Randour. Games Where You Can Play Optimally With Finite Memory
Abstract:
Two-player games provide a natural framework for controller synthesis, with well-known connections with logic and automata. A seminal result in the study of two-player (turn-based) games on (finite) graphs is due to Gimbert and Zielonka [1], who established a complete characterization of preference relations (and consequently, winning objectives) for which players can play optimally with memoryless strategies, i.e., without looking at the past at all. Almost all simple objectives in the literature fall in this class and thus yield memoryless determined games. Still, the recent appearance of more complex objectives and, above all, the increasing resort to multi-objective games (often required to accurately account for trade-offs between several qualitative and quantitative aspects in real-world applications) has led to games where the players do need to use memory, which can be finite or even infinite in some cases (e.g., multi-mean-payoff games). In this talk, I will present ongoing research, where we tackle the question of finite-memory strategies in a flavor similar to Gimbert and Zielonka’s approach of memoryless strategies. We will see that obtaining a perfect equivalent of Gimbert and Zielonka’s results is out of the question, as counter-examples exist; and we will describe how we circumvent the related obstacles to achieve a general characterization of preference relations for which finite memory suffice to play optimally. My talk will focus on examples and key concepts to highlight the core challenges and fundamental differences with the memoryless case. This talk is based on joint work with Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj and Pierre Vandenhove.Karoliina Lehtinen. From Parity to Büchi with univesal trees.
Abstract:
Automata translations are instrumental to understanding the trade-offs between different automata types. Better translations can yield better algorithms for checking emptiness and containment, while lower bounds show differences in the power of different automata models. Translations of alternating parity word automata into automata with simpler acceptance conditions, such as Büchi or weak, are particularly interesting as such a translation implies a solution to parity games of which the complexity matches the blow-up in the state-space of the automaton.Paweł Parys. Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time
Abstract:
Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is the Zielonka’s recursive algorithm, which is very simple, exponential in the worst case, and the fastest in practice. We combine these two approaches: we propose a small modification of the Zielonka’s algorithm, which ensures that the running time is at most quasi-polynomial. In effect, we obtain a simple algorithm that solves parity games in quasi-polynomial time. We also hope that our algorithm, after further optimizations, can lead to an algorithm that shares the good performance of the Zielonka’s algorithm on typical inputs, while reducing the worst-case complexity on difficult inputs.Clément Tamines. Partial Solvers for Generalized Parity Games
Abstract:
Parity games have been broadly studied in recent years for their applications to controller synthesis and verification. In practice, it has been shown that partial solvers for parity games that execute in polynomial time, while incomplete, can solve most games in publicly available benchmark suites. We combine those partial solvers with the classical Zielonka algorithm to obtain an algorithm that is efficient in practice and complete. We also show how to extend partial solvers to generalized parity games which are games with conjunction of parity objectives or disjunction of parity objectives. We also show how to combine those partial solvers with a generalization of the Zielonka algorithm for generalized parity games. We have implemented those algorithms and evaluated them on a large set of benchmarks.Tom van Dijk. Distractions in Parity Games
Abstract:
Parity games are infinite games between two players on a finite directed colored graph where the winner of each infinite path is determined by the parity of the highest color. They are conceptually simple but expressive enough to capture the power of least and greatest fixed points, as evidenced by the tight linear relationship of parity games to the model checking problem of the modal mu-calculus. Inspired by one could say the rather silly approach (but in practice with surprising superior speed) of solving a parity game by naively evaluating the corresponding mu-calculus formula, we propose the concept of a distraction. Using this new concept, we now find a fundamental distinction between two classes of parity game algorithms, namely those based on two-player attractor computation, and those based on increasing value along progressive paths. Finally, we provide directions for future research aiming at bridging this fundamental distinction.Registration
Invited Spotlight Talks: Reachability in Petri Nets and Vector Addition Systems
Jerome Leroux. Reachability in Vector Addition Systems is Not Elementary
Abstract:
Vector addition systems, also known as Petri nets, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for vector addition systems is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS this year. We establish a non-elementary lower bound: the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi and other areas, that are known to admit reductions from the vector addition systems reachability problem, are also not elementary.Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension
Abstract:
The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The best known upper bound on this problem was not primitive-recursive, even when considering systems of fixed dimension.coffee
Session 5: VECTOR ADDITION SYSTEMS
Jan Otop. Long-Run Average Behavior of Vector Addition Systems with States
Abstract:
A vector addition system with states (VASS) consists of a finite set of states and counters.Wojciech Czerwiński. An Approach to Regular Separability in Vector Addition Systems
Abstract:
We study the problem of regular separability of languages of vector addition systems with states (VASS). It asks whether for two given VASS languages K and L, there exists a regular language R that includes K and is disjoint from L. While decidability of the problem in full generality remains an open question, there are several subclasses for which decidability has been shown.Michał Pilipczuk. Reachability for BoBrVASS
Abstract:
Bounded Vector Addition Systems with States (Bounded VASS) are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdziński proved that the reachability problem in this model is PSPACE-complete even in dimension 1.Radosław Piórkowski. Pumping in 2-VASS – geometry of runs
Abstract:
I will present a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. It is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem. I will show how one may apply it to reprove an exponential bound on the length of the shortest accepting run, and to prove a new pumping lemma for languages of 2-VASS.Dominik Velan. Deciding Fast Termination for Probabilistic VASS with Nondeterminism
Abstract:
A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires us the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism.lunch break
Session 6: MIXED TOPICS
Johannes Doleschal. Split-Correctness in Information Extraction
Abstract:
Programs for extracting structured information from text, namely information extractors, often operate separately on document segments obtained from a generic splitting operation such as sentences, paragraphs, k-grams, HTTP requests, and so on. Automated detection of this behavior of extractors, which we refer to as “split-correctness” would allow text analysis systems to devise query plans with parallel evaluation on segments for accelerating the processing of large documents. Other applications include the incremental evaluation on dynamic content, where re-evaluation of information extractors can be restricted to revised segments and debugging, where developers of information extractors are informed about potential boundary crossing of different semantic components.Petr Jancar. Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete
Abstract:
The proposed presentation is based on the joint paper with Sylvain Schmitz accepted to LiCS 2019, with the following abstract.Jędrzej Kołodziejski. Bisimulational Categoricity
Abstract:
I will present a result which says that for a complete modal theory t (i.e. a maximal consistent set of modal logic formulae), the following conditions are equivalent: (i) t has a unique model up to bisimulation; (ii) every model of t is bisimilar to a finitely branching one; (iii) t has a finitely branching model. I will further discuss examples (such as the EF-logic) and non-examples (e.g. the modal mu-calculus) of logics for which similar characterisation is possible.Wojtek Jamroga. Some Things are Easier for the Dumb and the Bright Ones (Beware of the Average!)
Abstract:
Model checking strategic abilities in multi-agent systems is hard, especially for agents with partial observability of the state of the system. In that case, it ranges from NP-complete to undecidable, depending on the precise syntax and the semantic variant. That, however, is the _worst case complexity_, and the problem might as well be easier when restricted to particular subclasses of inputs.Vadim Malvone. Reasoning about Natural Strategic Ability
Abstract:
In game theory, as well as in the semantics of game logics, a strategy can be represented by any function from states of the game to the agent’s actions. That makes sense from the mathematical point of view, but not necessarily in the context of human behavior. This is because humans are quite bad at executing complex plans, and also rather unlikely to come up with such plans in the first place. In this work, we adopt the view of bounded rationality, and look only at “simple” strategies in specifications of agents’ abilities. We formally define what “simple” means, and propose a variant of alternating-time temporal logic that takes only such strategies into account. We also study the model checking problem for the resulting semantics of ability.Bastien Maubert. Reasoning about Quality and Fuzziness of Strategic Behaviours
Abstract:
Temporal logics are extensively used for the specification of on-going behaviours of reactive systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviours in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalise concepts such as certainty or quality. We introduce and study SL[F] — a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0,1], reflecting “how much” or “how well” the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for our logic, based on a quantitative extension of Quantified CTL.Sławomir Lasota. Definable isomorphism problem
Abstract:
We investigate the isomorphism problem in the setting of definable sets (equivalent to sets with atoms): given two definable relational structures, are they related by a definable isomorphism?Oleg Verbitsky. Identifiability of Graphs with Small Color Classes by the Weisfeiler-Leman Algorithm
Abstract:
As shown by Immerman and Lander, every vertex-colored graphs with color multiplicitycoffee
Session 7a: BRACKETS, PETRI NETS, AND TIMED AUTOMATA
Dmitry Chistikov. Re-pairing brackets
Abstract:
Consider the following one-player game. Take a well-formed sequence of opening and closing brackets.Olivier Finkel. Wadge Degrees of -Languages of Petri Nets
Abstract:
We prove that -languages of (non-deterministic) Petri nets and -languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of -languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of -languages of (non-deterministic) Turing machines which also form the class of effective analytic sets. In particular, for each non-null recursive ordinal there exist some -complete and some -complete -languages of Petri nets,Michał Skrzypczak. On the strength of non-determinism for Buchi VASS
Abstract:
The motivating question is to understand the strength of non-determinism of Vector Addition Systems with States reading infinite words as the input. A special emphasis is put on the variants with limited number of dimensions (i.e. counters) and on unambiguous models. As it turns out, the non-determinism is inherent even for one-dimensional models. On the other hand, unambiguous models admit certain variant of determinisation construction.Piotr Hofman. Continuous Reachability for Unordered Data Petri Nets is in PTime
Abstract:
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In the talk, I will present the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. The main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.Patrick Totzke. Timed Basic Parallel Processes
Abstract:
Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time.Sayan Mukherjee. Fast Algorithms for Handling Diagonal Constraints in Timed Automata
Abstract:
A popular method for solving reachability in timed automata proceeds by enumerating reachable sets of valuations represented as “zones”. A naive enumeration of zones does not terminate. Various termination mechanisms have been studied over the years, for instance – checking a simulation relation between zones to stop enumeration from certain zones. In the presence of “diagonal constraints”, coming up with efficient simulations is significantly more challenging.Session 7b: MARKOV PROCESSES AND STOCHASTIC HYBRID SYSTEMS
David Purser. The big-O Problem for Labelled Markov Chains
Abstract:
Given two labelled Markov chains, consider the problem of whether one is big-O of the other. More concretely, the problem asks whether the probability of every finite word in the first chain is smaller than some constant multiple of the probability in the second. We show that the problem is, in general, undecidable. Even when it is known one is big-O of the other, the problem of finding or approximating the constant in the big-O is also undecidable. Our main result shows the big-O problem is coNP-complete for unlabelled Markov chains (i.e. when the alphabet consists of a single character).Jakob Piribauer. Long-run probabilities of path properties
Abstract:
We introduce the notion of long-run probabilities of paths properties in probabilistic systems. This quantitative measure indicates the degree to which a path property holds on the suffixes of a path. In verification, this measure could, e.g., be used to determine the expected proportion of time in which a system operates under normal conditions.Pierre Vandenhove. Reachability in Stochastic Hybrid Systems
Abstract:
Hybrid systems are dynamical systems combining continuous and discrete transitions. Continuous transitions represent the continuous evolution of various variables over time (e.g., according to a differential equation) and discrete transitions represent a change of mode of the system, where variables can be reset. Hybrid systems are widely used to model time-dependent reactive systems. In order to model uncertainty in a more subtle way, it can be valuable to make hybrid systems stochastic. We consider a class of stochastic hybrid systems (SHSs, for short) redefining hybrid systems by replacing non-determinism with randomness in both continuous and discrete transitions. We focus on reachability problems, which involve, e.g., deciding whether a specified set of states is reached almost surely (qualitative reachability), or approximating the probability of reaching a set (quantitative reachability). As reachability problems for hybrid systems are very prone to undecidability (already for rather restricted classes in the non-deterministic case), in order to obtain a decidable subclass, we need to balance restrictions to the discrete behavior and to the continuous behavior. Our approach is very restrictive toward the discrete transitions: we assume that the discrete transitions of our systems are strongly reset, i.e., that the value of the continuous variables cannot depend on their previous values before taking an edge, thereby decoupling the continuous behavior from the discrete behavior. A strong reset assumption has already been considered in [4, 3] for non-deterministic hybrid systems.Pranav Ashok. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Abstract:
Statistical model checking (SMC) is a technique for analysis of probabilistic systems that may be (partially) unknown. We present an SMC algorithm for (unbounded) reachability yielding probably approximately correct (PAC) guarantees on the results. We consider both the setting (i) with no knowledge of the transition function (with the only quantity required a bound on the minimum transition probability) and (ii) with knowledge of the topology of the underlying graph. On the one hand, it is the first algorithm for stochastic games. On the other hand, it is the first practical algorithm even for Markov decision processes. Compared to previous approaches where PAC guarantees require running times longer than the age of universe even for systems with a handful of states, our algorithm often yields reasonably precise results within minutes.Georg Zetzsche. Presburger arithmetic with stars, rational subsets of graph groups, and nested zero tests
Abstract:
We study the computational complexity of existential Presburger arithmetic with (possibly nested occurrences of) a Kleene-star operator. In addition to being a natural extension of Presburger arithmetic, our investigation is motivated by two other decision problems.Break
Session 8: AUTOMATA ON WORDS
Corto Mascle. On Nonnegative Integer Matrices and Short Killing Words
Abstract:
Unambiguous automata are a popular compromise between non-deterministic and deterministic automata in terms of succinctness and complexity. A word is called a killing word for an automaton if it is not a factor of any word recognized by this automaton. Here we will discuss the problem of computing a short killing word for an unambiguous automaton, as well as possible extensions. This problem has applications in the theory of codes as well as in some restrictions of the matrix mortality problem. This is a joint work with Stefan Kiefer, published at STACS 2019.Rafał Stefański. Single use register automata for data words
Abstract:
We introduce a new automaton model for data words, called single use register automata. These are like register automata for data words (introduced by Kaminski and Francez), with the restriction that every read access to a register destroys the register contents. We prove that the following models are equivalent: (a) one-way deterministic single use register automata; (b) two-way deterministic single use register automata; (c) languages recognised by orbit-finite semigroups.Nicolas Mazzocchi. Two-way automata with Presburger acceptance
Abstract:
This years, I will speak about two-way Parikh automata. This class of automata is an extension of two-way finite automata where transitions are labelled by a vector of integers and the acceptance condition consists to check if the component-wise addition of vectors along the run satisfies a given Presburger formula. I will investigate the emptiness problem, introducing conditions for decidability and tight complexity results depending on the acceptance constraint (existential, universal, with fix alternance Presburger formula). Please, see the attached long abstract for further information.Ismaël Jecker. On Equivalence Problem for Rational Relations
Abstract:
It is well-known that the containment and equivalence problems between rational relations is undecidable.Chris Köcher. Reachability Problems on Partially Lossy Queue Automata
Abstract:
We study the reachability problem for queue automata and lossy queue automata. Queue automata are known to be Turing-complete implying the undecidability of the reachability problem. In contrast to this result, reachability is decidable (but not primitive recursive) if the queue automata are allowed to forget any parts of their contents.Corentin Barloy. A robust class of linear recurrence sequences
Abstract:
This is joint work with Nathanaël Fijalkow, Nathan Lhote and Filip Mazowiecki.Informal Picnic
Invited Talk 2
Marie Fortin: Expressivity of first-order logic and star-free propositional dynamic logic over ordered structures
Abstract:
Star-free propositional dynamic logic is a variant of propositional dynamic logic (PDL) which is expressively equivalent to the 3-variable fragment of first-order logic. It is closely related to Tarski’s calculus of relations, and captures various temporal logics. In this talk, I will present sufficient conditions for star-free PDL and first-order logic to have the same expressive power over a class of linearly ordered structures with unary and binary relations; namely, that all binary relations are “interval-preserving”. This generalizes several results from the literature, in particular, the fact that linear orders as well as real-time signals have the 3-variable property. Another application is the synthesis of communicating finite-state machines from first-order specifications, using star-free PDL as an intermediate language.coffee
Session 9: REGULARITY
Dominik Wojtczak. Omega-Regular Objectives in Model-Free Reinforcement Learning
Abstract:
We provide the first correct solution for model-free reinforcement learning of ω-regular objectives for Markov decision processes (MDPs). We present a constructive reduction from the almost-sure satisfaction of ω-regular objectives to an almost-sure reachability problem, and extend this technique to learning how to control an unknown model so that the chance of satisfying the objective is maximized. We compile ω-regular properties into limit-deterministic Büchi automata instead of the traditional Rabin automata; this choice sidesteps difficulties that have marred previous proposals. Our approach allows us to apply model-free, off-the-shelf reinforcement learning algorithms to compute optimal strategies from the observations of the MDP. We present an experimental evaluation of our technique on benchmark learning problems.Simon Jantsch. From Linear Temporal Logic to Unambiguous Büchi Automata
Abstract:
This presentation considers a translation from Linear Temporal Logic (LTL) to unambiguous Büchi automata (UBA).Grzegorz Fabiański. Uniformization of MSO-definable relation on integers
Abstract:
We consider the problem to decide, whether a given MSO-definable relation R of the bi-infinite words (words over integers), there exist a MSO-definable function F (a functional relation between bi-infinite words) which uniformize it (meaning that if x R y then also x R f(x)).Vincent Michielini. Uniformization problem for class of regular languages: a algebraic approach
Abstract:
Given R a binary relation between finite words over an alphabet A andDenis Kuperberg. Computational content of cyclic proofs for regular expressions
Abstract:
We investigate the computational content of a cyclic proof system for Kleene algebra. If e,f are regular expressions such that L(e) is contained in L(f), the sequent e -> f can be proved in a formal proof system. Different proofs of the same sequent can beÉmile Hazard. An infinitary proof system for the inclusion of omega-regular languages
Abstract:
Proofs trees are usually supposed to be well-founded. However allowing infinite proof trees can be a fruitful generalization, in cases such as logics with fixed points. Moreover, regular non well-founded proofs (proofs having a finite number of subtrees) are still finite objects that can be processed by algorithms. Non well-founded proof systems for Kleene Algebra (and variants) were studied by Das and Pous in [1,2]. They introduced a non-well founded proof systems for Kleene Algebra, and show its soundness and regular completeness.Nathan Lhote. Computability and continuity of regular functions over ω-words
Abstract:
The class of regular functions from infinite words to infinite words is characterized by MSO-transducers, streaming ω-string transducers (transducers with registers) as well as deterministic two-way transducers with regular look-ahead. In their one-way restriction, the latter transducers define the class of rational functions.Christopher Hugenroth. Separating Languages over Infinite Words with Product Automata
Abstract:
We study the separation problem for regular languages over infinite words with respect to the Wagner hierarchy. The membership problem is known to be efficiently decidable in this setting. The decision procedure for membership analyses the loop structure of a given automaton. We show that it suffices to analyse the loop structure of the product automaton of two automata in order to decide separability of languages defined by deterministic automata.Break
Session 10: MEAN-PAYOFF GAMES, REACHABILITY GAMES, AND PATROLLING GAMES
Véronique Bruyère. Energy mean-payoff games
Abstract:
In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.Daniele Dell’Erba. Quasi Dominion Measures for Mean-Payoff Games
Abstract:
We propose a novel algorithm for the solution of mean-payoff games, which merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and can significantly speed up convergence to the solution. Experiments point outs that the resulting algorithm performs orders of magnitude better than the best solution algorithm currently known.Pierre Ohlmann. Universal Graphs for Mean Payoff Games
Abstract:
We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP∩coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by two other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to the study of mean payoff games.Aline Goeminne. On Relevant Equilibria in Reachability Games
Abstract:
We study multiplayer reachability games played on a finite directed graph equipped with target sets, one for each player. We are interested in both the qualitative setting where each player wants to reach his target set and the quantitative setting where each player wants to reach it as quickly as possible. In those qualitative/quantitative reachability games, it is known that there always exists a Nash equilibrium (NE) and a subgame perfect equilibrium (SPE). But sometimes several equilibria may coexist such that in one equilibrium no player reaches his target set whereas in another one several players reach it. It is thus very natural to identify “relevant” equilibria. We consider several notions of interesting equilibria including Pareto optimal equilibria and equilibria with high social welfare. Our contribution is twofold. First, we identify subclasses of qualitative/quantitative reachability games where an interesting equilibrium always exists. Secondly, we provide complexity results for various related decision problems.Marie Van Den Bogaard. The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
Abstract:
In this talk, we present the main ideas behind an algorithm to decide in polynomial space the constrained existence problem for Subgame Perfect Equilibria in quantitative reachability games.David Klaška, Antonín Kučera, Tomáš Lamser and Vojtěch Řehák. Automatic Synthesis of Efficient Regular Strategies in Adversarial Patrolling Games
Abstract:
We give a polynomial-time algorithm for synthesizing efficient regular strategies in adversarial patrolling games with general topology. Regular strategies use finite memory to gather some relevant information about the history of Defender’s moves which results in substantially better protection of the targets. So far, the scope of automatic strategy synthesis was limited to positional strategies (which ignore the history) or to regular strategies where the underlying finite-memory observer had to be supplied \emph{manually}. Furthermore, the existing methods do not give any information on how far are the constructed strategies from being optimal. In this paper, we try to overcome these limitations. We develop a novel \emph{gradient-based} algorithm for synthesizing regular strategies where the underlying finite-memory observers are constructed \emph{algorithmically}. The running time of our algorithm is \emph{polynomial} which makes the algorithm applicable to instances of \emph{realistic size}. Furthermore, we develop an algorithm for computing an \emph{upper bound} on the best achievable protection, and compare the quality of the constructed strategies against this bound. Thus, we can effectively measure the “distance” of the constructed strategies from optimal strategies, and our experiments show that this distance is often quite small.Closing Remarks