ABSTRACT. Suppose we have a deterministic finite-state transducer A and an infinite word x, and run A on x to obtain an infinite word A(x). Which properties of x are guaranteed to also hold for A(x)? In this talk, we consider this preservation question for various well-known classes of words having desirable combinatorial properties, e.g., recurrent words, primitive morphic words, and words that admit factor frequencies. The celebrated Krohn-Rhodes theorem provides the framework for proving our preservation results, and our techniques are based on the ergodic theory of symbolic dynamical systems, i.e., shift spaces. This talk is based on joint work with Valérie Berthé, Herman Goulet-Ouellet, Toghrul Karimov, and Dominique Perrin.

ABSTRACT. Transducers generalise automata by producing output word(s) for each input word, thereby defining a relation over words. A transducer is said to be finite-valued if, for every input word, it produces at most k output words, for some constant k. If k=1, then the transducer is said to be functional. The edit distance between two transducers is the minimal number of edits required to transform every output of one transducer into some output of the other, for each input word. This notion has been studied for functional transducers, where it is shown to be computable. However, it is uncomputable for transducers in general. In this work, we show the computability of the edit distance of finite-valued transducers, a class that is strictly more expressive than functional transducers.

This is a joint work with Dr. Prince Mathew (ULB), and has been accepted to ICALP 2026. The full version of the paper is available on arXiv: https://arxiv.org/pdf/2605.06269

ABSTRACT. We study bounded deviation of non-deterministic finite transducers under the Hamming distance: the bounded comparison problem asks, given two transducers and k in N, whether for every input the two transducers produce words at Hamming distance at most k. This problem is known to be decidable in polynomial time when k is fixed, and in co-NP otherwise. We show that the problem is NL-complete when k is fixed, co-NP-complete when k is given in binary, and it is DP-complete to decide if the distance is exactly k. We also prove that if the two transducers have bounded comparison, then the maximal distance is at most quadratic in the size of both transducers, and that this bound is asymptotically tight. We prove the results on deviations problem, which asks similar questions on the distance of the pairs of input and output of a single transducer, and show that these two families of problems are logspace many-one equivalent.

This research work was done in collaboration with Luc Dartois, Ismaël Jecker, and Pierre-cyrille Héam. It as been submitted to MFCS 2026.

Arxiv version: https://arxiv.org/abs/2604.25398

ABSTRACT. We generalize an efficient automata-based approach to string solving, the stabilization-based method behind the solver Z3-Noodler, to support relational constraints represented by finite-state transducers (useful for modeling replaceAll constraints, etc.). We focus on efficient handling of length constraints by reducing the need for expensive concatenation elimination, a major bottleneck in automata-based string solving. We also propose heuristics that significantly improve performance in practice. Implemented on top of Z3-Noodler, our method clearly outperforms other solvers on benchmarks with relational constraints: it solves more instances and runs orders of magnitude faster.

ABSTRACT. We seek an equational theory for string-to-string regular functions: a formal system in which every equivalence between two such functions can be derived from a finite set of simple axioms, in the spirit of the equational theory of regular languages [Salomaa, JACM'66 and Kozen, IC'94].

The formalism we work with is that of list functions [Bojańczyk, Daviaud and Krishna, LICS'18], which operate on structured objects built from disjoint sums, products, and the list constructor over a finite set. Under a standard encoding of input structures as strings, list functions capture exactly string-to-string MSO transductions, making them a convenient algebraic formalism for string-to-string regular functions. As a consequence of this correspondence, equivalence of list functions is decidable, following from the decidability of equivalence for string-to-string MSO transductions [Gurari, SICOMP'82].

