The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is rational: we design a finite automaton that can check whether the delay between two SSTs is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between (non-deterministic) SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two functional SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay.

This work was done in collaboration with Emmanuel Filiot, Christof Löding and Sarah Winter

In the recent years, JSON documents have become an important way of transferring information between computers. Notably, JSON documents contain two types of sequences that can be arbitrarily nested: an ordered collection of key-value pairs, and an unordered collection of values. To ensure that the communication can be done, i.e., that the receiver understands the message, a document should be structured in a specific way. This structure can be described by a JSON schema, which is itself a JSON document. With a schema, the receiver can verify that the document is valid, i.e., correct with regards to the schema. The state of the art consists in exploring the tree encoded in a JSON schema and verifying that there is a branch such that the JSON document satisfies all the constraints given on the branch.

In this joint work with Véronique Bruyère (University of Mons) and Guillermo A. Pérez (University of Antwerp), we propose an alternative approach to JSON document validation based on automata. The advantage of having a finite-state model to validate a document is that validating a JSON document in a streaming context becomes trivially efficient [1]. More precisely, we consider three types of automata: realtime one-counter automata (ROCAs), visibly one-counter automata (VCAs), and visibly pushdown automata (VPAs). Thanks to active learning algorithms [2, 3, 4], we can construct an automaton that behaves as a (simplified) validator. Our experiments show that VPAs are the most promising family of automata as they can be learned in a reasonable amount of time, and their stack enables them to easily verify whether the document is well-nested.

However, to make the learning process more efficient, we assume a fixed order for every sequence that appears in the JSON documents. Therefore, the automaton can only process documents following this order. This is problematic as, in a streaming context, some of the key-value pairs might appear in a different order. An easy fix would be to consider every possible permutation of key-value pairs but it would lead to an exponential blowup in the automaton's size. We thus want to explore alternative solutions to allow permutation of the pairs without this exponential blowup.

[1] Alfred V. Aho, Ravi Sethi, Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley series in computer science / World student series edition. Addison-Wesley, 1986.
[2] Véronique Bruyère, Guillermo A. Pérez, Gaëtan Staquet. Learning Realtime One-Counter Automata. To appear in TACAS' proceedings, 2022.
[3] Daniel Neider, Christof Löding. Learning Visibly One-Counter Automata in Polynomial Time. Technical Report AIB-2010-02, RWTH Aachen (January 2010), 2010.
[4] Malte Isberner. Foundations of Active Automata Learning: an Algorithmic Perspective. Technical University Dortmund, Germany, 2015.

The class of polyregular functions is a class of string-to-string transducers. Among several other possibilities, this class can be characterised as the least class of functions that contains certain prime functions and is closed under certain combinators. For example, one of the combinators is map: if a function f : τ -> σ is polyregular, then the same is true for the function f* : τ* -> σ* that applies f to each list element.

In this talk, I will discuss what happens if we want to add the fold combinator, as in functional programming languages. It turns out that with a more refined type system, inspired by linear logic, the fold combinator preserves polyregular functions.

Symbolic automata and transducers are objects of formal languages that can process inputs on an infinite signature through a finite number of rules guarded by a finite representation of subsets of the input signature. In the case of transducers, output is described using functions from the input signature to the output signature. In this paper, we propose a symbolic formalism for deterministic top-down tree transducers with a bottom-up lookahead. These transducers first read a tree from the bottom up, annotating the input tree, then read this annotated tree with a top-down transducer that produces and output. In our proposed symbolic formalism, both of those machine possess a finite number of states and a finite number of registers that can store data, but not test or perform computations on their content. This class is quite expressive and is stable under composition. We study the complexity of its equivalence problem via reduction to classical finite alphabet deterministic top-down transducers. We also present the subclass where the top-down part of the symbolic transducer carries no register, and show that the reduction of the equivalence problem to the classical case is much more efficient under that restriction.

In database theory, RPQs (regular path queries) are the building block of most query languages for querying graph databases. RPQs are generally evaluated under homomorphism semantics; in particular only the endpoints of the matched walks are returned.

On the contrary, due to user pressure, most real graph-database engines actually return the full matched walks. Under homomorphism semantics, there might be an infinite number of such walks. Hence each real query language had to adapt the semantics of RPQs in order to meet this popular demand, often neglecting theoretical implications. For instance, the most popular query language, Cypher, uses trail semantics: only walks with no repeated edges are returned. In that case, the result set is indeed finite, but the simplest computational problems are untractable.

We propose new semantics for RPQs, called simple-run semantics, as a candidate to reconcile theoretical considerations with practical aspirations. Just as trail semantics, simple-run semantics aims at keeping the output finite by filtering out redundant results. Trail semantics filter based on redundancy in the computed walk: repeated edges are forbidden. Simple-run semantics filter based on redundancy in the run: a node can be reused only if the query computation did progress compared to the previous times the node was visited.

Joint work with Claire David and Nadime Francis.

This paper initiates the study of data-path query languages (in particular, regular data path queries (RDPQ) and conjunctive RDPQ (CRDPQ)) in the classic setting of embedded finite model theory, wherein each graph is ``embedded'' into a background infinite structure (with a decidable FO theory or fragments thereof). Our goal is to address the current lack of support for typed attribute data (e.g. integer arithmetics) in existing data-path query languages, which are crucial in practice. We propose an extension of register automata by allowing powerful constraints over the theory and the database as guards, and having two types of registers: registers that can store values from the active domain, and read-only registers that can store arbitrary values.
We propose an extension of register automata by allowing powerful constraints over the theory and the database as guards, and having two types of registers: registers that can store values from the active domain, and read-only registers that can store arbitrary values. We prove NL data complexity for (C)RDPQ over the Presburger arithmetic, the real-closed field, the existential theory of automatic structures and word equations with regular constraints. All these results strictly extend the known NL data complexity of RDPQ with only equality comparisons, and provides an answer to a recent open problem posed by Libkin et al. Among others, we introduce one crucial proof technique for obtaining NL data complexity for data path queries over embedded graph databases called ``Restricted Register Collapse (RRC)'', inspired by the notion of Restricted Quantifier Collapse (RQC) in embedded finite model theory.

This paper was recently accepted at PODS'22 and is joint with Diego Figueira and Artur Jeż.

We solve finite ontology-mediated query entailment for ontologies expressed in ALC (a description logic, closely related to (multi)modal logic) and queries expressed as UCRPQs (extending UCQs - unions of conjunctive queries - with constraints on paths given by regular expressions).
In this setting the problem is not finitely controllable - the answer regarding only finite models might differ from the one for arbitrary (potentially infinite) models - and it deals with significantly more expressive query language than previous results in this area.
We combine a simple but interesting construction for deterministic finite automata with a number of techniques used previously in similar query entailment settings, getting a tight 2ExpTime upper bound.
This is joint work with Víctor Gutiérrez Basulto, Yazmin Ibáñez García, and Filip Murlak.

We introduce subsequence-queries with wildcards and gap-size constraints (swg-queries, for short) as a tool for querying event traces. Intuitively, swg-queries describe situations of interest (e.g. abnormal job execution) within a certain range in historic event data in form of a query string and different window size constraints. Hence an swg-query q is given by a string s over an alphabet of variables and types, a global window size w and a tuple c = ((c^-_1, c^+_1), (c^-_2, c^+_2), ..., (c^-_{|s|-1}, c^+_{|s|-1})) of local gap-size constraints.
The query q matches in a trace t$ (i.e., a sequence of types) if the variables can uniformly be substituted by types such that the resulting string occurs in t as a subsequence that spans an area of length at most w, and the ith gap of the subsequence (i.e., the distance between the ith and i-1th position of the subsequence) has length at least c^-_i and at most c^+_i.
We formalise and investigate the task of discovering an swg-query that describes best the traces from a given sample S of traces, and we present an algorithm solving this task. As a central component, our algorithm repeatedly solves the matching problem (i.e., deciding whether a given query matches in a given trace), which is an NP-complete problem (in combined complexity).
Hence, the matching problem is of special interest in the context of query discovery, and we therefore subject it to a detailed (parameterised) complexity analysis to identify tractable subclasses, which lead to tractable subclasses of the discovery problem as well. We complement this by a reduction proving that any query discovery algorithm also yields an algorithm for the matching problem. Hence, lower bounds on the complexity of the matching problem directly translate into according lower bounds of the query discovery problem.

We propose an algorithm for schema-based determinization of finite automata on words and of stepwise hedge automata on nested words. The idea is to integrate schema-based cleaning directly into automata determinization. We prove the correctness of our new algorithm and show that it is always more efficient than standard determinization followed by schema-based cleaning. Our implementation permits to obtain a small deterministic automaton for an example of an XPath query, where standard determinization yields a huge stepwise hedge automaton for which schema-based cleaning runs out of memory.

In this work, we analyse register systems over graph databases, over an infinite data domain. We define a model of non-deterministic, 2-way, concurrent register automata walking on the underlying graphs of graph databases. We then consider the following problem: Given a family of graph databases where the underlying graphs are described by an HR-equational system, and such a concurrent graph walking register automaton, is some graph database in the family accepted by the automaton? The general problem is undecidable even for multi-head DFA over non-data words. We show that a bounded version of the problem is decidable. We start by describing behaviours using graphs with data constraints. A graph is realisable if we can assign data-stamps to the nodes so that they satisfy the constraints of the behaviour. We show that this realisability property is MSO-definable whence the bounded problem can be reduced to the MSO-satisfiability problem over HR-equational graphs. This technique gives a uniform approach for the analysis of a wide class of register systems over graph databases with auxiliary data-structures like stacks and queues.
This is joint work with Mohan Dantam and S. Akshay.

We introduce a model for transforming strings, that provides fine control over what modifications are allowed. The model consists of actions, each of which is enabled only when the input string conforms to a predefined template. A template can break the input up into multiple fields, and constrain the contents of each of the fields to be from pre-defined regular languages. The template can also constrain two fields to be duplicates of each other. If the input string conforms to the template, the action can be performed to modify the string. The output consists of the contents of the fields, possibly in a different order, possibly with different numbers of occurrences. Optionally, the action can also apply transductions on the contents of the fields before outputting.

For example, the sentence "DLT will be held <cap:1>online</cap:1> if <cap:2>covid-19</cap:2> cases surge." conforms to the template x<cap:y>z</cap:y>w}. The output of the action can be defined as xf(z)w, where f is defined by a transducer. If f just capitalises its input, then we can perform this action twice to get the output "DLT will be held ONLINE if COVID-19 cases surge." Notice that, if we did not have the identifiers specified by y, then it will capitalise parts of the input text not intended to be capitalised.

