The Steering Committee of Highlights of Logic, Automata, and Games condemns the aggression by the Russian Federation against Ukraine in the strongest possible terms.

The Steering Committee expresses its solidarity with the Ukrainian people in their plight, calls for immediate peace, and is fully committed to peaceful co-operation, mutual understanding and tolerance across borders, and despite the current situation continues to hope for reflection, restraint and a swift end to the crisis.

Highlights is an annual conference with the goal of integrating the community of researchers working on logic, games and automata. The 2022 edition of Highlights happened from June 28th to July 1st, 2022, in Paris, France. The conference will be hosted by Université Paris-Cité, and happen on the site of Grands Moulins.

Just like other conferences in the field, Highlights proposes tutorials and invited talks. The contributed talks are just ten minutes long, allowing participants to get an overview of a wide range of different topics in a short amount of time. Additionally, authors are encouraged to prepare posters about their work, which are then presented and discussed in poster sessions.

Highlights takes place on-site, and the preferred form of participation is to give your talk in-person. Before coming from far away, please review how your trip and international flights are contributing to climate change. We encourage you to make the most of your stay in Paris, e.g., by also attending the ICALP'22 conference and/or using this opportunity for a research visit (see below).

If you cannot attend, you can watch the talks remotely via a video stream, interact via text-based questions and answers, and you can also submit a proposal for a pre-recorded talk. If it is accepted, you will provide a video of your talk, which will be hosted online with other conference videos and be advertised on-site. The selection process will not discriminate between pre-recorded talks and in-person talks.

#### Venue Information

The conference took place at the Halle aux Farines building of Université Paris Cité, at 2, rue Marguerite Duras, Paris, 13th district. The entrance to the conference rooms is below (direct link here):

The closest subway stop is "Bibliothèque François Mitterand", with subway line 14 and RER line C (suburban trains). There is also a nearby stop "Avenue de France" for tramway line T3a.

To get to the conference venue from the "Gare de l'Est" or "Gare du Nord" train stations, take metro line 4 to Châtelet and change for line 14. To come from the train station "Gare Montparnasse", take metro line 4 to Saint-Michel-Notre-Dame and change for RER C. To come from the train stations "Gare Saint-Lazare" or "Gare de Lyon", directly take metro line 14. If you are coming by coach, to get to the venue from the Paris-Gallieni coach station, the simplest is to take line 3 to "Gare Saint-Lazare" and change for line 14; to get to the venue from the Bercy coach station, you can simply walk (15 min). All these connections are possible with a regular subway ticket. If you are coming by plane, to get to the venue from the Charles-de-Gaulle airport, take RER B to Saint-Michel-Notre-Dame and change for RER C; to get to the venue from Orly airport, take CDGVAL to Antony, then RER B to Saint-Michel-Notre-Dame and change for RER C; to get to the venue from low-cost airport "Paris Beauvais", take the shuttle to Porte Maillot and take RER line C. Information about public transportation in Paris is available on the RATP website (in English), and trips can be planned with the ViaNavigo website (in English).

#### Restaurant Recommendations

The restaurant recommendations below can also be found in the printed conference program.

#### Program

You can also download the printed program in PDF.

The program describes the talk that will be given in-person. Highlights also welcomes some prerecorded online talks, by community members who do not attend in-person. These talks are available on the website and attached to a session where they will be advertised, but they will not be streamed — participants are encouraged to watch these talks at their leisure.

## Dana Fisman: Tutorial on Automata Learning

In this tutorial we will get acquainted with the research area called grammatical inference or automata learning. We will start with the earliest results on the subject, and span different learning paradigms. We will describe several positive results, and efficient algorithms for learning regular languages in various different formalisms, including deterministic, non-deterministic and alternating automata. We will prove several negative results for learning different classes of languages in different learning paradigms. We will discuss connection between learning problems and other problems in automata theory.

## S. Akshay: Boolean Functional Synthesis: A View from Theory and Practice