However, existing decidability proofs have two significant shortcomings: (1) they proceed by reduction to results about other models, providing little insight into the structure of these functions; and (2) they do not appear to extend to established generalisations such as the polyregular functions [Bojańczyk, LICS'22], for which decidable equivalence remains open.

Jointly with Mikołaj Bojańczyk, Kacper Lewandowski and Antoni Puch, we are currently working towards such an equational theory, which would also address the shortcomings above, yielding an equivalence procedure intrinsic to the model rather than relying on reductions, and might provide a path towards decidable equivalence for polyregular functions. In this presentation, I will report on work in progress: the current state of our approach, the main tools we employ, and the remaining obstacles toward a sound and complete equational theory.

ABSTRACT. A membership problem asks, given a property expressed in a formalism F , whether such a property can be expressed in a strictly less expressive (or in- comparable) formalism F'. Research on membership problems dates back to the 1960s in language theory, finding one of its first seminal result in the Schutzenberger’s theorem, which shows that it is decidable if a given regular lan- guage of finite words is star-free (or, equivalently, first order definable). While the study of membership problems has yielded elegant results for languages of finite and infinite words, the corresponding problems for tree languages stand among the most challenging in language theory. Furthermore, when focusing specifically on logical formalisms defining ω-regular tree languages, results are even more sparse. In 1970, Rabin established a breakthrough connection between definability of ω-regular tree languages in weak MSO (where monadic second order quantifica- tion ranges only over finite sets) and recognizability by nondeterministic B¨uchi tree automata [6]. This correspondence was later extended to weak alternating automata [5]. By virtue of these results, the membership problem asking if an MSO definable ω-regular tree language is also definable in weak MSO is reducible to the problem of deciding if a language recognized by a parity automaton is also recognizable by a weak automaton. While there is no clear approach for solving the former problem directly, the latter has seen significant progress in recent years [2][1][4]. Rabin’s theorem is therefore crucial: it enables the reduction of an elusive membership problem in logic to a more tractable problem in automata theory. In this work, we present Rabin-like theorems for two well-known fragments of MSO, namely Monadic Chain Logic (MCL) and Monadic Path Logic (MPL) [7], in which monadic second order quantification is limited to range only over, respectively, sets of mutually comparable nodes of a tree and branches of a tree. We show that, interestingly, decidability of the above mentioned automata-theoretic problem does not imply decidability of the membership problem from MCL (resp., MPL) to Weak MCL (resp., Weak MPL). Hence, we identify logics for which a Rabin-like the- orem is instead possible. We show that indeed the membership problem from MCL to Loop PDL, an extension of the well-known PDL introduced in 1978 [3], can be reduced to the membership problem from parity to weak automata. Moreover, the same holds for the one from MPL to the extension of CTL with past temporal operators, even though this result is currently conditional to the truth of a conjecture regarding the expressive power of a certain automata class. This line of re- search has yielded several other notable results, most significantly the decidability of the membership problem from LTL to CTL with past. Crucially, this result provides a novel approach to tackling a 40-year-old open problem: deciding the common fragment of LTL and CTL.

This is joint work with M. Benerecetti, D. Della Monica, F. Mogavero and G. Puppis.

References

[1] Thomas Colcombet, Denis Kuperberg, Christof L¨oding, and Michael Van- den Boom. Deciding the weak definability of Buchi definable tree languages. In CSL, 2013. [2] Thomas Colcombet and Christof Loding. The non-deterministic Mostowski hierarchy and distance-parity automata. In International Colloquium on Automata, Languages, and Programming, pages 398–409. Springer, 2008. [3] David Harel and Vaughan R Pratt. Nondeterminism in logics of programs. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 203–213, 1978. [4] Olivier Idir and Karoliina Lehtinen. Using games and universal trees to characterise the nondeterministic index of tree languages. arXiv preprint arXiv:2504.16819, 2025. [5] David E Muller, Ahmed Saoudi, and Paul E Schupp. Alternating automata, the weak monadic theory of the tree, and its complexity. In International Colloquium on Automata, Languages, and Programming, pages 275–283. Springer, 1986. [6] Michael O Rabin. Weakly definable relations and special automata. In Studies in Logic and the Foundations of Mathematics, volume 59, pages 1– 23. Elsevier, 1970. [7] Wolfgang Thomas. Logical aspects in the study of tree languages. In Proc. of the Conference on Ninth Colloquium on Trees in Algebra and Programming, page 31–49, USA, 1984. Cambridge University Press.

ABSTRACT. Verification of a program (modelled as trees) can be captured game-theoretically as an acceptance game between Verifier and Falsifier. The existence of a winning strategy for Verifier then corresponds to the existence of an accepted run-tree of a given automaton over a model. However, traditional acceptance game are strictly Boolean. By treating near-misses and total failures identically, this rigid pass/fail approach obscures how close a program is to satisfying the property. To address this, we propose a quantitative version of this game that liberates from rigid acceptance to a framework allowing for a measurable defect.

In this paper, we draw inspiration from how bisimulation distance is an extension of bisimilarity to define our quantitative acceptance game, called epsilon-acceptance game. This game configuration consists of an automaton, a program, and a measurable defect budget, called epsilon. The addition of this budget to the game is to compensate for parts of the program that do not perfectly meet the property. Our main result establishes that a program T is accepted with a budget of epsilon iff there exists a traditionally accepted version of that program T' that is at a bisimulation distance of at most epsilon from T.

We further show that this framework makes a strong connection to probability measures on trees, which we illustrate by applying our game to evaluate program failure. In particular, our framework is defined over binary trees with leaves and infinite branches where the winning budget establishes an upper bound on the probabilistic measure of the set of rejected branches.

ABSTRACT. In this work, we study infinite equational systems, built from operations of potentially infinite arity. We restrict ourselves to systems that have the structural property of being ultimately-cyclic: when iteratively following the dependency relation between variables, either this terminates, or a cycle is eventually built. We show that such equational systems are subject to a Bekić-like theorem : these systems can be solved by inductively solving systems of dimension one and nesting them coherently. We further develop the algebraic theory of these ultimately-cyclic systems. Our aim is to use it in the development of a theory of regular languages of infinite trees. This is a joint work with Thomas Colcombet and Daniela Petrisan.

ABSTRACT. We study games on finite graphs with labelled or weighted edges in which plays end as soon as the first loop is formed. We consider two semantics for such games, where the winner depends on the value of either the loop or the entire play (lasso). We show that adopting lasso semantics may have a dramatic impact on both the complexity of the game and the memory required to play optimally. Mean-payoff games with lasso semantics are no longer positionally determined, and solving such games is PSPACE-complete. In contrast, parity games with lasso semantics are equivalent to weak parity games, remaining positionally determined and solvable in polynomial time. Furthermore, we show that if a positionally determined winning objective is closed under concatenation and cyclic permutations, it is essentially equivalent to the parity objective. Finally, we consider mod-$k$ games where the winner depends on the length of the path modulo $k \geq 2$, and show that these games, under both semantics, are PSPACE-complete. Alongside the complexity of solving these games, we analyze the memory required to play optimally. We establish that for any objective positionally determined in loop semantics, a memory of size $2^n$ is sufficient in lasso semantics. We demonstrate that this exponential bound is tight in certain cases: for both lasso mean-payoff games and mod-$k$ games, the winning player may require exponential memory.

ABSTRACT. Given a letter-to-letter deterministic transducer over an alphabet of size d, one can construct a corresponding 1-Lipschitz function on d-adic integers, which admits a unique expansion as a Van der Put series, with reduced coefficients. Grigorchuk and Savchuk showed that the reduced sequence of coefficients is d-automatic, and that the Moore automaton can effectively be built directly from the transducer.

In this work, we propose a new algorithm for computing the Moore automaton, as new ground to improve in two ways the results of Grigorchuk and Savchuk. Firstly, we show that it is possible to do the reverse construction, ie. build a transducer out of a Moore automaton, and secondly, that these constructions extend to (non-necessarily letter-to-letter) functional deterministic transducers.

This work was made in collaboration with Matthieu Picantin and Olivier Carton.

ABSTRACT. The Orbit Problem asks whether the orbit of a point under a matrix reaches a given target set. When the target is a single point, the problem was shown to be decidable in polynomial time by Kannan and Lipton. This decidability result was later extended by Chonev et al. to targets of dimension 3 (in arbitrary ambient dimension), but decidability remains open for subspaces of dimension 4. At the other extreme, the special case of the Orbit Problem in which the target set is a hyperplane of co-dimension 1 is equivalent to the Skolem Problem for linear recurrence sequences, whose decidability has been open for many decades.

The Subspace Orbit Problem thus has two important parameters: the dimension of the target subspace and the dimension of the orbit itself. We characterise decidability and complexity of the problem from this perspective. We show that the Subspace Orbit Problem is decidable if the target subspace has dimension logarithmic in the dimension of the orbit. Over the rationals, we moreover obtain a complexity bound NP^RP in this case, when the target space dimension is bounded. On the other hand, we show that the version of the Subspace Orbit Problem where the dimension of the target subspace is linear in the dimension of the orbit is as hard as the Skolem Problem.

This joint work with Piotr Bacik has been accepted for publication at LICS 2026.

ABSTRACT. The Kannan-Lipton Orbit Problem asks whether the orbit of a point under repeated multiplication by a matrix ever hits a target subspace. The Orbit Problem subsumes the Skolem Problem, which asks whether a given linear recurrence sequence has a zero term. However, despite being studied for over 90 years, decidability of the Skolem Problem (and hence, the Orbit Problem) remains stubbornly open.

Though the full problem is currently out of reach, several breakthroughs have been made by restricting the dimension of the orbit (denoted d), and the dimension of the target subspace (denoted t). In 2013, Chonev, Ouaknine and Worrell showed the Orbit Problem is decidable whenever t is at most 3. In 2026, my coauthor Anton Varonka and I showed that the problem is decidable whenever t < 2log_3(d).

In the present talk, I will discuss a further improvement that may be made assuming a conjecture in transcendence theory. In particular, that assuming the p-adic Schanuel Conjecture, the Orbit Problem is decidable whenever t < d^{2/3}.

ABSTRACT. XNFAs (also known as XOR-NFAs or symmetric-difference NFAs) are a variant of standard finite automata in which an input word is accepted iff the number of accepting runs is odd. Equivalently, these are weighted automata over the field of two elements, whereas the more familiar nondeterministic finite automata (NFAs) are weighted automata over the Boolean semiring. Much like NFAs, XNFAs recognise exactly the class of regular languages and are exponentially more succinct than DFAs. Unlike NFAs, XNFAs admit efficient complementation and minimisation.

Given an automaton A and a word w, the acceptance problem asks whether A accepts w. In this talk, we compare the acceptance problem for XNFAs and NFAs in a fine-grained manner, focusing on optimising the degrees of polynomials in the running-time bounds. We first refine the upper bounds for the acceptance problem for XNFAs and NFAs of bounded ambiguity (e.g., unambiguous automata). We then show that, under the assumption of polynomial ambiguity, NFA acceptance reduces to XNFA acceptance. This is joint work with Dmitry Chistikov, Radoslaw Piorkowski and Brink van der Merwe.

ABSTRACT. Loop invariants are properties that hold before and after each iteration of a program loop, and they play a central role in program verification by ensuring the correctness of algorithms throughout execution. In this talk, I focus on polynomial loops, where loop assignments are given by polynomial maps. While computing polynomial invariants for general loops is undecidable, efficient methods exist for certain restricted classes of loops such as solvable loops. I consider a more general setting in which the loop assignments may involve arbitrary polynomials. Using tools from algebraic geometry, I present two algorithms for generating all polynomial invariants of a polynomial loop up to a specific degree. These algorithms differ depending on whether the initial values of the loop variables are fixed or treated as parameters.

This work is joint work with Fatemeh Mohammadi and Rémi Prebet

ABSTRACT. We introduce the class of non-negative residual functions from strings to rationals. A function is called non-negative residual if the cone generated by the rows of its Hankel matrix is finitely generated. We show that this class is well behaved: it is closed under reversal, admits minimal representatives, is efficiently learnable, and has decidable non-negativity and positivity problems. Finally, we provide a decision procedure for determining whether a function computed by a unary weighted finite automaton is non-negative residual. This problem is equivalent to deciding whether a given linear recursive sequence can be realised by a linear recurrence relation with non-negative coefficients.

This is a joint work with Arthur Gall, Nathanael Fijalkow, Remi Morvan and Antoni Wisnewski.

ABSTRACT. We present a parallel abstract interpretation technique for polynomial programs with assertions presented as unions of range bound constraints. We use the powerset domain of hyper-rectangles to overapproximate sets of reachable states. Our key technical contributions include novel abstract transformers and refinement operators that account for the semantics of polynomial assignments and guards more precisely than earlier work, while remaining amenable to parallelization and efficient implementation. This is achieved by appealing to Farkas' Lemma and Handelman's Theorem, and by exploiting geometric properties of unions of hyper-rectangles. Our abstract interpretation technique proves safety properties of many polynomial programs that state-of-the-art abstract interpretation tools fail to prove. We have implemented our approach in a tool called PolyAbs, and experimentally evaluated it on a suite of benchmarks. Our experiments demonstrate the improved precision and broader coverage of PolyAbs vis-a-vis state-of-the-art abstract interpretation tools, including a commercial-grade tool.

This paper is accepted and will be presented at CAV'26.

ABSTRACT. We consider linear single-path loops of the form

while phi do x <- A * x + b end

where x is a vector of variables, the loop guard phi is a conjunction of linear inequations over the variables x, and the update of the loop is represented by the matrix A and the vector b. It is already known that termination of such loops is decidable. In this work, we consider loops where A has real eigenvalues, and prove that it is decidable whether the loop's runtime (for all inputs) is bounded by a constant if the variables range over reals or rationals. This is an important problem in automatic program verification, since safety of linear while-programs is decidable if all loops have constant runtime, and it is closely connected to the existence of multiphase-linear ranking functions, which are often used for termination and complexity analysis. To evaluate its practical applicability, we also present an implementation of our decision procedure.

This is joint work with Florian Frohn, Jürgen Giesl, and Peter Giesl that appeared at TACAS '26.

ABSTRACT. I will present joint work with Kevin Batz (Cornell University), Joost-Pieter Katoen (RWTH Aachen) and Tobias Winkler (RWTH Aachen). We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) continuous distributions, and (iii) conditioning. To handle loops we rely on user-provided quantitative invariants, as is well established. However, in the realm of continuous distributions, invariant verification becomes extremely challenging due to the presence of integrals in expectation-based program semantics. Our key idea is to soundly under- or over-approximate these integrals via Riemann sums. We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove convergence of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting discrete probabilistic programs for the verification of programs involving continuous sampling. Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.