We want to check that whenever the input comes from a given regular language, the output of any action also belongs to that language. We call this problem regular invariance checking. We show that this problem is decidable and is PSPACE-complete in general. For some restricted cases where there are no variable repetitions in the source and target templates (or patterns) and the regular language is given by a DFA, we show that this problem is co-NP-complete. We show that even in this restricted case, the problem is W[1]-hard with the length of the pattern as the parameter.

This work is in collaboration with C. Aiswarya and M. Praveen from Chennai Mathematical Institute and is accepted to be published in May at DLT 2022.

I will present joint work with Moses Ganardi, Anthony W. Lin, and Georg Zetzsche submitted to LICS 2022.
Automatic structures are infinite structures that are finitely represented by synchronized finite-state automata. This paper concerns specifically automatic structures over finite words and trees (ranked/unranked). We investigate the “directed version” of Ramsey quantifiers, which express the existence of an infinite directed clique. This subsumes the standard “undirected version” of Ramsey quantifiers. Interesting connections between Ramsey quantifiers and two problems in verification are firstly observed: (1) reachability with Büchi and generalized Büchi conditions in regular model checking can be seen as Ramsey quantification over transitive automatic graphs (i.e., whose edge relations are transitive), (2) checking monadic decomposability (a.k.a. recognizability) of automatic relations can be viewed as Ramsey quantification over co-transitive automatic graphs (i.e., the complements of whose edge relations are transitive). We provide a comprehensive complexity landscape of Ramsey quantifiers in these three cases (general, transitive, co-transitive), all between NL and EXP. In turn, this yields a wealth of new results with precise complexity, e.g., verification of subtree/flat prefix rewriting, as well as monadic decomposability over tree-automatic relations. We also obtain substantially simpler proofs, e.g., for NL complexity for monadic decomposability over word-automatic relations (given by DFAs).

We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regards to its set of objectives, given the behaviour of the system (which is committed in advance of any interaction). When the objectives are ω-regular, we prove that the Pareto-rational verification problem is co-NP-complete and fixed-parameter tractable (FPT) in the number of objectives of the environment. When the objectives are described by LTL formulas, the problem is PSPACE-complete, similarly to the classical LTL model-checking problem. In order to evaluate the applicability of our results in practice, we have implemented and evaluated two variations of our FPT algorithm on our running example and on randomly generated instances. This is a joint work with Véronique Bruyère and Jean-François Raskin.

We consider parameterized verification problems for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes.
Motivated by an asynchronous binary consensus algorithm introduced by Aspnes, we consider round-based distributed algorithms communicating with shared memory.
A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. Verification algorithms thus needs to manage both sources of infinity.
In this setting, we study several verification problems, among which safety (the error state cannot be reached) or inevitability (the error state cannot be avoided).
This a joint work with Nathalie Bertrand, Nicolas Markey and Ocan Sankur.

Reconfigurable broadcast networks (RBN) are a model of distributed computation in which agents can broadcast messages to other agents using some underlying communication topology which can change arbitrarily over the course of executions. We conduct parameterized analysis of RBN. We consider cubes, (infinite) sets of configurations in the form of lower and upper bounds on the number of agents in each state, and we show that we can evaluate boolean combinations over cubes and reachability sets of cubes in PSPACE. In particular, reachability from a cube to another cube is a PSPACE-complete problem. To prove the upper bound for this parameterized analysis, we prove some structural properties about the reachability sets and the symbolic graph abstraction of RBN, which might be of independent interest. We justify this claim by providing applications of these results. First, we show that the almost-sure coverability problem is PSPACE-complete for RBN, thereby closing a complexity gap from a previous paper. Second, we define a computation model using RBN, à la population protocols, called RBN protocols. We characterize precisely the set of predicates that can be computed by such protocols.

This is joint work with A. R. Balasubramanian and Lucie Guillou. It is the subject of an article accepted at FossaCS 2022, available here: https://arxiv.org/abs/2201.10432

Broadcast networks are a formalism of distributed computation that allows one to model networks of identical nodes communicating through message broadcasts over a communication topology that does not change over the course of executions. The coverability problem for such networks consists of deciding if there is a run of the network from some initial configuration in which some node reaches a given state. This problem is known to be undecidable (Delzanno, Sangnier, and Zavattaro, CONCUR 2010). In the same paper, the authors prove that, if the underlying communication topology has a bound on the longest path, then the coverability problem becomes decidable.