It is often easy to write down the specification of a system as a relation between inputs
and outputs. But implementing it requires us to take a functional view, i.e., to have
functions that produce outputs from inputs. Can we automatically synthesize such
functions from a given relational specification? In this tutorial, we focus on this
question in the Boolean setting: given a relation between Boolean inputs and outputs as
the specification, the Boolean functional synthesis problem asks to synthesize each
output as a function of the inputs such that the specification is met.

We
start by showing the centrality of this problem via multiple examples and applications
in a variety of domains ranging from program synthesis to planning. We then look at
theoretical hardness results and survey some of the algorithmic techniques that have
been developed in recent years to tackle this problem, remarking on their surprising
practical performance. This leads us to examine the structure of specification in more
depth and doing so we develop a theory of knowledge representations and new algorithmic
directions. We end with several open questions and avenues for future work.

## Tatiana Starikovskaya: Regular Expression Search in a Stream

Regular expression search is a key primitive in myriads of applications, from web scraping to bioinformatics. A regular expression is a formalism for compactly describing a set of strings, built recursively from single characters using three operators: concatenation, union, and Kleene star. Two basic algorithmic problems concerning such expressions are membership and pattern matching. In the regular expression membership problem, we are given a regular expression R and a string T, and must decide whether T matches R. In the regular expression pattern matching problem, the task is to find the substrings of T that match R. In this talk, I will give a survey of recent algorithms for regular expression search in the practically relevant streaming setting.

**Databases, Streaming, Transducers**(Amphitheatre 2A)

## Ismaël Jecker: A Rational and Complete Notion of Delay for Streaming String Transducers

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

## Gaëtan Staquet: Active Learning of Automata for JSON-Streaming Validation

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.

## Mikołaj Bojańczyk: Folding Transducers

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.

## Adrien Boiret: Symbolic Register Tree Transducers with Symbolic Register Lookahead

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.

## Victor Marsault: Simple-Run Semantics for RPQs

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.

## Anthony Widjaja Lin: Data Path Queries over Embedded Graph Databases

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

## Albert Gutowski: Finite Entailment of UCRPQs over ALC Ontologies

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.

## Sarah Kleest-Meißner: Discovering Event Queries from Traces: Laying Foundations for Subsequence-Queries with Wildcards and Gap-Size Constraints

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.

## Joachim Niehren: Schema-Based Automata Determinization

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.

**[Online talk]** Dhruv Nevatia:
Register
Systems Through the Lens of Logic

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.

**[Online talk]** Sahil Mhaskar:
Checking Regular Invariance under Tightly-Controlled
String Modifications

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.

**Verification**(Amphitheatre 6C)

## Pascal Bergsträßer: Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification

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

## Clément Tamines: Pareto-Rational Verification

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.

## Nicolas Waldburger: Parameterized Verification of Round-Based Shared-Memory Systems

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.

## Chana Weil-Kennedy: Parameterized Analysis of Reconfigurable Broadcast Networks

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

## A. R. Balasubramanian: Complexity of Coverability in Bounded Path Broadcast Networks

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.

## Corto Mascle: Avoiding Deadlocks in Lock-Sharing Systems

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.

## Muhammad Usama Sardar: Understanding Trust Assumptions for Remote Attestation via Formal Verification

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.

## Benjamin Lucien Kaminski: Quantitative Strongest Post

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

## Wojtek Jamroga: A Survey of Requirements for COVID-19 Mitigation Strategies

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)

**Skolem Problem**(Amphitheatre 2A)

## Joris Nieuwveld: Progress on the Skolem Problem

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.

## George Kenison: On the Skolem Problem for Reversible Sequences

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.

## Arka Ghosh: Orbit-Finite Systems of Linear Equations

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.

## James Worrell: The Pseudo-Reachability Problem for Linear Dynamical Systems

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

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.

## Isa Vialard: On the Cartesian Product of Well-Orderings

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.

## Edon Kelmendi: Computing the Density of the Positivity Set for Linear Recurrence Sequences

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.

## Klara Nosan: The Membership Problem for Hypergeometric Sequences with Rational Parameters

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