ABSTRACT. Inexpressibility results are among the most natural questions in automata theory. They are also often some of the most difficult. One of the few reliable tools for proving them are pumping lemmas, but most models are too complex to admit any version of them. We propose a new tool for such proofs, called Pumping Sequence Families. In my talk I will explain this concept and, to showcase it, prove a pumping sequence family lemma for regular languages that lets one separate them from context free grammars. I will also state a pumping sequence family lemma for Copyless Cost Register Automata, a model with no known pumping lemma, which allows for separation between this model and Polynomially Ambiguous Weighted Automata. Based on joint work with Filip Mazowiecki and Daniel Smertnig.

ABSTRACT. This talk considers decision problems related to finite monoids of rational matrices. We show that determining finiteness of a given monoid is in PSPACE, improving the known co-NEXP^NP upper bound. We also show that the membership problem for finite matrix monoids is PSPACE-complete, improving the known NEXP-upper bound. Our two complexity results are corollaries of a new polynomial bit-size bound on matrix entries in finite monoids. Our techniques also give us a polynomial-time algorithm for deciding whether a monoid of rational matrices is conjugate to a monoid of integer matrices.

Presentation of a paper with same title, accepted at ICALP 2026.

Co-Authors: Rida Ait El Manssour, Nathan Lhote, Mahsa Shirmohammadi, James Ben Worrell