We provide complexity results for the above problem and prove that the coverability problem for bounded path topologies is $\mathbf{F}_{\epsilon_0}$-complete, where $\mathbf{F}_{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes. This solves an open problem of Hasse, Schmitz and Schnoebelen (LMCS, Vol 10, Issue 4). This work has been published at FSTTCS 2021.

We consider distributed synthesis problem where the task is to construct a controller for each process so that the controlled system does not have a deadlock. In our model processes synchronize by taking and releasing locks. A classical dinning philosophers problem is an example of a system of this kind.
A strategy for each process has access only to local information, it should decide on a next action of a process knowing solely the previous actions of the process.
The problem is undecidable even when every process can use at most four locks. However, when each process can use at most two locks the problem is solvable in the second level of the polynomial hierarchy, and even in PTIME under some additional assumptions. Dining philosophers problem uses two locks per process. We also prove that the problem is decidable when the number of locks per process is not bounded but locks must be used in a nested manner.

This is joint work with Hugo Gimbert, Anca Muscholl and Igor Walukiewicz.

Trust is a very critical and yet one of the least understood processes in the computing paradigm. As opposed to typical case studies based on toy examples, we demonstrate how we leverage formal verification to understand the complicated notion of trust, with a specific focus on remote attestation in confidential computing. In this talk, we present the challenges and lessons learnt in the formal specification and verification of Intel's next generation architecture named Intel Trust Domain Extensions, and demonstrate how we ended up making Intel update the specification.

We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre allows reasoning about the value of a quantity after a program terminates on a given initial state, quantitative strongest post allows reasoning about the value that a quantity had before the program was executed and reached a given final state. We show how strongest post enables reasoning about the flow of quantitative information through programs. Similarly to weakest liberal preconditions, we also present a quantitative strongest liberal post. As a byproduct, we obtain the entirely unexplored notion of strongest liberal postconditions and show how these foreshadow a potential new program logic — partial incorrectness logic — which would be a more liberal version of O’Hearn’s recent incorrectness logic.

This is joint work with Linpeng Zhang. It is to appear at OOPSLA 2022. A preprint is available here: https://arxiv.org/pdf/2202.06765.pdf

The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies, based on social, political, and technological instruments. It seemed clear at the first glance what all those measures have been trying to achieve, and what the criteria of success are. But is it really that clear?

Quoting various media sources, with COVID we had to fight an unprecedented threat to *health* and *economic stability*. While fighting it, we should protect *privacy*, *equality* and *fairness*, as well as do a coordinated assessment of *usefulness*, *effectiveness*, *technological readiness*, *cyber-security risks*, and threats to *fundamental freedoms* and *human rights*. Taken together, this is hardly a straightforward set of goals and requirements.

We postulate that modal logics for multi-agent systems provide a common platform to study (and balance) essential properties of pandemic mitigation strategies. We also show how one can obtain a list of such properties by ``distilling'' them from media snippets. Finally, we present a preliminary take on their formal specification.

(Joint work with David Mestel, Peter B. Roenne, Peter Y.A. Ryan, and Marjan Skrobot)

The Skolem Problem is the question of determining whether a given linear recurrence sequence (such as the Fibonacci numbers) contains a zero or not. Its decidability has been open for almost a century. The last major breakthroughs, dating back from the early 1980s and employing advanced machinery from analytic number theory and Diophantine approximation, concern linear recurrence sequences of small order (4 or less). Very recently, new techniques (some relying on certain central conjectures in number theory) have enabled substantial further advances on the Skolem Problem. We present a survey of recent developments in the field.

This talk is based on joint work with Yuri Bilu, Richard Lipton, Florian Luca, Joël Ouaknine, David Purser, and James Worrell.

Given an integer linear recurrence sequence ⟨X_0, X_1, X_2,...⟩, the Skolem Problem asks to determine whether there is a natural number n such that X_n = 0. The decidability of the Skolem Problem is a long-standing open problem in verification. In a recent preprint, Lipton, Luca, Nieuwveld, Ouaknine, Purser, and Worrell prove that the Skolem Problem is decidable for a class of reversible sequences of order at most seven. Herein, we give an alternative proof of the result. The novelty of our approach arises from our employment of theorems concerning the polynomial relations between Galois conjugates. In particular, we make repeated use of a result due to Dubickas and Smyth for algebraic integers that lie alongside all their Galois conjugates on two (but not one) concentric circles centred at the origin.

We are interested in orbit-finite systems of linear equations. Intuitively, a system of linear equations is orbit-finite if there are finitely many variables and equations up to certain symmetries, even if the set of variables and equations are infinite. Formally, we can represent an orbit-finite system of linear equations as a finitely-supported matrix M, with rows and columns, indexed respectively by orbit finite sets B and C, and a finitely supported vector t indexed by B. A solution of such a system is a vector x indexed by C, such that M.x = t.

We have proven the decidability of the existence of finitely supported solutions and finite solutions. Currently, we are trying to extend our results to solve orbit-finite linear programming and orbit-finite integer linear programming, and to give a method to compute the set of solutions.

This is a work in progress, jointly with Piotr Hofman and Sławomir Lasota.

Joint work with Joel Ouaknine, James Worrell, Rupak Majumdar, Sadegh Soudjani, Julian D'Costa and Mahmoud Salamati.

A linear dynamical system is given by an update matrix M and a starting point s. The reachability problem for LDS asks, given a semialgebraic target S, whether the orbit ever hits S. This problem is open and at least as hard as the Skolem and the Positivity problems for linear recurrence sequences.

We consider reachability questions for pseudo-orbits, which is a fundamental notion in theory of dynamical systems going back to works of Anosov, Bowen and Conley. An epsilon-pseudo orbit of s under M is a sequence such that x_0=s and x_{n+1}=Mx_n + d_n for a perturbation d_n of size at most epsilon. The pseudo-reachability problem then is to determine if for every epsilon>0, there exists an epsilon-pseudo-orbit that hits S. This can be viewed as a robust version of the reachability problem.

In our work presented at MFCS21, we showed that the pseudo-Skolem problem (pseudo-reachability problem where the target S is a hyperplane) is decidable using established methods. In our ongoing work, relying on o-minimality of R_exp, we have shown that for diagonalisable systems, the pseudo-reachability problem is decidable for arbitrary semialgebraic targets. Moreover, our methods can readily be applied in the continuous setting and to certain other formulations of the robust reachability problem.

Well quasi-orderings (wqos) are used in program termination (see eg. Dershowitz and Manna 1979, or Blass and Gurevich 2008) and automated program verification (eg of well-structured systems, see Finkel and Schnoebelen 2001). There is notion of measure on wqos called the ordinal invariants - the height, width, and maximal order type (de Jongh and Parikh 2019) - which provides bounds on complexity of wqo-based programs.
Complex wqos are often built from simpler wqos through classical constructions such as disjoint sum, lexicographic sum, cartesian product, and high-order constructions like powerset or sequences. One main challenge is to compute the ordinal invariants of such wqos compositionally (see Džamonja, Schmitz, and Schnoebelen 2020).
We develop a game-theoretical approach to compute lower bounds on the width of wqos and apply it to compute the width of the cartesian product of finitely many linear orderings. We then leverage this result to compute the width of an elementary family of wqos.

Preprint available at arxiv.org/abs/2202.07487

Bibliography:
N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979.
A. Blass and Y. Gurevich. Program termination and well partial orderings. ACM Trans. Computational Logic, 9(3):1–26, 2008.
A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere. Theoretical Computer Science, 2001.
D. H. J. de Jongh and R. Parikh. Well-partial orderings and hierarchies. Indag. Math., 39(3):195–207, 1977.
Mirna Džamonja, Sylvain Schmitz, and Philippe Schnoebelen. On ordinal invariants in well quasi orders and finite antichain orders. In P. Schuster, M. Seisenberger, and
A. Weiermann, editors, Well Quasi-Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends in Logic, chapter 2, pages 29–54. Springer, 2020.

The set of indices that correspond to the positivie entries of a sequence of numbers is called its positivity set. In this talk, we present a couple of results regarding the density of the positivity set of a given linear recurrence sequence. We show that one can compute this density to arbitrary precision, and decide whether it is equal to 1.

We investigate the Membership Problem for hypergeometric sequences: given a hypergeometric sequence $\langle u_n \rangle_{n=0}^\infty$ of rational numbers and a target $t \in \mathbb{Q}$, decide whether $t$ occurs in the sequence. We show decidability of this problem under the assumption that in the defining recurrence $p(n)u_{n+1}=q(n)u_n$, the roots of the polynomials $p(x)$ and $q(x)$ are all rational numbers. Our proof relies on bounds on the density of primes in arithmetic progressions. We also observe a relationship between the decidability of the Membership problem (and variants) and the Rohrlich-Lang conjecture in transcendence theory.

This work is in collaboration with Amaury Pouly, Mahsa Shirmohammadi and James Worrell. The full paper is available online: https://arxiv.org/abs/2202.07416

We study the Radical Identity Testing problem (RIT): Given an algebraic circuit representing a multivariate polynomial $f(x_1, \dots, x_k)$ and nonnegative integers $a_1, \dots, a_k$ and $d_1, \dots,$ $d_k$, written in binary, test whether the polynomial vanishes at the \emph{real radicals} $\sqrt[d_1]{a_1}, \dots,\sqrt[d_k]{a_k}$, i.e., test whether $f(\sqrt[d_1]{a_1}, \dots, \sqrt[d_k]{a_k}) = 0$. We place the problem in {\coNP} assuming the Generalised Riemann Hypothesis (GRH), improving on the straightforward {\PSPACE} upper bound obtained by reduction to the existential theory of reals. Next we consider a restricted version, called $2$-RIT, where the radicals are square roots of prime numbers, written in binary. It was known since the work of Chen and Kao~\cite{chen-kao} that $2$-RIT is at least as hard as the polynomial identity testing problem, however no better upper bound than {\PSPACE} was known prior to our work. We show that $2$-RIT is in {\coRP} assuming GRH and in {\coNP} unconditionally.
Our proof relies on theorems from algebraic and analytic number theory, such as the Chebotarev density theorem and quadratic reciprocity.

This is a joint work with Klara Nosan, Mahsa Shirmohammadi and James Worrell and is currently under submission. A full version can be found here - https://arxiv.org/abs/2202.07961

In this work, we look at good-for-games Rabin automata that recognise a given Muller language (a language that is entirely characterised by the set of letters that appear infinitely often in each word). We establish that minimal such automata are exactly of the same size as the minimal memory required for winning Muller games with this condition. We show how to effectively construct such minimal automata. Finally, we establish that these automata can be exponentially more succinct than equivalent deterministic ones, thus proving as a consequence that chromatic memory for winning a Muller game can be exponentially larger than unconstrained memory.
This is joint work with Thomas Colcombet and Karoliina Lehtinen.

I will present recent work on how to characterize half-positionality over arbitrary arenas by means of universal graphs. More precisely, we will see that an objective is positional if and only if it has a well-ordered universal monotonic graph, for each cardinal. I will also describe a few examples, and state some open problems.

Zero-sum games on graphs are a natural framework used as a model in multiple areas of theoretical computer science, such as the field of reactive synthesis. A central class of specifications for these games is the one of omega-regular languages, which encompasses, e.g., linear-time temporal logic specifications. Part of its interest is due to the landmark result that finite-state machines are sufficient to implement optimal strategies in omega-regular games. Surprisingly, the question of characterizing the precise size of the finite-state machines needed for optimal strategies in omega-regular games is not yet settled. Understanding when small strategies suffice has theoretical and practical significance. We set out to provide a novel piece in this puzzle by characterizing the languages recognizable by deterministic Büchi automata (DBA) that are half-positional, i.e., for which the protagonist needs no memory to play optimally. Our characterization consists of three conditions, two of which pertaining to more general objectives and one of which being specifically suited to handle DBA. Our characterization may also help study the decidability of the half-positionality of languages recognized by DBA.
This talk is based on ongoing joint work with Patricia Bouyer, Antonio Casares, and Mickael Randour.

Security is a subject of increasing attention in our actual society in order to
protect critical resources from information disclosure, theft or damage. The informal model of attack trees introduced by Schneier [2], and widespread in the industry, is advocated in the 2008 NATO report to govern the evaluation of the threat in risk analysis. Attack-defense trees have since been the subject of many theoretical works addressing different formal approaches (see [3] for an exhaustive list).

In [1], the authors introduced a path semantics over a transition system for attack trees. The presentation will be established over an ongoing work framed by Sophie Pinchinat from IRISA and Thomas Brihaye from UMONS in which we generalise the works of [1] by allowing a multi-agent interpretation of the attack-tree formalism. To do it, we replace transition systems by concurrent game arenas and our associated semantics consist of strategies. We then show that our proposed semantics can be recognised by tree automata and we finish by determining bounds to the complexity
of the emptiness problem. This problem answers the following question : is there a winning strategy for the the player/coalition trying to achieve the objective described by the attack tree ?

References :

[1] Maxime Audinot, Sophie Pinchinat, and Barbara Kordy, Is my attack tree correct?, European Symposium on Research in Computer Security, Springer, 2017,
pp. 83–102.
[2] Bruce Schneier, Attack trees, Dr. Dobbs journal 24 (1999), no. 12, 21–29.
[3] Wojciech Wide l, Maxime Audinot, Barbara Fila, and Sophie Pinchinat, Beyond
2014: Formal methods for attack tree–based security modeling, ACM Computing
Surveys (CSUR) 52 (2019), no. 4, 1–36.

In this talk, we present the main ideas behind solving the constrained existence problem for Subgame Perfect Equilibria in multiplayer parity games.
We present new complexity results that close gaps in the literature. Our techniques are based on a recent characterization of SPEs in prefix-independent games that is grounded on the notions of requirements and negotiation, and according to which the plays supported by SPEs are exactly the plays consistent with the requirement that is the least fixed point of the negotiation function. The new results are as follows. First, checking that a given requirement is a fixed point of the negotiation function is an NP-complete problem. Second, we show that the SPE constrained existence problem is NP-complete, this problem was previously known to be ExpTime-easy and NP-hard.
This talk is based on results obtained in a joint work with Léonard Brice and Jean-François Raskin (Universit\'e libre de Bruxelles), presented at CSL this year.

We introduce countdown mu-calculus, an extension of the modal fixpoint calculus with operators denoting ordinal approximations of fixpoints. The logic is capable of capturing (un)boundedness-related phenomena, yet possesses many of the nice properties of the standard mu-calculus. In particular, an extension of parity games - called countdown games - lifts the classical logic~games~automata correspondence beyond regular properties: automata and (vectorial) countdown logic define the same languages, whereas the (provably weaker) scalar fragment of the logic has a simple syntactic characterization on the automata side.
This is a joint work with Mikołaj Bojańczyk and Bartek Klin.

In a two-player zero-sum graph game, the players move a token throughout the graph to produce a finite or infinite path, which determines the winner of the game. Bidding games are graph games in which the players have budgets, and in each turn, an auction determines which player moves the token. One characterisation of bidding games refers to the allowed bids: in continuous bidding, bids can be arbitrarily small, whereas in discrete bidding, the granularity of the bids is restricted. Discrete bidding is thus more appropriate for most practical applications.

We focus on qualitative objectives. Both continuous- and discrete-bidding games are known to be determined, which in bidding games is captured by the concept of a threshold budget: roughly, a budget that is necessary and sufficient for a player to win the game from a given vertex.

We study the complexity of computing the threshold budgets in discrete-bidding games.
For reachability objectives, threshold budgets in continuous-bidding games satisfy an average property: the budget at a vertex is the average of two of its neighbours.
Moreover, there is a unique function with the average property. Uniqueness immediately implies that the complexity of finding threshold budgets is in NP and coNP.

Under discrete-bidding, threshold budgets are known to satisfy a discrete version of the average property. We show, somewhat surprisingly, that there can be more than one function satisfying the average property. This complicates the search for threshold budgets. We study, for the first, time, discrete-bidding games in which the sum of budgets is given in binary and show that finding threshold budgets is in NP and NP. Our algorithm uses a careful reduction to turn-based reachability games that is based on an intricate analysis of the optimal strategies of the players.

We turn to parity and B{\"u}chi objectives. Under continuous bidding, parity bidding games reduce easily to reachability games. Under discrete-bidding, however, it was known that a key property of the reduction fails.

We develop a fixed-point algorithm that takes a very different approach from the one in continuous-bidding games. The algorithm reveals the structure of threshold budgets in discrete-bidding games.
We are currently working on employing this structure in order to show membership in NP and coNP.
In the future, we expect that our techniques will be useful in studying other variants of discrete bidding games, e.g. mean-payoff games, which exhibit interesting properties under continuous bidding but have never been studied under discrete bidding.

Joint work with Guy Avni.

Players in a game take their decisions with respect to their knowledge of what the other players do, or have done or even in some cases, will do. The study of temporal dependencies requires specific formalism through Delay games: two players play a classical Gale-Stewart game but the moves of one player are delayed.

In this presentation, we propose a formalism generalizing Delay games, Dependency Matrices, for a multi-player setting. We solve the problem of the existense of a winning uniform strategy when all delays are finite and show that this problem is undecidable when delays may be infinite. We then propose a fragment to recover decidability that we call perfectible information. We solve the problem on this fragment by unifying Büchi automaton complemention and parity-game resolution.

We present a characterization of subgame-perfect equilibria in prefix-independent infinite-duration multi-player games played on graphs, and use it to propose a new algorithm solving the SPE threshold problem in mean-payoff games. That problem was recently proved to be decidable and 2ExpTime-complete: we show that it is NP-complete.

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata.
Here, we study the extension of the classical framework onto infinite inputs, as well as their history-deterministic variant and the problem of solving games with winning conditions expressed by Parikh automata.

We define reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and show that safety and co-Büchi ones have an undecidable emptiness problem. On the other hand, Parikh automata with reachability or Büchi acceptance have a decidable emptiness problem, implying, in particular that in this setting Büchi acceptance does not subsume safety, at least not effectively.

History-deterministic automata allow a limited form of nondeterminism and are often well-suited for applications which classically call for deterministic automata, e.g., solving games and composition.
We show that history-deterministic Parikh automata are more expressive than deterministic ones, but less expressive than nondeterministic ones.
However, they are not well-suited for games, as we prove that solving games is undecidable even for winning conditions given by deterministic Parikh automata on finite words.
Furthermore, we determine the closure properties of history-deterministic Parikh automata and show that universality and regularity are undecidable for such automata.

We present an algorithm for generating geodesic regular tree structures for periodic hyperbolic and Euclidean tessellations. The core of our algorithm is conceptually similar to Angluin's algorithm of learning regular languages. Our experimental results show that our algorithm runs fast in practice.

We explain the links between automata theory and hyperbolic geometry. We define the periodic tessellations we are working with. We explain how to use tree structures to generate a periodic tessellation. We discuss the limitations of earlier methods. We describe our algorithm, its applications, and experimental results.

This is joint work with Eryk Kopczyński.

We define novel algorithms for the inclusion problem between two ω-visibly pushdown languages, an EXPTime-complete problem. Intuitively our algorithms search for counterexamples to inclusion in the form of ultimately periodic words, that are words of the form uv^ω where u and v are finite words. The search is pruned using antichain-like techniques: a quasiorder tells us which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. Our algorithm uniquely combines antichain-like techniques with the use of distinct quasiorders for prefix and period of ultimately periodic words. The use of distinct quasiorders for prefix and period enables further pruning compared to a unique quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages.
This is a joint work with Pierre Ganty and Luka Hadzi-Djokic.

We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an adaptive manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness.
To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most k leaves and we provide an n^{O(k^2)} time algorithm for this problem. This is joint work with A. R. Balasubramanian published at CONCUR 2021

Regular nested word languages (a.k.a. visibly pushdown languages) strictly extend regular word languages, while preserving their main closure and decidability properties. Previous works have shown that considering words with two matchings (or, equivalently, $2$-visibly pushdown languages) is not as successful. In this work, inspired by homomorphic representations of indexed languages, we identify a subclass of $2$-nested words, which we call $2$-wave words. This class strictly extends the power of nested words, while preserving its main properties. More precisely, we prove closure under determinization of the corresponding automaton model, and as a consequence derive a logical characterization, as well as closure and decidability properties. We also show that the word projection of the languages we define belong to the class of linear indexed languages.
Joint work with Séverine Fratani and Pierre Alain Reynier.

In this talk we will focus on automata having multiple stacks as their memory. Concretely, our automata consist of multiple local finite automata each having one stack. We additionally allow partial synchronizations between these stacks. This means, whenever we read or write a letter we do this operation on a specified subset of these stacks at the same time. Note that our model also covers automata having one or more stacks without synchronization.

It is well-known that automata having at least two stacks are as powerful as Turing-machines implying the undecidability of all non-trivial verification problems of such systems. To circumvent these undecidabilities we consider a special restriction to these automata. So, when applying a transition of our special automata, we read a letter a, execute local transitions simultaneously on each local automaton able to handle the letter a, and we write other letters at most into the stacks associated to the letter a.

We can show then that the set of backwards reachable configurations of a recognizable set of configurations of such special multi-pushdown automaton is effectively recognizable again. In contrast we can find a recognizable set of configurations such that the forwards reachable configurations are not recognizable anymore. Anyways, we learn that the reachability problem and even recurrent reachability problem are decidable in polynomial time. We also obtain that the model checking problem of Thiagarajan's LTL for traces is decidable in our multi-pushdown automata.

Note that this talk is based on a joint work with Dietrich Kuske.

A finite and deterministic complete automaton is \emph{synchronizing} if there exists a reset state and an input word that drives the automaton to the reset state when started from any state. The notion of synchronizability has been extended to various other models: non-deterministic and partial automata, weighted and timed automata, register automata, nested word automata, Markov decision processes, probabilistic automata and push-down automata. Parikh automata were introduced by Klaedtke & Rueß and enrich finite automata with counters that are checked against a semilinear condition at the end. Here, we will present various notions of synchronization for Parikh automata that yield decidable problems that are PSPACE-complete in general. We will also consider subclasses for which the problem is NP-complete or polynomial time computable.
This is ongoing (yet unpublished) work.

One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests.
Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems.

The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN admits an equivalent DOCN, has not received attention.

We introduce four notions of OCN determinizability, which arise naturally due to intricacies in the model, and specifically, the interpretation of the initial counter value.
We show that in general, determinizability is undecidable under most notions, but over a singleton alphabet (i.e., 1 dimensional VASS) one definition becomes decidable, and the rest become trivial, in that there is always an equivalent DOCN.

Probabilistic pushdown automata (recursive state machines) are a widely known model of probabilistic computation associated with many decidable problems about termination (time) and linear-time model checking. Higher-order recursion schemes (HORS) are a prominent formalism for the analysis of higher-order computation.
Recent studies showed that, for the probabilistic variant of HORS, even the basic problem of determining whether a scheme terminates almost surely is undecidable. Moreover, the undecidability already holds for order-2 schemes (order-1 schemes are known to correspond to pushdown automata).
Motivated by these results, we study restricted probabilistic tree-stack automata (rPTSA), which in the nondeterministic setting are known to characterise a proper extension of context-free languages, namely, the multiple context-free languages.
We show that several verification problems, such as almost-sure termination, positive almost-sure termination and omega-regular model checking are decidable for this class.
At the level of higher-order recursion schemes, this corresponds to being able to verify a probabilistic version of the so-called affine-additive higher-order recursion schemes (PAHORS). PAHORS extend order-1 recursion schemes and are incomparable with order-2 schemes.

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata.
Here, we study the extension of the classical framework onto infinite inputs, as well as their history-deterministic variant and the problem of solving games with winning conditions expressed by Parikh automata.
We define reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and show that safety and co-Büchi ones have an undecidable emptiness problem. On the other hand, Parikh automata with reachability or Büchi acceptance have a decidable emptiness problem, implying, in particular that in this setting Büchi acceptance does not subsume safety, at least not effectively. History-deterministic automata allow a limited form of nondeterminism and are often well-suited for applications which classically call for deterministic automata, e.g., solving games and composition.
We show that history-deterministic Parikh automata are more expressive than deterministic ones, but less expressive than nondeterministic ones. However, they are not well-suited for games, as we prove that solving games is undecidable even for winning conditions given by deterministic Parikh automata on finite words. Furthermore, we determine the closure properties of history-deterministic Parikh automata and show that universality and regularity are undecidable for such automata.

String constraints impose constraints over variables that take strings as assignments. Given a string constraint C, the satisfiability problem asks if there is an assignment which satisfies every constraint in C. Most classes of string constraints in their full generality although have high expressive power turn out to be undecidable. Hence, a natural direction to recover decidability is to consider meaningful subclasses of string constraints. In this talk, we consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. We call this variant subword-ordering string constraints. The satisfiability problem for the variant turns out to be undecidable (even with regular membership). We consider a fragment in which the subword order constraints do not impose any cyclic dependency between variables. We show that this fragment is NEXPTIME-complete. As an important application of our result, we establish strong connection between the acyclic fragment of the subword-ordering string constraints and acyclic lossy channel systems, an important distributed system model. This allowed us to settle the complexity of control state reachability in acyclic lossy channel pushdown systems. The problem was shown to be decidable by Atig et al. in 2008. However, no elementary upper bound was known. We show that this problem is NEXPTIME-complete. This is a joint work with C. Aiswarya and Prakash Saivasan.

This is joint work with Nir Piterman and Gerardo Schneider.

The reactive synthesis problem is framed as the problem of finding a program that reacts appropriately to an environment to achieve certain goals, or proving such a program does not exist. Ordinarily both the goals and the adversarial environment are specified in LTL. This can hamper real world applicability, given often an environment does not come a priori with an LTL specification.

In this presentation we describe ongoing work to apply reactive synthesis when at least part of the environment is known operationally. We call this operational part a monitor. We assume a non-operational part that acts first, after which the monitor reacts, and then the controller can react to both (for convenience we allow the monitor to re-adjust internally to the controller before the next time-step).

If the monitor is a finite-state automaton then with appropriate variables to encode its states we can represent the monitor in LTL, and add it as an environment assumption for standard reactive synthesis. An interesting problem is when the monitor is richer and is more like a general program: with internal variables, and transitions that can guard on these variables and transform them. Such a language can be non omega-regular --- it can encode pushdown properties or unbounded infinite-state systems.


We take inspiration from the work of lazy abstraction for model checking and apply it here in an attempt to determine realisability by exposing just enough information about the internal state of the monitor with possibly successive refinement steps.

Given a specification F(X,Y) over inputs X and output Y, defined over a background theory T, the problem of program synthesis is to design a program P such that Y = P(X) satisfies the specification F. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach for program synthesis where in addition to the specification F, the end-user also specifies a grammar L to aid the underlying synthesis engine. This paper investigates the feasibility of synthesis techniques without grammar, a sub-class defined as T-constrained synthesis.

We show that T-constrained synthesis can be reduced to DQF(T), i.e., to the problem of finding a witness of a Dependency Quantified Formula Modulo Theory. When the underlying theory is the theory of bitvectors, the corresponding DQF(BV) problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific synthesis techniques. Our empirical analysis shows that T-constrained synthesis can achieve significantly better performance than syntax-guided approaches.

This is a joint work with Subhajit Roy and Kuldeep S. Meel. The corresponding paper was published at International Joint Conference on Artificial Intelligence, IJCAI, 2021.

In this talk I will introduce a new class of strategies for solving synthesis in non-Markovian stochastic domains with linear-time goals called 'stochastic best-effort' (SBE) strategies. A SBE strategy is one that, from every history, ensures the goal is satisfied with probability 1 if this is possible, and otherwise ensures the goal is satisfied with positive probability if this is possible.
Like optimal strategies, SBE strategies take advantage of stochasticity even if the goal cannot be enforced with probability 1 from the initial state. However, in contrast to optimal strategies, SBE strategies always exist. Moreover, like strategies that enforce the goal with probability 1, SBE strategies do not depend on the precise probabilities (under some reasonable and necessary conditions).
At the end of the talk, I will discuss how these results shed light on the nature of nondeterministic planning in AI.
This is joint work with Benjamin Aminof, Giuseppe De Giacomo, and Florian Zuleger.

This talk is based on joint work with Sasha Rubin and François Schwarzentruber, published in AAAI22.
I will introduce a new type of problem in logic called the formula synthesis problem: for a logic L, given a set of formulas represented by a context-free grammar G, and a structure M , find a formula ϕ (or say none exists) generated by G that is true in M. This problem generalizes the model-checking problem (in case the grammar generates just a single formula). I will instantiate this problem taking L to be propositional dynamic logic (PDL) extended with program shuffle. This is a very interesting case because PDL formulas contain programs.
In this setting, the formula synthesis problem is undecidable, but I will consider some natural restrictions that are decidable using classic tools of tree automata theory. For instance, the problem is EXPTIME-complete if the logic is restricted to PDL. The choice of this logic was also motivated by rephrasing a hierarchical synthesis problem in AI known as Hierarchical Task Network Planning.

We study the synthesis problem for first order specifications in a distributed setting where agents do not fully see what other agents are doing.
More specifically, we consider data words as executions, i.e. a sequence of pairs including an action from a finite alphabet (what action has been performed) and a data value from an infinite domain (what agent performed the action).
The agents collaborate against an adversarial environment in a game structure in order to create an execution that should satisfy a given specification.
Typically one would find a winning strategy for the agents in the form of a single controller that essentially dictates at every moment what agent should perform which action.
However, this is not really a distributed strategy and need every agent to be able to see the whole system at all times, which is unrealistic for some applications.
Therefore we study the setting where an agent perceives its own actions, but other agents will only see what kind of action has been performed but not from which agent it originates.
This setting introduces several interesting differences with respect to the full view setting.
We show that the synthesis problem is undecidable for some fragments of first order logic, while the precise boundary between decidability and undecidability remains a work in progress.

We show the undecidability of the controller synthesis problem when both the plant and the controllers are asynchronous automata and the controllers have causal memory.

Modern CPUs diverge from the idealized, linear execution of code in two main ways: by having multiple cores that execute concurrently and by offering instructions that can compute component-wise operations on vectors. This talk focuses on the latter and how these instructions can be employed in the context of automata algorithms. These instructions, known as Single Instruction Multiple Data (SIMD), come in a wide variety of shapes and forms, with perks and caveats, and my goal is to provide some guidelines on how to use them.
I will give a short introduction on SIMD instructions, then present several examples where SIMD instructions have been used to boost the performances of automata-related algorithms. In particular, this will include Acacia-Bonsai, an LTL-synthesis C++ program that I developed together with Guillermo Pérez, and some exploratory work with several colleagues relying on circuit complexity.

In general, finite concurrent two-player reachability games are only determined in a weak sense: the supremum probability to win can be approached via stochastic strategies, but cannot be realized.
We introduce a class of concurrent games that are determined in a much stronger sense, and in a way, it is the largest class with this property. To this end, we introduce the notion of local interaction at a state of a graph game: it is a game form whose outcomes (i.e. a table whose entries) are the next states, which depend on the concurrent actions of the players. By definition, a game form is determined iff it always yields games that are determined via deterministic strategies when used as a local interaction in a Nature-free, one-shot reachability game. We show that if all the local interactions of a graph game with Borel objective are determined game forms, the game itself is determined: if Nature does not play, one player has a winning strategy; if Nature plays, both players have deterministic strategies that maximize the probability to win. This constitutes a clear-cut separation: either a game form behaves poorly already when used alone with basic objectives, or it behaves well even when used together with other well-behaved game forms and complex objectives.
Existing results for positional and finite-memory determinacy in turn-based games are extended this way to concurrent games with determined local interactions (CG-DLI).

Stochastic games (SGs) (with a reachability objective) are considered a fundamental construct both from a theoretical and a practical point of view. Regarding one aspect of their practical importance is that SGs serve as a standard model in the quantitative verification and strategy synthesis for complex systems, since they are able to express both stochastic and non-stochastic uncertainty. As a result, solving these types of games is an important problem which has gained a lot of interest over the years.

The most common solution techniques for reachability problems for SGs fall under the scope of the dynamic (e.g. value/strategy iteration, or extensions thereof) and quadratic programming paradigms [1]. However, the performance of these algorithms is often sensitive to the underlying graph structure of the models and assessing their performance can be challenging [2]. In addition, in certain cases, worst-case analysis can be pessimistic and does not provide any practical guidance over which algorithm to choose for a particular type of model. Moreover, the limited availability of realistic case studies renders the performance assessment of these algorithms based on experimental analysis not a viable alternative. In addition, the few specialized handcrafted reachability models which are available can be misleading in accurately evaluating the performance of algorithms over more general problems, since only extreme cases are considered.

We address these issues by developing an automated approach for the experimental comparison of algorithms by giving the ability to the users to emphasize towards specific model structures (e.g. amount of strongly connected components, etc.). This is based on our random SG generator and its extensions which facilitate the performance evaluation of algorithms for solving SGs, by allowing the user to analyze the sensitivity of the algorithms against several model parameters.

In this talk, I will first address the model-sensitive nature of these algorithms with respect to their performance, and then how our approach could help in tackling this issue. This is joint work with Muqsit Azeem, Jan Křetínský, Alexander Slivinskiy and Maximilian Weininger.

Stochastic games (SG), e.g. [4], are important as they can be used to model decision-making in the presence of adversary and uncer- tainty. We look at the SGs with reachability objective[s], called simple SG (SSG) [1]. Algorithms to solve SSGs can broadly be classified as pre- cise algorithms and approximate algorithms. On the one hand, Strategy Iteration (SI) and Quadratic Programming (QP) are precise algorithms, they are usually slow in practice. On the other hand, Value Iteration (VI) is an approximate algorithm which is faster than SI and QP, regarded as a standard solution approach to solve SSGs in practice. However, VI suffered from the lack of an stopping criterion. Recently, several solutions have appeared, such as “bounded” VI (BVI) [3], Widest Path (WP) [5], and “optimistic” VI (OVI) [2]. Among these, OVI is applicable only to one-player SGs with a particular graph structure, namely that they do not contain a certain kind of cycle, called end component. We lift these two assumptions, making them available to general SSGs. Further, we utilize the idea in the context of topological VI, where we provide an efficient precise solution.
This is a joint work with Alexandros Evangelidis, Jan Křetı́nský, Alexandar Silvinsky and Maximilian Weininger.


[1] Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203–224
(1992). https://doi.org/10.1016/0890-5401(92)90048-K
[2] Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 488–511. Springer (2020).
https://doi.org/10.1007/978-3-030-53291-8“˙26
[3] Kelmendi, E., Krämer, J., Kretı́nský, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 623–642. Springer (2018).
https://doi.org/10.1007/978-3-319-96145-3“˙36
[4] Mertens, J.F., Neyman, A.: Stochastic games. International Journal of Game Theory 10(2), 53–66 (Jun 1981). https://doi.org/10.1007/BF01769259,
https://doi.org/10.1007/BF01769259
[5] Phalakarn, K., Takisaka, T., Haas, T., Hasuo, I.: Widest paths and global propagation in bounded value iteration for stochastic games. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 349–371. Springer (2020).
https://doi.org/10.1007/978-3-030-53291-8“˙19

We study infinite two-player win/lose games (A,B,W) where A,B are finite and W is the winning set. At each round Player 1 and 2 concurrently chose one action in A and B respectively. Player 1 wins iff the generated sequence is in W.

We show that, under some topological conditions on the shape of the winning set (it can be expressed both as a countable union of closed sets and a countable intersection of open sets) as well as a well-partial order condition on the winning sets induced by the histories, when Player 1 has a winning strategy she has a finite-memory one. This result was presented at CSL 2022.

We will see how this result can be applied to well-studied classes of games (e.g. energy games, reachability games), as well as provide counter-examples that show that it is tight.

Co-authors: Patricia Bouyer, Stéphane Le Roux, Nathan Thomasset

We present a notion of game defined on Petri nets between two players: a user and an environment. The user has a goal on the system, expressed with an LTL formula, and the environment plays against her.
Each player controls a subset of transitions, and the environment must satisfy a progress constraint, i.e. cannot block the system if some of its transitions are enabled.
A play is a run on the unfolding of the net, and the user wins it if the play satisfies the formula. In order to reach her goal, the user can select some transitions to fire based on her information on the state of the system.
In particular, we assume that she can never observe the value of some local states, and she may receive the value of others with a certain delay, possibly preventing her to use this information.
The behavior of the user is coded into a strategy, that associates a set of choices to each partial cut observable by the user.
We discuss our ongoing researches based on this model.
First, we show some relations between our model and concurrent game structures in case of strategy with full and no memory.
In particular, we show that, when the strategy has no memory, the game on the net can be translated into a game on the concurrent game structure, and therefore we can look for strategies for the user using algorithms on graphs.
This translation fails when we consider strategies with full memory, since the unfolding stores information about different occurrences of the same local states, that are not included in the usual approaches on concurrent structures, and this leads to the idea of looking for algorithms defined directly on the unfolding.
Finally, we discuss how to implement a winning strategy on the net, if one exists, by adding places representing causality constraints for the controllabletransitions, so that all the maximal runs of the modified net satisfy the LTL formula.
This is a joint work with Luca Bernardinello and Lucia Pomello.

Two-player (antagonistic) games on (possibly stochastic) graphs are a prevalent model in theoretical computer science, notably as a framework for reactive synthesis.

Optimal strategies may require randomisation when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There is no unique way to define randomised strategies. For instance, one can use so-called mixed strategies or behavioural ones. In the most general settings, these two classes do not share the same expressiveness. A seminal result in game theory - Kuhn's theorem - asserts their equivalence in games of perfect recall.

This result crucially relies on the possibility for strategies to use infinite memory, i.e., unlimited knowledge of all the past of a play. However, computer systems are finite in practice. Hence it is pertinent to restrict our attention to finite-memory strategies, defined as automata with outputs. Randomisation can be implemented in these in different ways: the initialisation, outputs or transitions can be randomised or deterministic respectively. Depending on which aspects are randomised, the expressiveness of the corresponding class of finite-memory strategies differs.

In this work, we study two-player turn-based stochastic games and provide a complete taxonomy of the classes of finite-memory strategies obtained by varying which of the three aforementioned components are randomised. Our taxonomy holds both in settings of perfect and imperfect information.

This talk is based on joint work with Mickael Randour.

An infinite-state system is bidirected (sometimes called reversible) if for every transition, there exists another with opposite effect. We study reachability in bidirected systems in the framework of valence systems, an abstract model featuring finitely many control states and an infinite-state storage that is specified by a finite graph. Picking suitable graphs yields counters as in vector addition systems, pushdowns, integer counters, and combinations. We provide a comprehensive complexity analysis. For example, the complexity of bidirected reachability drops substantially (often to polynomial time) from that of general reachability, for almost every storage mechanism where general reachability is known to be decidable.
This is joint work with Moses Ganardi and Rupak Majumdar.
See https://arxiv.org/abs/2110.03654

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every operation (pushing a symbol or modifying a counter) has an accompanying opposite operation that reverses the operation (popping the symbol or reversing the change in the counter). Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the directed setting, where reachability is a long-standing open problem already for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimenstional PVASS with bounded stack.

The reachability relation in the bidirected (stateless) case is a congruence over N^d. Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. For the special case of one-dimensional PVASS, we show a saturation procedure over bounded-size counters.

We complement our upper bound with a TOWER-hardness result for arbitrary dimension and k-EXPSPACE hardness in dimension (2k+6) using a technique by Lazić and Totzke to implement iterative exponentiations.

This is joint work with Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche.

We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general, the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand, we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand, we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.

The whole paper is here: https://arxiv.org/abs/2202.08033
and it is currently submitted to LICS.

We study the regular separability problem for Büchi VASS languages: Given two
Büchi VASS with languages L_1 and L_2, check whether there is a regular language
that fully contains L_1 while remaining disjoint from L_2.

We show that the problem is decidable in general and PSPACE-complete in the
1-dimensional case assuming a succinct encoding. The results rely on several
arguments. We characterize the set of all regular languages disjoint from L_2.
Based on this, we derive a (sound and complete) notion of inseparability witnesses,
non-regular subsets of L_1. Finally, we show how to symbolically represent
inseparability witnesses and how to check their existence.

For finite-word VASS coverability languages, regular separability is known to be
equivalent to disjointness, a result that carries over to more general WSTS.
We show that, for infinite words, the situation is different. There are disjoint
Büchi VASS languages where separability fails. Moreover, there is a natural class of
WSTS such that for their languages of infinite words, intersection is decidable, but
regular separability is undecidable.

We study a particular reachability problem for vector addition systems with states (VASS), a well-studied class of infinite-state systems. The central problems are: the reachability problem, given two configurations, to decide whether you can reach one from the other one; and its relaxation the coverability problem. We consider the variant of 2-VASS where one counter is encoded in binary and the other in unary. Our main result is that the coverability problem for 2-VASS with one binary counter and one unary counter is in NP, an improvement upon the naively inherited PSPACE upper bound from coverability in binary 2-VASS. For our main technical contribution, we prove that every witnessing path can be modified to a path in a certain succinct linear form, that can then be guessed in NP.

We consider linear cost-register automata (equivalent to weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata.
The two problems of boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and to zero, respectively.
We aim to settle the decidability status for both problems.
In the general model both problems are undecidable so we focus on restrictions to the model.
In the case of copyless linear restriction we show that the boundedness problem is decidable.

As for the zero isolation problem we show undecidability already for copyless CRA---note copyless CRA are not necessarily linear but are a subclass of linear CRA (non-copyless).
For decidability, we need to further restrict the class.
We obtain a model, where zero isolation becomes equivalent to universal coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own.
In standard VAS runs are considered only in the positive orthant, while in OVAS every orthant has its own set of vectors that can be applied in that orthant.
Assuming Schanuel’s conjecture is true, we prove decidability of universal coverability for three-dimensional OVAS, which implies decidability of zero isolation in a model with at most three independent registers.
On the other hand the OVAS coverability problem is undecidable.

Joint work with Wojciech Czerwiński, Engel Lefaucheux, Filip Mazowiecki, and Markus Whiteland.

We study the complexity of the reachability problem for Vector Addition Systems with States (VASSes) in fixed dimensions. We provide four lower bounds improving the currently known state-of-the-art: 1) NP-hardness for unary flat 3-VASSes (VASSes in dimension 3), 2) PSpace-hardness for unary 5-VASSes, 3) ExpSpace-hardness for binary 6-VASSes and 4) Tower-hardness for unary 8-VASSes. On the presentation I plan to tell a few words about 1) the results, 2) techniques, which we have used, 3) motiviations to study low dimensional VASSes, and 4) important challenges, which remain for the future.