## Nikhil Balaji: Identity Testing for Radical Expressions

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

**Games I**(Amphitheatre 6C)

## Antonio Casares: On the Size of Good-for-games Rabin Automata and its Link with the Memory in Muller Games

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.

## Pierre Ohlmann: Well-Ordered Monotonic Universal Graphs for Half Positionality

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.

## Pierre Vandenhove: Half-Positional Deterministic Büchi Automata

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.

## Alexandre Terefenko: Multi-Player Attack Trees

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.

## Marie Van Den Bogaard: On the Complexity of SPEs in Parity Games

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.

## Jędrzej Kołodziejski: Countdown Mu-Calculus, Automata and Games

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.

## Guy Avni: Computing Threshold Budgets in Discrete-Bidding Games

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.

## Dylan Bellier: Dependency Matrices: Multi-player Delay Games

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.

## Léonard Brice: The Complexity of SPEs in Mean-Payoff Games

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.

**[Online talk]** Alexander Kozachinskiy:
State Complexity of Chromatic Memory in
Infinite-duration Games

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 will provide snacks, but welcome participants to bring drinks and extra food to share.

## Markus Lohrey: Straight-Line Programs: From Compression to Algorithmics

A straight-line program is a context-free grammar that produces exactly one word. The length of this word can be exponentially smaller (in the best case) than the size of the straight-line program. This is the underlying idea of grammar-based compression, where straight-line programs are used for the compression of strings. Compressors that exploit this idea are for instance LZ77, RePair, BiSection, and Sequitur. After introducing straight-line programs and grammar-based compression I will explore recent algorithmic applications of straight-line programs in stringology, group theory, and algebraic complexity theory. If time permits I will also talk about an extension to trees. Straight-line programs for trees have found applications in information theory and parallel algorithms.

**Pushdown Automata, Grammars, and Variants**(Amphitheatre 2A)

## Dorota Celińska-Kopczyńska: Generating Tree Structures for Hyperbolic Tessellations

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.

## Kyveli Doveri: Antichains Algorithms for the Inclusion Problem Between ω-VPL

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.

## K. S. Thejaswini: Adaptive Synchronisation of Pushdown Automata

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

## Guillaume Maurras: A Robust Class of Languages of 2-Nested Words

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.

## Chris Köcher: Verifying Multi-Pushdown Automata

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.

## Stefan Hoffmann: Directable and Synchronizable Parikh Automata

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.

## Asaf Yeshurun: Determinization of One-Counter Nets

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.

**[Online talk]** Guanyan Li:
Probabilistic Verification Beyond Context-Freeness:
An Extended Abstract

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.

**[Online talk]** Martin Zimmermann:
On Parikh Automata: Infinite Words, Games, and
History-determinism

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.

**[Online talk]** Soumodev Mal:
On the Satisfiability of Context-free String
Constraints with Subword Order

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.

**Synthesis**(Amphitheatre 6C)

## Shaun Azzopardi: How to Synthesize when your Environment is a Program

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.

## Priyanka Golia: Program Synthesis as Dependency Quantified Formula Modulo Theory

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.

## Sasha Rubin: Stochastic Best-Effort Synthesis

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.

## Sophie Pinchinat: Formula Synthesis in Propositional Dynamic Logic with Shuffle

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.

## Mathieu Lehaut: Distributed Synthesis of First Order Specifications for Agents with Partial Information

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.

## Hugo Gimbert: Distributed Asynchronous Games With Causal Memory are Undecidable

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.

## Michaël Cadilhac: Implementing Automata Algorithms: Low-Level Parallelism in Modern CPUs

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.

## Marta Kwiatkowska: Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges

Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Much of existing research has focused on turn-based games, where each state of the game is controlled by a single player. This lecture will provide an overview of recent advances concerning automated verification and strategy synthesis for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. This will include zero-sum as well as equilibria-based temporal logic properties (for Nash and correlated equilibria) and two optimality criteria, social welfare and social fairness. The lecture will also discuss future challenges in this area, including the recent development of neuro-symbolic concurrent stochastic games (NS-CSGs), whose agents are endowed with perception implemented using neural networks.