ABSTRACT. We study succinctness as a measure of the expressive power of transformers. Succinctness---how compactly a formalism can describe a language relative to other formalisms---is a classical notion in logic and automata theory. We prove that fixed-precision transformers are remarkably succinct: they can be exponentially more succinct than both linear temporal logic (LTL) and recurrent neural networks, and, by extension, state-space models, and doubly exponentially more succinct than finite automata. In other words, there exist families of languages describable by polynomial-size transformers whose smallest equivalent LTL formula or recurrent neural network is exponentially large, and whose smallest equivalent automaton is doubly exponentially large. We also establish matching upper bounds, showing that any fixed-precision transformer can be converted to an LTL formula with at most an exponential blow-up---improving a prior doubly exponential translation. As a consequence of this succinctness, we show that basic verification problems for transformers, such as emptiness and equivalence, are provably intractable: specifically, EXPSPACE-complete. This is joint work with Ryan Cotterell and Anthony W. Lin. Published at ICLR 2026.

ABSTRACT. We propose One-counter Positive Negative Inference (OPNI), a passive learning algorithm for deterministic real-time one-counter automata (DROCA). Inspired by the RPNI algorithm for regular languages, OPNI constructs a DROCA consistent with any given valid sample set. We further present a semi-algorithm for active learning of DROCA using OPNI, and provide an implementation of the approach. Our experimental results demonstrate that this approach scales more effectively than existing state-of-the-art algorithms. We also evaluate the performance of the proposed approach for learning visibly one-counter automata.