Previous version of this work was submitted to LICS 2022, a co-autor is Łukasz Orlikowski. The work is on arXiv.

Tree algebras in many of their forms, such as clones, hyperclones, operads, etc, as well as other kind of algebras, are infinitely sorted: the carrier is a multi sorted set indexed by a parameter that can be interpreted as the number of variables or hole types. Finite such algebras - meaning when all sorts are finite - can be classified depending on the asymptotic size of the carrier sets as function of the parameter, that we call the complexity of the algebra. This naturally defines the notions of algebras of bounded, linear, polynomial, exponential or doubly exponential complexity…

In previous work, we gave a precise description of the languages recognized by tree algebras of bounded complexity [ICALP 2021] and polynomial complexity, and proved the decidability of these classes. This talk is a continuation of that line of work, in which we describe the expressive power of tree algebras of exponential complexity.

This is joint work with Thomas Colcombet.

In the presentation, I will highlight some exciting joint work with Saptarshi Sarkar
and A V Sreejith. This work strengthens the recent algebraic framework/approach
for MSO-definability on countable words and provides a refined understanding of
language-logic-automata-algebra interplay beyond the standard settings of finite
and omega-words.

We propose an effective construction of block product operation into this framework
and generalize well-known block-product based decompositional characterizations of
first-order (FO) and its two variable fragment. One of the key benefits of such
characterizations is that it supports, thanks to the block product principle,
inductive reasoning. For instance, it can be used to prove
Schützenberger-McNaughton-Papert-Krohn-Rhodes-theorem over countable words which
equates marked star-free regular expressions, FO-logic and block-products of
a simple two-element algebra U_1.