**Games II**(Amphitheatre 2A)

## Benjamin Bordais: From Local to Global Determinacy in Concurrent Graph Games

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

## Alexandros Evangelidis: On the Performance Evaluation of Algorithms for Stochastic Games

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.

## Muqsit Azeem: Optimistic and Topological Value Iteration for Simple Stochastic Games

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

## Nathan Thomasset: Finite-Memory Strategies for Games in Two-Player Games

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

## Federica Adobbati: A Two-Player Asynchronous Game on Petri Nets with Partial Observability

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.

## James C. A. Main: Different Strokes in Randomised Strategies: Revisiting Kuhn's Theorem Under Finite-Memory Assumptions

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.

**Vector Addition Systems**(Amphitheatre 6C)

## Georg Zetzsche: The Complexity of Bidirected Reachability in Valence Systems

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

## Moses Ganardi: Reachability in Bidirected Pushdown VASS

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.

## Piotr Hofman: Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable

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.

## Pascal Baumann: Regular Separability in Büchi Vector Addition Systems

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.

## Henry Sinclair-Banks: Coverability in 2-VASS with One Unary Counter

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.

## David Purser: The Boundedness and Zero Isolation Problems for Weighted Automata over Nonnegative Rationals

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.

**[Online talk]** Wojciech Czerwiński:
Lower Bounds for the Reachability
Problem in Fixed Dimensional VASSes

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.

## Dexter Kozen: 25 Years of KAT

Kleene algegra with tests (KAT) is a system for equational reasoning about imperative programs. The system is based on Kleene algebra, the algebra of regular expressions. In this talk I will trace the origins of the system and survey past and recent results on expressiveness, decision complexity, and deductive completeness, along with various applications, including correctness of compiler optimizations and verification of packet switching networks.

**Automata, Algebra, Logic**(Amphitheatre 2A)

## Arthur Jaquard: A Complexity Approach to Tree Algebras: the Exponential Case

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.

## Bharat Adsul: Block Product Decompositions over Countable Words for First Order Logic and its Infinitary Quantifier Extensions

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.

## Uli Fahrenberg: Languages of Higher-Dimensional Automata

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

## Chase Ford: Graded Monads and Behavioural Equivalence Games

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.

## Corentin Barloy: The Regular Languages of First-Order Logic with One Alternation

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.

## Rémi Morvan: First-order Separation over Countable Scattered Linear Orders

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.

## Leon Bohn: Passive Learning of Deterministic Büchi Automata by Combinations of DFAs

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.

## Thomas Colcombet: Uniformization of MSO over Countable Ordinals

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

## Christopher Hugenroth: Extension Acceptance and Regular ω-Languages

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.

## Michał Skrzypczak: Computing Measure of Regular Languages of Infinite 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.

**[Online talk]** Ramanathan S. Thinniyam:
Existential Definability over the Subword
Ordering

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.

**Temporal Logics**(Amphitheatre 6C)

## Laura Nenzi: Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes

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.

## Giuseppe Perelli: Timed Trace Alignment with Metric Temporal Logic over Finite Traces

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.

## Ennio Visconti: Online Monitoring of Spatio-Temporal Properties for Imprecise Signals

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.

## Jonni Virtema: Temporal Team Semantics Revisited

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.

## Ritam Raha: Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic

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.

## Léo Tible: Fairness and Promptness for Muller Formulas

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.

## Anissa Kheireddine: Model Checking in Calm Waters with BSaLTic

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

## Jan Kretinsky: LTL-Constrained Steady-State Policy Synthesis

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: A Decision Diagram Operation for Reachability

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.

## Kush Grover: Planning Via Model Checking with Decision-Tree Controllers

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.

**[Online talk]** Nathanael Fijalkow:
Learning Linear
Temporal Logic formulas from Examples

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**(Amphitheatre 2A)

## Shibashis Guha: PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

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.

## Jakob Piribauer: Tradeoffs Between Expectation and Variance in Weighted Markov Decision Processes

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.