Joint work with: Anirban Majumdar (TIFR), Shibashis Guha (TIFR), and A.V. Sreejith (IIT Palakkad)

Publication: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.35 Tool: https://zenodo.org/records/17310292

ABSTRACT. As an alternative to visibly pushdown automata, we introduce visibly recursive automata (VRAs), composed of a set of classical automata that can call each other. VRAs strictly extend systems of procedural automata, a model proposed in 2021 by Frohme and Steffen. Deterministic VRAs forms a strict subclass in terms of expressive power. To overcome this limitation, we propose a (weaker) notion, called codeterminism, that does not restrict expressive power. Using properties of codeterminism, we study the complexity of standard language-theoretic operations and decision problems for VRAs. Many practical systems exhibit a recursive structure, making VRAs a natural and compact model compared to monolithic automata. Moreover, their modular nature means they can be used to realize compositional model-based testing or verification. Motivated by this, we show the existence of a canonical VRA and propose an active learning algorithm for VRAs within Angluin's framework that learns this canonical VRA.

ABSTRACT. This paper presents a novel dynamic post-shielding framework that enforces the full class of $\omega$-regular correctness properties over learned probabilistic policies. This constitutes a paradigm shift from the predominant setting of safety-shielding -- i.e., ensuring that nothing bad ever happens -- to a shielding process that additionally enforces liveness -- i.e., ensures that something good eventually happens. At the core, our method uses \emph{Strategy-Template-based Adaptive Runtime Shields (STARs)}, which leverage permissive strategy templates to enable post-shielding with minimal interference. As its main feature, STARs introduce a mechanism to \emph{dynamically control interference}, allowing a tunable enforcement parameter to balance formal obligations and task-specific behavior \emph{at runtime}. This allows triggering more aggressive enforcement when needed while allowing for optimized policy choices otherwise. In addition, STARs support runtime adaptation to changing specifications or actuator failures, making them especially suited for cyber-physical applications. We evaluate STARs on various benchmarks to showcase their scalability, adaptability and performance.