Going beyond FO, we propose a new extension of FO which admits infinitary
quantifiers to reason about inherent infinitary properties of countable words,
and obtain a natural hierarchical block-product based characterization of this
extension. Its role in view of classical logical systems such as WMSO and
FO[cut] is explicated. We also rule out the possibility of a finite-basis for
a block-product based characterization of these logical systems. The presentation
will be based on results which have appeared in LICS'19, FCT'21 and some ongoing
efforts to provide block-product based characterizations for several sublogics of MSO.

Higher-dimensional automata (HDAs) were introduced by Pratt and van Glabbeek as a geometrical model for non-interleaving concurrency. HDAs are general models of concurrency that subsume, for example, event structures and safe Petri nets. Unlike for standard automata and many other models, there has until recently been no theory of languages of HDAs. Such notions are important for connecting models to behaviours, but HDAs have been developed first of all with a view on operational, topological and geometric aspects.

In two recent papers [1,3] we have started to develop the language theory of HDAs. Like languages related to other formalisms for concurrency, languages of HDAs need to account for both the sequential and the concurrent nature of computations. Their elements are thus finite pomsets. More precisely, we show in [1] that languages of HDAs are subsumption-closed sets of interval-order pomsets with interfaces [2] and that these languages are closed under union and parallel composition.