## Théo Matricon: Markov Decision Processes meet Abstraction Refinement

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.

## Tansholpan Zhanabekova: Deciding What is Good-for-MDPs

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.

**[Online talk]** Dominik Wojtczak:
Model-Free Reinforcement Learning for
Lexicographic ω-Regular Objectives

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

**Graphs**(Amphitheatre 6C)

## Jakub Gajarský: Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

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.

## Sandra Kiefer: Treelike Decompositions for Transductions of Sparse Graphs

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.

## Szymon Toruńczyk: Ordered Graphs of Bounded Twin-Width

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.

## Lars Jaffke: A Logic-Based Algorithmic Meta-Theorem for Mim-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.

## Mikaël Monet: (Weighted) Counting of Matchings in Graph Families of Unbounded Treewidth

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.

**[Online talk]** Wojciech Przybyszewski:
Distal Combinatorial Tools
for Graphs of Bounded Twin-Width

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.

## Experimental Session on Research Tools and Practices

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

#### Discussion Session on the Climate Crisis and the Future of Highlights

This year, we had a discussion about the ongoing climate crisis, the role of Highlights in this crisis, how to adjust the organization of the conference for future editions, and how to change the model of academic conferences more broadly.

The slides of the introduction are here. Here are some key facts (the figures do not coincide with the values in the slide because the methodology has changed):

- Highlights has signed the TCS4F manifesto to commit to reducing its carbon footprint.
- The overall footprint of Highlights'22 is 42 tons of CO2e, for 173 registered participants in total. The code used to compute this is available and open-source.
- Highlights is co-located with ICALP 2022 to encourage participants to attend both conferences and limit travel. There were 37 participants of Highlights who were also attending ICALP.
- Highlights proposed the Highlights Extended Stay Support Scheme (HESSS) to encourage participants to extend their stay with a visit in a neighboring lab, similarly to the analogous mechanism for ICALP. There were 12 teams or labs listed. There were 6 foreign researchers who took part to such a scheme, and more broadly 24 researchers who extended their stay for professional reasons.

#### Experimental Session on Research Tools and Practices

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

The experimental session welcomed 8 talks:

- Michaël Cadilhac, latexmk and the subfile packages
- Michał Skrzypczak, The Beamerikz package
- Mikołaj Bojańczyk, Slajdomat
- Aliaume Lopez, The knowledge package
- Rémi Morvan, knowledge-clustering
- Mikaël Monet, The CStheory Q&A website (asked question)
- Alexandre Duret-Lutz, The importance of mentioning version numbers in papers
- Nguyễn Lê Thành Dũng (Tito), Pledges and other collective initiatives

#### Highlights Code of Conduct

Highlights is committed to be a respectful forum for its participants, free from any discrimination or harassment of any nature, particularly when abuse of power is involved. All Highlights attendees are expected to behave accordingly.

If you experience or witness discrimination, harassment or other unethical behavior at the conference, we encourage you to seek advice and remedy by consulting with the SafeToC counsellor of Highlights: Daniela Petrisan <petrisan @irif.fr>.

The local organizers are entitled to remove registered participants from the conference (without refunding the conference fees) if they are deemed to pose an ethical risk to other participants.#### Committees

- C. Aiswarya (India)
- Udi Boker (Israel)
- Véronique Bruyère (Belgium)
- Dmitry Chistikov (UK)
- Claire David (France)
- Dietrich Kuske (Germany)
- Karoliina Lehtinen (France)
- Sebastian Maneth (Germany)
- Kai Salomaa (Canada)
- Alexandra Silva (US)
- Michał Skrzypczack (Poland)
- Sophie Tison (chair)
- Szymon Torunczyk (Poland)
- Thomas Zeume (Germany)

- Quentin Aristote
- Dung Bui
- Sam van Gool
- Lucie Guillou
- Anatole Leterrier
- Aliaume Lopez
- Maël Luce
- Vincent Moreau
- Klara Nosan
- Soumyajit Paul
- Jakub Różycki
- Daniel Szabo
- Weiqiang Yu