The paper has been accepted for publication at AAMAS'26. This is joint work with Satya Prakash Nayak, Ritam Raha and Anne-Kathrin Schmuck.

ABSTRACT. LTL-Synthesis, i.e. the problem of automatically construct- ing a correct-by-construction controller from a given specification in Lin- ear Temporal Logic[3], is a fundamental problem in formal methods with applications in the design of safety-critical systems. One of the established state-of-the-art tools for LTL Synthesis is SemML. The synthesis pipeline of SemML starts with an LTL formula, which is translated into an automaton and subsequently into a parity game. Solving the game then yields a winning strategy. The first step, i.e. translating an LTL formula into an automaton, is one of the standard approaches in LTL synthesis. However, the usual approaches used determinisation procedures, e.g. by Safra, to obtain a desired deter- ministic parity automaton, which can be up to doubly exponential in the size of the input LTL formula. SemML, on the other hand, uses a direct translation that follows the logical structure of the formula, which results in a more compact automaton and keeps the semantical information by construction. When computing winning regions during the strategy synthesis from the parity game, since synthesising the whole strategy directly is expensive and in some cases infeasible, SemML explores the important game parts and builds the strategy on the fly, achieving better scalability. However, heuristic-guided synthesis does not guarantee optimality in the initial attempt, and the resulting strategy may require repair or refinement. In our ongoing work with Jan Křetínský and Max Prokop, we focus on the problem of strategy repair: given a suboptimal strategy, we aim to improve it using semantic information gathered during synthesis and ML techniques. By exploiting this information, we seek to identify the regions of the strategy that are likely suboptimal and focus repair efforts on those areas, directing the optimal strategy search and saving resources.

ABSTRACT. Probabilistic programs extend classical programs by statements that take samples from random distributions. As such, program variables, as well as the number of loop iterations until termination are random variables. Natural verification tasks for such programs are then deciding whether they terminate, and computing bounds for the expected value of expressions of the program variables after termination.

Those tasks can be accomplished through proof rules, which require synthesizing Supermartingales and Martingales, which serve as ranking functions and invariants respectively. To guarantee soundness those proof rules however require either their absolute step-wise difference to be bounded, or a global lower bound on their value. These restrictions make it particularly hard to synthesize such expressions even for very simple branching-free single loop programs, where the updates for random variables are not bounded. In this talk I will present how for a restricted class of programs the distribution of expressions over program variables in the n-th iteration can be bounded, which can then be used to bound the expected value after termination. Notably this works for programs with unbounded updates for which analysis fails with other state of the art approaches.

The talk consists of work presented at QEST+FORMATS'25 and ongoing work. Joint work with Laura Kovács, Anne Schreuder, C.-H. Luke Ong.

ABSTRACT. Stone-Age networks are distributed systems operating under extremely weak communication assumptions. In particular, beep networks restrict communication to a single binary signal: in each synchronous round, a process either emits a beep or listens, in which case it can only distinguish between silence and the presence of at least one neighbouring beep.

In this paper, we focus on anonymous networks in which all processes execute the same finite-state protocol. We study the state-coverability problem for such Stone-Age and beep protocols over arbitrary network topologies. We first show that both models are equivalent with respect to coverability. Our main result is that coverability is undecidable already on tree topologies. The proof relies on a simulation of two-counter Minsky machines, in which machine configurations are encoded along branches of the network and instructions are propagated locally through message waves.

We also investigate restricted classes of topologies. While coverability is undecidable in general, we show that bounding the depth of the trees yields a decidable problem, which is Tower-complete. Moreover, when restricting the topology to cliques, coverability becomes PSPACE-complete.

This is a joint work with A.R. Balasubramanian.

ABSTRACT. 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 output. In practice, it is natural to allow each agent to carry a unique identifier and compare it with that of another agent before interacting. We model this extension by having agents be totally ordered and interactions between two agents to be fireable only if their pair of identifiers falls in some condition set. For instance, PP[<] allows for two agents to interact only if the first one appears before the second one.

In this talk, I will present a study of population protocols over ordered agents PP[N] where N is a set of predicates available to restrict transition firing, and IO-PP[N], the immediate observation fragment of PP]N] where only one agent changes state per interaction. Our main result is that IO-PP[<] recognizes exactly the unambiguous star-free languages, which admits many other characterizations, such as two-variable first-order logic or two-way deterministic partially-ordered automata. We also provide a logic and an automaton model that fits in PP[<]. We further show that if the successor predicate appears in a set of NSPACE-computable predicates, then IO-PP[N]=PP[N]=NSPACE(n). Finally, we investigate the problem of deciding whether a given population protocol always stabilizes to a consensus. While this problem is decidable for unordered population protocols, we show that this is undecidable already for PP[<] and IO-PP[+1], but conditionally decidable for IO-PP[<].