Union, parallel composition, serial composition, and the (serial) Kleene star give a natural notion of rational languages, and in [3] we show a Kleene-type theorem that the rational languages are precisely the regular languages. This requires rather intricate tools from algebraic topology which may be of independent interest.

Joint work with Christian Johansen (NTNU, Norway), Georg Struth (U of Sheffield, UK and Collegium de Lyon, France), and Krzysztof Ziemiański (Warsaw U, Poland) based on the following papers:
[1] https://arxiv.org/abs/2103.07557
[2] https://arxiv.org/abs/2106.10895
[3] https://arxiv.org/abs/2202.03791

The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity (e.g. as found on the linear-time/branching-time spectrum) over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand. We illustrate the mentioned constructions in the case of trace equivalence on labelled transition systems. This talk is based on joint work with Harsh Beohar, Barbara König, Stefan Milius, and Lutz Schröder.

The regular languages with a neutral letter expressible in first-order logic with one alternation are characterized. Specifically, it is shown that if an arbitrary Sigma_2 formula defines a regular language with a neutral letter, then there is an equivalent Sigma_2 formula that only uses the order predicate. This shows that the so-called Central Conjecture of Straubing holds for Sigma_2 over languages with a neutral
letter, the first progress on the Conjecture in more than 20 years. To show the characterization, lower bounds against polynomial-size depth-3 Boolean circuits with constant top fan-in are developed. The heart of the combinatorial argument resides in studying how positions within a language are determined from one another, a technique of independent interest.
This is joint work with Michaël Cadilhac, Charles Paperman and Thomas Zeume.

We consider regular languages of words whose domain is a countable scattered linear ordering (examples of countable scattered linear orders include the set of integers or any countable ordinal). Given two regular languages, we want to decide whether there exists a formula of first-order logic that is satisfied by every word of the first language but by no word of the other. We prove that this problem is decidable using an algebraic construction: given a morphism from the set of all words to a finite scattered monoid, we show that one can effectively build a function that approximates the original morphism while being definable in first-order logic. Essentially, this approximant is obtained from the original morphism by forgetting about group-like phenomena and gap-detection using an algorithm resembling Henckell's saturation algorithm for computing aperiodic pointlike sets of finite semigroups.
We also study the case of words indexed by countable ordinals (on which first-order logic admits a simpler characterisation), which was published at FoSSaCS '22, and separation by first-order logic extended with monadic quantification over Dedekind cuts.
This is joint work with Thomas Colcombet and Sam van Gool.

We present the first passive learner for the full class of deterministic Büchi automata (DBA). Given a finite sample consisting of positive and negative example words, the learner constructs a DBA by combining multiple DFAs, which it infers using a polynomial-time active learning algorithm (e.g. L*).
We show that our algorithm can learn all DBA-recognizable languages in the limit in polynomial time, thus it generalizes known results of passive learning for ω-automata, which are complete only for the class of languages with an informative right congruence.
While completeness of our algorithm for the full class of DBA-recognizable languages can only be guaranteed through characteristic samples that are, in general, exponential in the size of the minimal DBA for the target language, we show that for a fixed k, the class of DBAs with at most k language-equivalent states can be learned in the limit from polynomial data. As the minimal DBA for a language with an informative right congruence has precisely one language-equivalent state per congruence class, our approach thus also recovers the previously known results.
This is joint work with Christof Löding.

