Publications
-
WinPop: Making populations win together
In repeated games, players choose actions concurrently at each step. We consider a parameterized setting of repeated games in which the players form a population of an arbitrary size. Their utility functions encode a reachability objective. The problem is whether there exists a uniform controller strategy that ensures the population reaches the target almost surely. -
Optimal sequential flows
We provide a new algebraic technique to solve the sequential flow problem in polynomial space. The task is to maximize the flow through a graph where edge capacities can be changed over time by choosing a sequence of capacity labelings from a given finite set. -
Optimally controlling a random population
The population control problem is a parameterized control problem where a population of agents has to be moved simultaneously into a target state. The decision problem asks whether this can be achieved for a finite but arbitrarily large population. We focus on the random version of this problem, where each agent is a copy of the same automaton and the controller chooses a global action at each step. -
Population Protocols over Ordered Agents
Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according to a fixed transition function. The computation is defined by the eventual stabilization of the population to a consensus that represents the result of the computation. -
Computing the downward-closure of an indexed language
By the well-known Higman’s lemma, the downward closure of a language is regular. This makes the downward closure a fundamental abstraction: it is a regular over-approximation that preserves information about pattern occurrences and unboundedness. We study the complexity of computing downward closures of indexed languages and give upper and lower bounds for deterministic and nondeterministic automata. -
The trichotomy of regular property testing
Property testing is concerned with the design of algorithms making a sub-linear number of queries to distinguish whether the input satisfies a given property or is far from having this property. We study property testing of formal languages and establish a trichotomy that classifies the complexity of the problem for regular properties. -
On the Minimisation of Deterministic and History-Deterministic Generalised (co)Büchi Automata
We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBüchi automata. On the other hand, we establish that the minimisation problem for deterministic generalised Büchi automata is intractable in general. -
The Complexity of Simplifying ω-Automata through the Alternating Cycle Decomposition
In 2021, Casares, Colcombet and Fijalkow introduced the Alternating Cycle Decomposition (ACD), a structure used to define optimal transformations of Muller automata into parity automata and to obtain theoretical results about relabelling acceptance conditions. We study the complexity of computing the ACD and its DAG-version. -
Verification of Population Protocols with Unordered Data
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration satisfies a given property, and we study the verification problem for population protocols with unordered data. -
Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability
We consider the parameterized verification of networks of agents which communicate through unreliable broadcasts. In this model, agents have local registers whose values are unordered and initially distinct, and can compare or store received values. We study the complexity and decidability frontier of this model. -
Model-checking parametric lock-sharing systems against regular constraints
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. We consider infinite behaviours under process fairness, and study the problem of deciding whether some regular property holds for all runs of such a system. -
Distributed controller synthesis for deadlock avoidance.
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction, this problem is undecidable even for three processes each using a fixed number of locks; we propose two restrictions making it decidable. -
Keyboards as a New Model of Computation.
We introduce a new formalisation of language computation, called keyboards. We consider a set of atomic operations such as writing, erasing, and moving the cursor, and define a keyboard as a set of finite sequences of such operations. The generated language is the set of words obtained by applying some non-empty sequence of keys. -
Responsibility and verification: Importance value in temporal logics.
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a component is. -
From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics.
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical systems by observing run prefixes. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic properties. We move from LTL to robust LTL (rLTL), which improves monitorability by allowing a signal to be considered sufficiently close to satisfaction or violation. -
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas.
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information-flow policies by relating multiple traces of a security-critical system. We study the satisfiability problem and identify two sources of decidability: small models and very simple formulas. -
On Finite Monoids over Nonnegative Integer Matrices and Short Killing Words.
Let n be a natural number and M a set of n × n-matrices over the nonnegative integers such that M generates a finite multiplicative monoid. We show that if the zero matrix is a product of matrices in M, then there are matrices in M whose product is zero. This result has applications in automata theory and in the theory of codes.
PhD thesis
-
Verification and Synthesis of Distributed Systems with Weak Synchronisation
Distributed programs are a cause of difficulty for formal methods. The interactions of multiple components lead to a combinatorial explosion, which complicates verification. In the context of controller synthesis, this is further compounded by the fact that the environment may have to resolve choices without global information.
Unpublished work
-
Distributed synthesis, well-quasi-orders and memory for games
We study distributed synthesis in the case of asynchronous processes communicating using locks and shared variables. The goal is to compute a local strategy for each process that together ensure a global safety objective. So processes must base their decisions exclusively on their local history. While the problem is undecidable in general, we show that we regain decidability when we impose that executions of the system are divided into a bounded number of phases, and the flow of information between processes during a phase is acyclic. To obtain our result, we rely on well-quasi-orders and on the novel concept of two-player games with objective-independent memory. We show a result of independent interest about such games, namely that for every well-quasi-order with effectively regular upward-closed sets, the class of upward-closed safety objectives has objective-independent memory. -
Simulation and bisimulation of gap-constraint systems
We investigate the simulation and bisimulation problems for gap-order constraint systems (GCS), an abstraction of counter systems that allows zero-tests but loosens counter increments and decrements. Our main result is positive: we show that simulation is decidable, and EXPTIME-complete, for those systems. The upper bound is obtained through a series of reductions leading to a special case of a model of quantitative games called games with guess actions, introduced by Colcombet and Göller in 2016. The lower bound already holds for simulation between GCS and finite-state systems. We contrast this with an undecidability proof for the bisimulation problem between GCS. -
Learning temporal formulas from examples is hard
We study the problem of learning linear temporal logic formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is understandable for humans. We initiate the study of the computational complexity of the learning problem.