Work with Michael Blondin, Benjamin Courchesne, Lucie Guillou, Corto Mascle, and Isa Vialard. ICALP 2026.

ABSTRACT. Knowledge compilation studies representations of Boolean formulas for which queries (satisfiability, model count, ...) and operations (conditioning, conjunction, ...) are tractable, while keeping representation size compact for various formula classes. It finds applications in formal methods (software verification, quantum circuit simulation, ...) and AI. While the literature focuses on sequential tractability (P), parallel tractability (NC) is increasingly important in a world where parallel hardware (multi-core, GPUs) is becoming the norm.

We are investigating the theoretical parallel complexity of representations in the sequential knowledge compilation map as well as more recent structures (SDNNF, SDD, TDD) in order to inform future research both on the application-oriented side as well as for the design of new representations.

So far, we found queries on more general (succinct) representations are often P-complete (meaning that there is an NC-algorithm only in the case that P = NC, which is considered unlikely), and that the more structured representations (SDD, TDD, subclasses of SDNNF) do admit NC-algorithms for various queries and operations. As existing sequential algorithms tend to use bottom-up approaches on structures that can be deep, some parallelizations require novel insight. We have preliminary results that circuits with certain tree-like structure admit an NC evaluation algorithm, from which positive results for SDDs and TDDs follow.

The presentation will briefly introduce the field of knowledge compilation and present our preliminary results on a parallel perspective.

This is joint work with Alexis de Colnet and Alfons Laarman.

ABSTRACT. Games on graphs constitute a fundamental model. Applications include reactive synthesis, which reduces to solving a zero-sum two-player game, and reasoning about multi-agent systems by modeling them as a multi-player game. We study a class of graph games called bidding games in which the players are allocated a budget, and in each turn, an auction determines which player moves the token. Two-player bidding games have been extensively studied. We study, for the first time, multi-player bidding games. We focus on discrete bidding, which imposes granularity restrictions on the players’ budgets and bids. The original motivation for discrete bidding is practical applications, and technically, it is appealing that the game has only finitely-many configurations. We initiate our study by considering a game between two coalitions of players. We show that under mild assumptions on the mechanism that is applied to break bidding ties, bidding games are determined: from every initial configuration, one of the coalitions has a winning strategy. Thus, we identify a sub-class of multi-player concurrent games that is determined. Using determinacy, we show that a pure Nash equilibrium always exists. Finally, we show that the complexity of deciding which coalition wins from a given configuration is PSPACE-hard already in reachability games and already for budgets given in unary. This is in stark contrast to two-player games, which are known to be in NP and coNP even for budgets given in binary.

ABSTRACT. Bidding games are graph games in which each player starts with an initial budget, and a simultaneous auction determines which player moves the token; the players' budgets are then updated accordingly. Motivated by scenarios such as resource-allocation systems in which agents receive periodic income (e.g., credits, energy) while competing for control, we introduce and study bidding games with income, in which, at each vertex, players may receive additional budget. We focus on reachability discrete poorman bidding games with income (DPBGi). The main challenge when compared to discrete bidding games without income is that the configuration graph is infinite. To this end we introduce a novel technique to eliminate plays with suboptimal infixes. This enables focusing on a finite part of the infinite configuration graph in order to solve the game via approximation to continuous bidding games. Finally, on a subclass of DPBGi in which the reachability player holds a substantial advantage, we provide an explicit solution with better complexity.

Co-authored by Dana Fisman, Ben Gurion University.

ABSTRACT. Cellular automata (CA) are canonical models of parallel computation, classically studied as recognizers. We adopt a generative perspective: given a regular set of initial configurations on a bi-infinite grid, what language is formed by the set of configurations reachable under the CA's local rule? Prior work on CA over bounded grids, where CA are viewed as recognizers, showed that the Chomsky-hierarchy complexity of the input language is preserved under evolution. On an unbounded grid, the generative picture is fundamentally different: even from the simplest regular initializations, the reachable configurations can form languages far beyond regular, spanning the entire one-counter automata hierarchy and reaching context-sensitive territory, as witnessed by {a^n b^n c^n | n in N}.

To explain this expressiveness structurally, we introduce gliders: atomic single-cell entities, each carrying a symbol at a fixed velocity, with interaction semantics derived directly from the CA's local rule. A finite collection of gliders equipped with a dominance order specifying which glider prevails upon collision defines a natural and strict subclass of CA-expressible languages. Our main result shows that all bounded languages whose Parikh image is a linear set are glider-expressible, thereby capturing forms of expressive power far beyond those of context-free or one-counter models.