Joint work with Alex Rabinovich.

The question of uniformization consists, given a formula $\Psi(X,\bar Y)$, in constructing a formula $\Psi^*(X,\bar Y)$ such that, for all valuations of $\bar Y$, if there exists some $X$ such that $\Psi(X,\bar Y)$ holds, then there exists a unique $X$ such that $\Psi^*(X,\bar Y)$, and $\Psi(X,\bar Y)$.

It is known, from [Lifsches and Shelah 98], that uniformization is not possible on the ordinal $\omega^\omega$. The non-uniformizable property $\Phi_\omega(X)$ states that $X$ has order type $\omega$ and is cofinal in the universe of the chain.

In this work, we establish two results:

(1) MSO can be uniformized over all countable ordinals in the extended logic MSO+$u_\omega$. There, $u_\omega(Y)$ is a new construct which, given a set $Y$, outputs a set $X:=u_{\omega}(Y)\subseteq Y$ of order-type $\omega$ and cofinal in $Y$. In some sense, this result shows that the counter-example of [Lifsches and Shelah 98] is the maximal obstruction that prevents MSO from being uniformizable over countable ordinals.

(2) It is decidable, given a monadic formula, whether it can be uniformized over all ordinals.

The results relies on the composition method / the algebraic theory of monadic theories over chains. On the algebraic side, it relies on classical tool for semigroups and monoids that are Green's relations and factorization forests (in a slightly non standard version which is definable over ordinals).

We introduce a new acceptance type for regular \omega-languages, called extension acceptance, which unifies all classical acceptance conditions.
We show that extension acceptance has several advantages over other acceptance conditions:
1) All classical acceptance types for regular \omega-languages, like Rabin and Muller acceptance, can be translated into extension acceptance in polynomial time and they can be seen as simple restriction of extension acceptance.
2) Boolean operations on deterministic extension automata (DEA) cause only polynomial blowup.
3) Emptiness and other decision problems for DEAs can be decided in polynomial time.
4) An extension condition is easy to specify and it can be decided in polynomial time whether a given tuple is an extension condition.
Further, extension acceptance is tightly connected to the Wagner hierarchy and to Zielonka trees.

During the talk I want to overview recent results on the following problem:
- given a regular language of infinite trees L,
- compute (a representation of) the standard measure \mu(L).

This talk will be based on joint results with Damian Niwiński and Marcin Przybyłko.

We study first-order logic (FO) over the structure consisting of finite words over some alphabet A, together with the (non-contiguous) subword ordering. In terms of decidability of quantifier alternation fragments, this logic is well-understood: If every word is available as a constant, then even the \\Sigma_1 (i.e., existential) fragment is undecidable, already for binary alphabets A.
However, up to now, little is known about the expressiveness of the quantifier alternation fragments: For example, the undecidability proof for the existential fragment relies on Diophantine equations and only shows that recursively enumerable languages over a singleton alphabet (and some auxiliary predicates) are definable.
We show that if |A| ≥ 3, then a relation is definable in the existential fragment over A with constants if and only if it is recursively enumerable. This implies characterizations for all fragments \Sigma_i: If |A| ≥ 3, then a relation is definable in \Sigma__i if and only if it belongs to the i-th level of the arithmetical hierarchy. In addition, our result yields an analogous complete description of the \Sigma_i-fragments for i ≥ 2 of the pure logic, where the words of A^* are not available as constants.

In this talk, we will present the paper "Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes", accepted at TACAS 2022, the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, and nominated for a best-paper award.

The paper introduces a similarity function on formulae of signal temporal logic (STL). The similarity function comes in the form of a kernel function, well known in machine learning as a conceptually and computationally efficient tool. The corresponding kernel trick allows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task of predicting (quantitative) satisfaction of STL formulae on stochastic processes:
Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor.

We will discuss also the possible interesting applications of the technique. The main potential of our kernel (and generally introducing kernels for any further temporal logics) is that it opens the door to efficient learning on formulae via kernel-based machine-learning techniques. Other applications that immediately suggest themselves are: game-based synthesis, translating, sanitizing and simplifying specifications, and requirement mining.

Trace Alignment is a prominent problem in Declarative Process Mining, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in DECLARE, a strict sublanguage of linear-time temporal logic over finite traces (LTLf). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf. In this presentation, we introduce the timed version of trace alignment,
where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf ), essentially a superlanguage of LTLf. Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.