This talk is based on joint work with Dana Fisman: Atomic Gliders and Cellular Automata as Language Generators. In: Verification, Model Checking, and Abstract Interpretation. VMCAI 2026. Lecture Notes in Computer Science, vol 16417. Springer, Cham.

https://arxiv.org/pdf/2511.12656

ABSTRACT. We propose a decoupled approach to synthesizing a word, letter by letter, that is in the conjunction of a given pair of regular objectives. A key application is multi-objective robotic path planning, where each letter corresponds to a robot action and the goal is to find a plan that satisfies both objectives. The traditional monolithic solution would construct the product automaton, and obtains a ``generator'' that outputs an accepting word. Instead, we synthesize two independent generators and compose them at runtime via an auction-based mechanism: at each time step, the generators bid for who chooses the next symbol. Advantages of this approach include design in parallel or by different vendors, and reusability, namely when an objective changes only the relevant generator is updated and the other is reused. We design, for the first time, a framework in which each generator is designed on a separate automaton. This enables decoupled planning for a conjunction of objectives each of which is given as a logical specification, e.g., in LTLf, and addresses a central limitation of previous approaches.

For cases in which a feasible solution is not found, we develop a successive refinement algorithm that searches for a pair of assumptions that regain feasibility. Weaker assumptions lead to increased modularity. Our algorithm is based on a novel automata-learning algorithm that can be of independent interest; the algorithm produces a sequence of automata, each provides as assumption, that converge to the target automaton (the ``teacher's automaton'') and whose languages are all contained in it. Containment implies that the assumptions are sound.

We provide a proof-of-concept implementation and demonstrate the effectiveness of the approach. We demonstrate the reusability of our solutions and show that our refinement algorithm gains feasibility by finding non-trivial assumptions.

ABSTRACT. We present RATTL (Risk-Adversarial Total-Reward Learning), a framework for safe sequential decision making in partially observable stochastic games in which the agent's Bayesian belief entropy \emph{implicitly selects} its position on the Entropic Value-at-Risk spectrum---maximal caution under ignorance, risk-neutrality after identification, principled interpolation in between. The construction is a Wasserstein ambiguity ball whose radius is modulated by the Shannon entropy of the current belief; via the EVaR--DRO duality, this yields a Nash-Robust Bellman operator whose unique fixed point is sandwiched between type-blind maximin and type-omniscient Bayesian best-response. We motivate the choice of Wasserstein over KL geometry on safety grounds, illustrate the resulting ``safety switch'' on a diagnostic game, and pose the open problem of identifying the coherent risk measure dual to $W_1$ balls.

ABSTRACT. Due to advances in deep learning, several problems that were previously considered intractable, like language modelling and image classification, can now be solved by training Deep Neural Networks (DNNs) on appropriate datasets. However, these DNNs have been shown to lack robusness and be vulnerable to adversarial attacks. Due to this, DNNs still only find limited applicability in safety critical domains such as medical imaging and controllers autonomous vehicles. This is because even plausible real-world inputs can be adversarial for the DNN being deployed, and lead to a safety violation.

Runtime monitoring of DNNs attempts to alleviate this issue by trying to predict if, for a given input, the output of the DNN can be trusted correct and therefore safe. While several techniques for runtime monitoring of DNNs have been explored in the literature, the formal safety guarantees provided remains limited. Out of distribution detection techniques only provide empirical evidence for the effectiveness of the technique, while other techniques provide statistical guarantees contingent upon assumptions on the distribution of input data or activation values within the layers which may not hold in real life. Other works use techniques from formal methods, like abstraction, and therefore can provide concrete formal safety guarantees. However, the safety properties only encode deviation of the input or activation values from a pre-determined training dataset, and therefore may not cover all possible sources of real-life safety violations. Thus, when incorporating these monitors into safety critical systems, challeneges remain.

Randomised smoothing can convert any classifier into a robust classifier by considering the consensus output obtained by sampling a neighborhood of the original input. Intuitively, if the classifier agrees with high probability within a neighbourhood around an input $\vct{x}$ original input, one can derive a formal guarantee that perturbing the input slightly to $\vct{x} + \vct{\delta}$ does not change the consensus answer. Crucially, this is not dependent on any distributional assumptions on input data or activation values, nor does it depend on behavioral assumptions on the DNN.

In this talk I will present ongoing work with Prof. Jan K\v{r}et{\'{\i}}nsk{\'{y}} and Sabine Reider exploring leveraging randomised smoothing for building a DNN monitor that provides concrete safety guarantees with respect to local robustness properties. I will also briefly talk about how such monitors may be adapted to monitoring a DNN-based policy in an MDP setting, which is a basis of a more early-stage exploration with Deep Ganguly and Prof. Jan K\v{r}et{\'{\i}}nsk{\'{y}}