Monitoring the behavior of dynamical systems often requires reasoning about interconnected entities arranging in the spatial environment and evolving over time. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and reason about spatio-temporal properties. STREL considers each system’s entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing the node’s behavior. While algorithms already existed for monitoring STREL specifications offline, over pre-recorded traces, we are widening the boundaries of applicability of this formal technique by extending the methodology to solve a plethora of real-world challenges, spanning from monitoring out-of-order imprecise samples, to providing partial guarantees, and to defining new operators to increase its expressivity.
The co-authors of this research are Ezio Bartocci, Michele Loreti, Laura Nenzi, who contributed to a previous publication to the International Conference on Formal Methods and Models for System Design (MEMOCODE '21), and who are actively working on future developments.

We introduce a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We define three new logics: TeamLTL, TeamCTL and TeamCTL∗, which are obtained by adding quantification over so-called time evaluation functions controlling the asynchronous progress of traces. We study the complexity of model checking of different fragments of the new logics, and map their undecidability boundier. We show that the model checking problem for already the existential fragment of TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. On the positive side, we present a translation from TeamCTL∗ to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfiability problems. Finally, we identify a restrictive setting in which model checking can be done in polynomial time.

This is joint work with Jens Oliver Gutsfeld, Arne Meier, and Christoph Ohrem.

Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL formulas for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open-source implementation against publicly available benchmarks.

In this talk we consider two different views of the model checking problems for the Linear Temporal Logic (LTL). On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula that all the runs of the system satisfy the formula. On the other hand, fair model checking problem for LTL asks that for a given system and a given formula almost-all the runs of the system satisfy the formula.
It was shown that these two problems have the same theoretical complexity i.e. PSPACE complete. The question arises whether one can find a fragment of LTL for which the complexity of these two problems differs. One such fragment was identified in a previous work, namely the Muller fragment.
We address a similar comparison for the prompt fragment of LTL (pLTL). pLTL extends LTL with an additional operator, i.e., the prompt-eventually. This operator ensures the existence of a bound such that liveness properties are satisfied within this bound.
We show that the corresponding Muller fragment for pLTL does not enjoy the same algorithmic properties with respect to the comparison considered. We also identify a new fragment for which the fair model checking is faster than the universal one.
This is a joint work with Youssouf Oualhadj and Daniele Varacca.

Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, that are supposed to work for any SAT problem.

We introduce BSaLTic, a SAT-based BMC tool that tunes the SAT algorithm using: (1) a static classification based on the variables used to encode the BMC into a boolean formula, (2) and by exploiting the hierarchy of Manna&Pnueli(Manna1990AHO) that classifies any property expressed through Linear-time Temporal Logic (LTL). By combining these two information with the classical Literal Bloc Distance (LBD) measure, we designed a new heuristic, well suited for solving BMC problems. In particular, BSaLTic identifies and exploit new set of relevant learnt clauses.

Our experiments over a large database of BMC problems, show promising results. In particular, BSaLTic provides good performances on UNSAT problems. This work highlights the importance of considering the structure of the underlying problem in SAT procedures.

Co-authors: Etienne RENAULT and Souheib BAARIR

Decision-making policies for agents are often synthesized with the constraint that a formal specification of behaviour is satisfied. Here we focus on infinite-horizon properties. On the one hand, Linear Temporal Logic (LTL) is a popular example of a formalism for qualitative specifications. On the other hand, Steady-State Policy Synthesis (SSPS) has recently received considerable attention as it provides a more quantitative and more behavioural perspective on specifications, in terms of the frequency with which states are visited. Finally, rewards provide a classic framework for quantitative properties. In this paper, we study Markov decision processes (MDP) with the specification combining all these three types. The derived policy maximizes the reward among all policies ensuring the LTL specification with the given probability and adhering to the steady-state constraints. To this end, we provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. This is enabled by Limit-Deterministic Büchi Automata (LDBA), recently studied in the context of LTL model checking on MDP, and allows for an elegant solution through a simple linear programme. The algorithm also extends to the general omega-regular properties and runs in time polynomial in the sizes of the MDP as well as the LDBA.

The paper has been published in IJCAI'21.

Sebastiaan Brand and Alfons Laarman

Computing fixpoints is a core task in model checking, as the verification of many properties can be reduced to it. Among decision diagram based approaches to computing fixpoints, the saturation algorithm is considered to be the state-of-the-art method. We present a new, relatively simple decision diagram operation to compute fixpoints called REACH. Unlike saturation, our algorithm does not require the transition relation to be partitioned, but rather can take as input a single global transition relation. We give implementations of REACH for both binary and multi-valued decision diagrams. We benchmark our algorithm against saturation on a set of 692 model checking problem instances in different languages. Our experimental results show that there is a large set of instances on which REACH outperforms saturation. From the theoretical side we show that there exist instances for which REACH is exponentially faster than saturation.

Planning problems can be solved not only by planners but also by model checkers. While the former yield a plan that requires replanning as soon as any fault occurs, the latter provides a “universal” plan (a.k.a. strategy, policy, or controller) able to make decisions under all circumstances. One of the prohibitive aspects of the latter approach is stemming from this very advantage: since it is defined for all possible states of the system, it is typically so large that it does not fit into small memories of embedded devices. As another consequence of the size, its execution may be slow. In this paper, we provide a solution to this issue by linking the model checkers with decision-tree learners, resulting in decision-tree representations of the synthesized strategies. Not only are they dramatically smaller, but also more explainable and orders-of-magnitude faster to execute than plans with replanning. In addition, we describe a method for model validation and debugging via the model checker and the decision-tree learner in the loop. We illustrate the approach on our case study of a robotic arm for picking items in a real industrial setting.
Joint work with Jonis Kiesbye, Pranav Ashok, Jan Kretinsky.

We are interested in constructing linear temporal formulas (LTL) from finite traces. The problem has attracted a lot of attention recently in different communities: software engineering, verification and control of cyber-physical systems, and artificial intelligence.

In this talk, I will report on two papers:
- a complexity-theoretic study, published in ICGI'21 with Guillaume Lagarde
- a tool, published in TACAS'22 with Ritam Raha, Rajarshi Roy, and Daniel Neider

The goal of these papers is to develop new algorithms for learning fragments of LTL by analysing formulas at a syntactic level.

Markov decision processes (MDP) and continuous-time MDP (CTMDP) are the fundamental models for non-deterministic systems with probabilistic uncertainty. Mean payoff (a.k.a. long-run average reward) is one of the most classic objectives considered in their context. We provide the first algorithm to compute mean payoff probably approximately correctly in unknown MDP; further, we extend it to unknown CTMDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability, which has been advocated in literature. In addition to providing PAC bounds for our algorithm, we also demonstrate its practical nature by running experiments on standard benchmarks.

This is a joint work with Chaitanya Agarwal, Jan Křetínský, and M. Pazhamalai.

Many verification problems for probabilistic systems address optimal expected values of incurred costs or received rewards. In Markov decision processes (MDPs), a standard operational model combining non-deterministic and probabilistic transitions, these verification questions frequently result in stochastic shortest path problems where the task is to find a scheduler that optimizes the expected value of the amount of weight accumulated before reaching a target state. Other aspects besides the expectation of the resulting probability distribution of the accumulated weights are completely disregarded.

In many application areas, however, the uncertainty coming with the probabilistic behavior cannot be neglected. In traffic control systems or energy grids, for example, large variability in the throughput comes at a high cost due to the risk of traffic jams or the difficulty of storing surplus energy. Also a probabilistic program employed in a complex environment might be of more use with a higher expected termination time in exchange for a lower chance of extreme termination times. A standard measure to quantify probabilistic uncertainty is the variance.

This talk will address problems arising in finding a good tradeoff between variance and expectation in the stochastic shortest path problem. One way to achieve different tradeoffs is to consider variance-penalized expectations where a multiple of the variance is incurred as a penalty on the obtained expectation. Varying the penalty factor leads to different tradeoffs. We show that variance-penalized expectations in MDPs with non-negative weights can be computed in exponential space and that the corresponding threshold problem whether the optimum exceeds a given rational is in NEXPTIME and EXPTIME-hard. In addition, optimal schedulers can be chosen to be deterministic finite-memory schedulers.

Furthermore, the talk will indicate difficulties arising in the question whether there is a scheduler that achieves at least an expectation of e while having variance at most v for given rationals e and v: Schedulers using memory and randomization are necessary here in general. In addition, when plotting possible combinations of expectation and variance that can be achieved by schedulers in an MDP, the resulting feasible region is not convex and the border is composed of parabolic line segments. This indicates a significant contrast to many other problems on weighted MDPs.

The talk is based on ongoing joint work with Ocan Sankur and Christel Baier.

We show how to construct small optimal strategies for MDPs using strategy improvement.
We represent strategies as a list of rules and directly perform strategy improvements over such strategies with little overhead.
This is joint work with Nathanaël Fijalkow.

Nondeterministic Good-for-MDP (GFM) automata are for MDP model checking and reinforcement learning what good-for-games automata are for synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof.

We study the problem of finding optimal strategies in Markov decision processes with lexicographic omega-regular objectives, which are ordered collections of ordinary omega-regular objectives. The goal is to compute strategies that maximise the probability of satisfaction of the first omega-regular objective; subject to that, the strategy should also maximise the probability of satisfaction of the second omega-regular objective; then the third and so forth. For instance, one may want to guarantee critical requirements first, functional ones second and only then focus on the non-functional ones. We show how to harness the classic off-the-shelf model-free reinforcement learning techniques to solve this problem and evaluate their performance on four case studies.

(Joint work with Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, and Ashutosh Trivedi.)

The first-order model checking problem for finite graphs asks, given a graph G and a first-order sentence phi as input, to decide whether phi holds on G. After the existence of an efficient model checking algorithm was shown for classes of sparse graphs, attention turned to the more general setting of graph classes which can be obtained from sparse graphs via interpretations/transductions. However, despite efforts of several groups of researchers, no positive algorithmic result has been achieved since 2016, when the existence of an efficient algorithm was shown for graph classes interpretable in graphs of bounded degree.

We present a fixed-parameter tractable algorithm for first-order model checking on interpretations of graph classes with bounded local cliquewidth. Notably, this includes interpretations of planar graphs (and more generally, of locally bounded treewidth) and vastly generalizes the result for interpretations of graphs of bounded degree. To obtain this result we developed a new tool which works in a very general setting of dependent classes and which we believe can be an important ingredient in achieving similar results in the future.

This is joint work with Édouard Bonnet, Jan Dreier, Stephan Kreutzer, Nikolas Mählmann, Pierre Simon, Szymon Toruńczyk.

We give new decomposition theorems for classes of graphs that can be transduced in first-order logic from classes of sparse graphs - more precisely, from classes of bounded expansion and from nowhere dense classes. In both cases, the decomposition takes the form of a single coloured rooted tree of bounded depth where, in addition, there can be links between nodes that are not related in the tree. The constraint is that the structure formed by the tree and the links has to be sparse. Using the decomposition theorem for transductions of nowhere dense classes, we show that they admit low-shrubdepth covers of size O(n^ε), where n is the vertex count and ε>0 is any fixed real. This solves an open problem posed by Gajarský et al. (ACM TOCL '20) and also by Briański et al. (SIDMA '21).

The talk is based on work conducted with Jan Dreier, Jakub Gajarský, Michał Pilipczuk, and Szymon Toruńczyk.

We establish a list of characterizations of bounded twin-width for hereditary classes of totally ordered graphs:
as classes of at most exponential growth studied in enumerative combinatorics, as monadically NIP classes studied in model theory, as classes that do not transduce the class of all graphs studied in finite model theory, and as classes for which model checking first-order logic is fixed-parameter tractable studied in algorithmic graph theory.

This has several consequences.
First, it allows us to show that every hereditary class of ordered graphs either has at most exponential growth, or has at least factorial growth. This settles a question first asked by Balogh, Bollobás, and Morris [Eur. J. Comb. '06] on the growth of hereditary classes of ordered graphs, generalizing the Stanley-Wilf conjecture/Marcus-Tardos theorem.
Second, it gives a fixed-parameter approximation algorithm for twin-width on ordered graphs.
Third, it yields a full classification of fixed-parameter tractable first-order model checking on hereditary classes of ordered binary structures.
Fourth, it provides a model-theoretic characterization of classes with bounded twin-width.

We introduce a logic called distance neighborhood logic with acyclicity and connectivity constraints (A&C DN for short) which extends existential MSO1 with predicates for querying neighborhoods of vertex sets and for verifying connectivity and acyclicity of vertex sets in various powers of a graph. Building upon [Bergougnoux and Kanté, ESA 2019; SIDMA 2021], we show that the model checking problem for every fixed A&C DN formula is solvable in n^O(w) time when the input graph is given together with a branch decomposition of mim-width w. Nearly all problems that are known to be solvable in polynomial time given a branch decomposition of constant mim-width can be expressed in this framework. We add several natural problems to this list, including problems asking for diverse sets of solutions.
Our model checking algorithm is efficient whenever the given branch decomposition of the input graph has small index in terms of the d-neighborhood equivalence [Bui-Xuan, Telle, and Vatshelle, TCS 2013]. We therefore unify and extend known algorithms for tree-width, clique-width and rank-width. Our algorithm has a single-exponential dependence on these three width measures and asymptotically matches run times of the fastest known algorithms for several problems. This results in algorithms with tight run times under the Exponential Time Hypothesis (ETH) for tree-width and clique-width; the above mentioned run time for mim-width is nearly tight under the ETH for several problems as well. Our results are also tight in terms of the expressive power of the logic: we show that already slight extensions of our logic make the model checking problem para-NP-hard when parameterized by mim-width plus formula length.
This is joint work with Benjamin Bergougnoux and Jan Dreier.

For a fixed graph family G, we are interested in the following computational problem, denoted PrMatch(G):
- The input is an undirected graph G=(V,E) of G, together with (rational) probability values p(e) for each e \in E.
- The output is the probability that G contains a simple path of length 2, when every edge e of G has a probability of existence p(e), independently from the others
Equivalently, the output is one minus the probability to obtain a *matching* of G, i.e., a subset of edges such that no two edges share an incident vertex. Note that we can set the edge probabilities to be 0, so we may assume that the family C is closed under subgraphs.
It is known that if G has bounded treewidth, then PrMatch(G) can be solved in polynomial time. The result we want to present is that, essentially, bounding the treewidth is the only way to make this problem tractable. More precisely, we show that, for any graph family G that does not have bounded treewidth, and where high-treewidth graphs can be efficiently constructed, the problem PrMatch(G) is intractable (specifically, #P-hard under RP-reductions).
During the presentation, we will present the proof for a simpler version of this result. We will show a reduction from the #P-hard problem of counting matchings in 3-regular planar graphs, which works by constructing polynomially many instances for the problem PrMatch(G) and obtaining a system of linear equations. We will show how, if the equations are invertible, we can recover the number of matchings of the original graph via multiple oracle calls to the problem . We will also discuss at a high level the intuitive idea and difficulties of the general proof, which uses the grid minor extraction theorem.
This result extends an earlier result by Amarilli, Bourhis, and Senellart at PODS'16 where the same result is shown for a more complicated property in first-order logic; and it relates to the known intractability of computing tractable lineages over such graph families. This is ongoing work that is not yet published.

During the presentation, we will study set systems formed by neighborhoods in graphs of bounded twin-width. In particular, we will prove that such classes of graphs admit linear neighborhood complexity, in analogy to previous results concerning classes with bounded expansion and classes of bounded clique-width. Additionally, we will show how, for a given graph from a class of graphs of bounded twin-width, to efficiently encode the neighborhood of a vertex in a given set of vertices A of the graph. For the encoding we will use only a constant number of vertices from A. The obtained encoding can be decoded using FO formulas. This will prove that the edge relation in graphs of bounded twin-width, seen as first-order structures, admits a definable distal cell decomposition, which is a notion from model theory. From this fact we will derive that we can apply to such classes strong combinatorial tools based on the Distal cutting lemma and the Distal regularity lemma (a stronger version of Szemerédi regularity lemma). This presentation will be based on my manuscript VC-density and abstract cell decomposition for edge relation in graphs of bounded twin-width avaliable on arxiv.

As an experiment for this year at Highlights, we closed the conference with an informal session to exchange about the software tools and other useful practices that we use to do our research. Are you the developer of a nifty software tool, or a power-user of an arcane utility or package? Do you have good or bad experiences with unusual ways to work on papers or manage your time? The floor is yours. The goal is to learn from each other, no matter where we are in our research careers.

Example of topics: LaTeX packages, command-line utilities, text editors and configuration, academic search engines, metaresearch datasets, recommendation engines, bibliography management tools, task managers, time managers, meeting planners, shared online boards, flashcard software, online discussion platforms, publication practices, e-print servers, ways to find papers, creativity techniques, research competitions, zoos, open problem lists, and many other things (surprise us!).