ABSTRACT. Rabin's Tree Theorem says that the MSO theory of the infinite binary tree 2* is decidable. Shelah showed that MSO logic becomes undecidable if this tree is extended to 2^≤ω, i.e. by allowing quantification over sets of infinite branches. A longstanding open problem is whether the decidability can be recovered in 2^≤ω by restricting set quantification to Borel sets. We make some progress in this direction, by identifying a suitable automaton model, and showing that most of the automata-theoretic approach to Rabin's Theorem can be extended to the new framework. The only missing part is a conjecture about finite-memory determinacy in certain games. This paper states and explores the conjecture. We prove it in some restricted cases, and give lower bounds on the memory required in those games. Joint work with Mikołaj Bojańczyk, Antonio Casares and Paweł Parys (submitted to LICS).

ABSTRACT. We introduce layered automata, a subclass of alternating parity automata that generalises deterministic automata. Assuming a consistency property, these automata are history deterministic and 0-1 probabilistic. We show that every omega-regular language is recognised by a unique minimal consistent layered automaton, and that this canonical form can be computed in polynomial time from every layered or deterministic automaton. We further establish that, for layered automata, both consistency checking and inclusion testing can be performed in polynomial time. Much like deterministic finite automata, minimal consistent layered automata admit a characterisation based on congruences. This work will be presented at LICS'26. Full version https://arxiv.org/abs/2601.15940

ABSTRACT. We describe a 65-state history-deterministic Büchi automaton that has strictly less states than every language-equivalent deterministic Büchi automaton. This solves a problem that had been open since the introduction of history-determinism and actively investigated for over a decade.

This is joint work with Antonio Casares and K. S. Thejaswini, and the related paper can be found on arxiv.

ABSTRACT. I propose to present a work that I prepared along with Mauricio Cari and Cristian Riveros, both from Pontificia Universidad Católica de Chile, that is about disambiguation of finite automata. We have submitted it to the Track S of ESA, and is currently under revision.

Abstract:

We study the task of disambiguation of finite state automata, namely, converting an automaton into an equivalent, unambiguous one. We do this by developing a novel and simple algorithmic framework that generalizes the subset construction for determinization, and that satisfies some desirable properties: (1) it preserves the original automaton if it was already unambiguous, (2) it computes the successor states on-the-fly and (3) computes each new state in polynomial time---this last point is crucial as it guarantees that the running time is polynomial in the size of the output automaton.

Then, we show how to apply this framework for _partial_ disambiguation: by changing the criterion that builds the new states, we develop algorithms for different levels of ambiguity, namely, finitely ambiguous, and polynomially ambiguous automata. These algorithms also satisfy condition (1) for their respective levels, and also (2) and (3).

Finally, we show that the disambiguation framework can easily be extended to other models of automata like weighted automata. Indeed, we extend the disambiguation procedure onto weighted automata, for the same levels of ambiguity, while preserving the same properties as before. The resulting automaton is not always finite, so we focus on automata over the tropical semiring and present some simple conditions to ensure finiteness in this case.

ABSTRACT. Minimizing the size of finite automata is a fundamental problem in theoretical computer science. Beyond standard minimization, further reductions can be achieved by decomposing an automaton into smaller components whose languages combine via intersection or union to recover the original language. However, in general, no polynomial-time algorithm is known for computing such decompositions. In this paper, we focus on automata that recognize ideals, that is, languages at level 1/2 in the Straubing–Thérien hierarchy. Equivalently, these languages are expressible as a finite union of languages of the form A^* a_1 A*... A^* a_n A* where A is an alphabet and a_i are letters of A. We show that the two problems of deciding whether such a language can be decomposed into an intersection or a union of smaller automata are decidable in NL. Moreover, we provide a polynomial-time algorithm that computes a decomposition into an intersection, if one exists, while ensuring that the resulting components also recognize ideal languages.

This work is a joint work with Pierre-Cyrille Héam and Ismaël Jecker and has been submitted to CONCUR. The full version is available on arXive: https://arxiv.org/abs/2604.25619

ABSTRACT. This talk presents joint work with Antoine Amarilli and Charles Paperman.

Regular languages are classically viewed as the languages that can be recognized with constant memory when the input word is read from left to right. But what happens when the letters of the word arrive out of order? We study this question through the problem of out-of-order membership: the length of a word is known in advance, but its letters are streamed as pairs (i,w[i]), one for each position, in an arbitrary order. The goal is to decide whether the completed word belongs to a fixed regular language while minimizing memory.

I will present our classification results and the algebraic picture behind them. At the level of monoids, we obtain a complete trichotomy for out-of-order evaluation: the optimal space is either Θ(1), Θ(logn), or Θ(n), characterized by natural varieties of monoids. For semigroups, where no neutral element is available, the situation becomes subtler: we characterize exactly the semigroups admitting constant-space algorithms and show logarithmic lower bounds outside this class. Finally, I will explain why the original language problem is richer than both algebraic abstractions, with examples ranging from constant-space languages such as (ab)*, to linear lower bounds such as Σ*aaΣ*, and to unexpected intermediate behaviours, including logarithmic and sublinear-space algorithms.

The interest of the result is twofold: it introduces a natural streaming variant of regular-language membership motivated by distributed and networked data, and it reveals a sharp interaction between automata theory, algebraic language theory, and space complexity.

ABSTRACT. We introduce the {Asymptotic Hausdorff} lifting, denoted {AH}_{d}, a general method for lifting an element-level metric {d} to a (pseudo-) metric on sets, that captures asymptotic similarity in infinite domains equipped with a notion of size. The construction is designed to be insensitive to finite deviations and to avoid the limitations of classical Hausdorff-based approaches, which are often overly sensitive to outliers and fail to reflect asymptotic behavior.

Formal languages provide a central motivating instance of this framework, where elements are words and sets are languages. When applied to normalized edit distances, the Asymptotic Hausdorff lifting yields metric-valued distances between languages that reflect asymptotic edit behavior while preserving metric structure. We study the equivalence classes of regular languages induced by {AH}_{d} for normalized edit distances {d}, and characterize their asymptotic essence. Focusing in particular on the normalized edit distance of Marzal and Vidal, {ned}, we investigate the computation of {AH}_{ned} for regular languages and for bounded context-free languages.

The talk is based on a joint work with Gal Meirom, accepted to ICALP'26.

https://arxiv.org/abs/2605.09668

ABSTRACT. Nested words augment words with matching call-return pairs, and are a natural model for data with dual linear-hierarchical structure. Such data includes XML documents and recursive procedure calls in programs. Nested word automata (NWA) traditionally describe regular languages of nested words. However, non-deterministic NWA suffer from the state explosion problem for determinisation. Moreover, we believe that interpretability of languages with deep nestings and distinct patterns within these nestings is hindered as the different nesting layers are not explicitly modelled. We recently introduced the hierarchical-alphabet automaton (HAA), an alternative finite-state acceptor for regular languages of nested words. We present the idea behind our model, demonstrate its usage with an example, and discuss its advantages.

ABSTRACT. We present an effective and elementary procedure for computing the measure of a regular language of infinite trees, which is, in general, an algebraic number.

One way of defining regular tree languages is via vectorial nested fixed-point expressions evaluated in the powerset tree algebra. The variables occurring there correspond to states of automata. After adding topology and measures over trees, these variables become random variables, generally highly correlated. What we seek is their joint distribution, and it turns out that this distribution can again be characterised via fixed points. However, this requires extending the fixed-point paradigm at both the syntactic and semantic levels. In the novel unary μ-calculus, fixed-point operators indicate a fixed point closest to a function argument (in an appropriate sense), thus avoiding reduction of the function's type. On the semantic level, a probabilistic powerdomain, although failing to form a lattice, still allows the desired probability distributions to be computed as fixed points.

We believe that the new techniques have the potential for further applications whenever the realm of automata intervenes with real numbers.

The presentation is based on the paper "On the Computability of Measures of Regular Sets of Infinite Trees" accepted to the Journal of the ACM, co-authored with Paweł Parys and Michał Skrzypczak. The result was previously announced by Paweł Parys at Highlights 2023. The talk aims to provide a broader perspective on the new techniques and to indicate directions for further development.

ABSTRACT. Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says "Heads" or "Tails". The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when each pair of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes!

We introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.

ABSTRACT. Recent work in formal methods has begun to study the computational complexity of equilibrium-based reasoning in multiplayer games, motivated by the need to reason about correctness in systems with multiple strategic agents that operate independently. In this talk, we study probabilistic concurrent multiplayer reachability games, where players choose actions simultaneously in a stochastic environment and are incentivized to satisfy a reachability objective. We focus on the verification problem, which asks whether a given candidate strategy profile satisfies standard equilibrium conditions. We study this question across several equilibrium notions, including Nash equilibria, correlated equilibria, and their subgame-perfect refinements. Across these settings, we observe a recurring and somewhat counterintuitive phenomenon: subgame-perfect equilibrium notions that impose additional structural constraints are strictly easier to verify than their more general counterparts under standard complexity-theoretic assumptions. At a technical level, this arises from a separation between global optimality reasoning and local optimality verification in an induced Markov Decision Process: while global optimality requires solving an MDP and is P-complete, verifying optimality of a fixed policy across all states simultaneously admits a bounded-precision, digit-wise analysis of quantitative values that can be carried out in NC. Therefore, unlike many classical treatments in formal methods, the analysis of these games requires explicit control of numerical precision and bounds on the size of values arising in computation, reflecting a robust quantitative structure that is not typically made explicit in equilibrium verification. Finally, we discuss how these verification results give us paths forward to reasoning about the realizability problem, which asks whether an equilibrium exists in a given game. This remains a major open problem in game theory, as the discontinuities in payoff structure induced by the prefix-dependent reachability goals prevent the direct application of fixed-point arguments that guarantee existence in other probabilistic models. This talk is a brief survey of the following highly related papers: https://arxiv.org/abs/2503.14690 (joint work with Moshe Y. Vardi, published in LMCS) https://arxiv.org/abs/2604.24655 (joint work with Jean-François Raskin and Moshe Y. Vardi, in submission)

ABSTRACT. This is joint work (in progress) with Deep Ganguly, Marta Grobelna, and Jan Kretinsky.

We study the problem of efficiently updating value functions for reachability in Markov decision processes (MDPs) and simple stochastic games (SGs) under local structural changes. In particular, we consider the setting where optimal state values for a model are already available, possibly approximately, and a modification is introduced by removing a single action from a given state. Such a change invalidates the existing value function, yet recomputing optimal values from scratch using standard value iteration can be prohibitively expensive. We propose a theoretical framework for reusing previously computed value information to derive sound and informative bounds on the new optimal value function after action removal. Our approach characterizes how local action restrictions propagate through the Bellman equations and provides a method to construct lower and upper bounds on the updated values directly from the original solution. These bounds are guaranteed to be compatible with the modified model and can be used to initialize value iteration, replacing the conventional zero or trivial initialization. We show that starting value iteration from these bounds preserves correctness and significantly reduces the number of iterations required for convergence. The framework applies uniformly to MDPs and turn‑based stochastic games, as well as to exact and approximate value functions.

ABSTRACT. Probabilistic hyperproperties describe relations among multiple sets of executions in a stochastic system. Prominent examples include information-theoretic formulations of security and privacy requirements. However, for existing probabilistic hyperlogics such as HyperPCTL and PHL, model checking is undecidable on Markov decision processes (MDPs), the standard model of concurrent stochastic systems. To overcome this limitation, we identify fragments of probabilistic hyperlogics that remain expressive for relevant specifications while admitting tractable model checking. Concretely, we introduce the fragment of relational properties that compare probabilities of events, potentially across independent executions of an MDP. Representative examples of relational properties include: Can two different target states be reached from the same initial state with equal probability? Can a fixed target state be reached from two different initial states with equal probability? Beyond reachability, our relational properties also capture safety, Büchi, and co-Büchi objectives. Moreover, they support conjunction and thus generalize standard multi-objective MDP properties. We provide efficient algorithms for relevant classes of relational properties and establish computational hardness results for others. Our implementation on top of the probabilistic model checker Storm outperforms solvers for more general probabilistic hyperlogics by orders of magnitude on the subset of their benchmarks covered by our fragment.

ABSTRACT. Given rationals α and β, the sure-almost-sure problem for an objective φ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have φ-value at least α (i.e., sure α satisfaction), and with probability 1 the outcome has φ-value at least β (i.e., almost-sure β satisfaction). The sure-limit-sure problem asks if for all ε > 0, one can simultaneously ensure that all outcomes have φ-value at least α, and with probability at least 1 − ε the outcome has φ-value at least β. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this.

In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that the average payoff of a finite window that slides over an infinite run be greater than a given threshold. We study two variants of window mean payoff; for both variants we show that sure-almost-sure problem and the sure-limit-sure problem are no harder than sure satisfaction and almost-sure satisfaction when considered separately for these objectives.

ABSTRACT. Concurrent stochastic games are a fundamental game-theoretical model. In the setting of formal methods, the reachability and safety objectives form the cornerstone of most properties. Despite significant effort, algorithms for approximating the value of these games with a guaranteed precision remained long elusive. The difficulty of this problem can be documented by past erroneous attempts. We leverage the insight gained in the recently provided value-iteration algorithm and provide a policy-iteration (a.k.a. strategy-improvement) algorithm with guaranteed precision. This can be also seen as providing a correct stopping criterion for the standard strategy iteration.

This is ongoing work with Jan Kretinsky, Maximilian Weininger, and Eline M. Bovy

ABSTRACT. We study concurrent graph games where $n$ players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other.

We show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals ($\exists\mathbb{R}$) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is $\NP$-hard. For the almost-sure reachability problem, we prove $\NP$-completeness.

We introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop.

ABSTRACT. Partially observable Markov decision processes (POMDPs) are a central model for uncertainty in sequential decision making. The most basic objective is the reachability objective, where a target set must be eventually visited, and the more general parity objectives can model all -regular specifications. For such objectives, the computational analysis problems are the following: (a) qualitative analysis that asks whether the objective can be satisfied with probability (almost-sure winning) or probability arbitrarily close to (limit-sure winning); and (b) quantitative analysis that asks for the approximation of the optimal probability of satisfying the objective. For general POMDPs, almost-sure analysis for reachability objectives is EXPTIME-complete, but limit-sure and quantitative analysises for reachability objectives are undecidable; almost-sure, limit-sure, and quantitative analysises for parity objectives are all undecidable. A special class of POMDPs, called revealing POMDPs, has been studied recently in several works, and for this subclass the almost-sure analysis for parity objectives was shown to be EXPTIME-complete. In this work, we show that for revealing POMDPs the limit-sure analysis for parity objectives is EXPTIME-complete, and even the quantitative analysis for parity objectives can be achieved in EXPTIME.

ABSTRACT. System analysis and verification always require new reasoning frameworks, to tackle novel programming features, or new considerations on programs. However, building such frameworks is a delicate activity. In particular, establishing a tight correspondence between a reasoning system and a semantic one often proves difficult.

This work aims at simplifying these tasks. I introduce a new abstract structure to model systems that contain both syntactic and semantic elements. This structure, called "representation", takes very lax assumptions, thus capturing a wide variety of systems.

This talk is based on my RAMiCS'26 paper.

ABSTRACT. We derive multiple program logics, including correctness, incorrectness and their probabilistic variants, and relational Hoare logic, from the axioms of imperative categories: uniformly traced distributive copy-discard categories. Examples of imperative categories include partial, relational and (sub)probabilistic program semantics. This is recent joint work with Filippo Bonchi, Mario Román and Sam Staton. Preprint available at https://www.arxiv.org/abs/2507.18238.

ABSTRACT. Normalization, D(X + 1) → D(X) + 1, is almost a distributive law; but because one of the distributive law axioms only holds up-to-idempotent, it yields a non-associative composition of normalized kernels. We introduce the Markov magmoid of normalized stochastic kernels: a normalized-by-construction semantics for probabilistic inference, unifying exact Bayesian observations and interventions as two parenthesizations of the same composite. Front-door and back-door criteria follow from the axioms of Markov magmoids; we implement these with non-associative monadic notation. This is joint work with Elena Di Lavore and Márk Széles (https://arxiv.org/pdf/2510.01131).

ABSTRACT. The recognition of languages by homomorphisms is a central notion in algebraic language theory. Initially studied for monoids and semigroups, it has subsequently been expanded to other algebras and categorified. We give a new categorical account based on fibrations, which have already seen various applications in automata theory. Our motivation comes from two observations. Firstly, the notion of recognition makes sense for arbitrary algebras: to each algebra one can associate a set of languages and a set of homomorphisms acting as recognisers, hence it seems natural to capture these data by fibres for suitable fibrations. Secondly, the Grothendieck construction gives a correspondence between (cloven) fibrations and fibres together with a functorial reindexing operation. The fact that languages are closed under inverse homomorphisms then suggests that a fibrational account is natural as well.

We establish language and quotient fibrations with the property that language recognition is stable under reindexing. Apart from this conceptual contribution, we make two technical contributions. (1) We show how some existing results by Adamek can be extended to prove the existence of syntactic objects, and follow results by Slominski to give a concrete construction of syntactic objects in specific cases using the language of fibrations and the notion of translations from universal algebra. (2) We show under which conditions regular languages are closed under Boolean operations, focusing in particular on the closure under limits and colimits.

This is joint work with Harsh Beohar and Georg Struth.

ABSTRACT. There have been fruitful extensions of computational models such as automata and Petri nets to settings where inputs carry data from an infinite relational structure \( A \). Consequently, systems of linear equations where indeterminates are indexed by elements of a relational structure \( A \) have received a lot of attention recently due to their usefulness in analyzing such computational models.

Following a similar approach, given a relational structure \( A \), we study polynomials whose variables are indexed by the elements of \( A \). This algebra carries a natural action of the automorphism group of \( A \), and its invariant ideals provide a setting for studying invariant systems of polynomial equations. We develop a theory of radical, prime, Goldman, and maximal ideals for algebras equipped with the action of a group, allowing us to recover an analogue of the spectrum of a ring in the presence of symmetry. We also study Nullstellensatz-type results, which prove or disprove the existence of (invariant) solutions to such invariant systems.

This is a joint work with Joanna Fijalkow, Arka Ghosh, and Aliaume Lopez.

ABSTRACT. We propose an alternative formulation of Kaminski&Francez’s register automata with a local view of memory: instead of having a fixed global bank of registers, each state carries only the registers that are live there, and transitions explicitly describe how successor registers are inherited from current registers and input data. To capture this idea, we introduce a notion of 'supported sets with justifications' and consider deterministic automata over these objects. We may then provide a simple semantic account of register automata through an equivalence with a category of nominal sets. An injective variant recovers the well-studied correspondence between equality-guarded register automata and nominal automata. This construction extends to a general categorical setting through a Grothendieck construction, thereby providing powerful abstract reasoning tools.

Extended abstract attached.

ABSTRACT. Alternation is the interleaving of two dual computational modes such as existential and universal choice. It is one of the fundamental ideas in theoretical computer science. Its significance lies in succinctness: alternating models can be exponentially more concise than their non-alternating counterparts.

The study of alternation has been extensive at the level of models of computation. By contrast, alternation at the syntactic and algebraic level remains largely unexplored.

Kleene Algebra gives a sound and complete system for proving when two expressions in some star-semiring are equivalent. In particular, when it is applied to regular expressions, it can check if they denote the same language. In this context, it is a powerful tool for reasoning about programs and systems that can be modeled as state machines.

As a first step towards studying alternation from an algebraic perspective, we extend the Kleene algebra (KA) to Alternating Kleene algebra (AKA) to support intersection. We utilize the succinctness of alternation to provide a complete equational axiomatization and demonstrate optimal proof complexity. We also provide its application in rewritting systems.

ABSTRACT. Cyber-physical systems can be subject to information leakage; in the presence of continuous variables such as time and energy, these leaks can be subtle to detect. Opacity is a critical property in security verification, as it ensures that private information cannot be deduced from the system's behavior. In this talk, we present our investigation into verifying opacity in systems under both timing and energy observations. We introduce guarded multi-energy timed automata as an extension of timed automata with multiple energy variables and guards over such variables. Despite the undecidability of this general formalism, we establish positive results over a number of subclasses, notably when the attacker observes the final energy and/or the execution time, but also when they have access to the value of the energy variables every time unit.

ABSTRACT. Correct-by-construction safety control is usually phrased as an all-or-nothing question: either the controller can keep the system safe forever, or synthesis fails. This talk is about the failure case: when safety is impossible, can we still synthesize a canonical, geometry-driven best-effort controller? The full technical developments appear as a CAV 2026 paper; the proposed talk will focus on the best-effort idea and on a two-tank case study whose optimal policy exhibits an interesting geometric structure.

ABSTRACT. Weighted timed games are weighted timed automata in which locations are divided between two players, Min and Max. Min aims to reach a goal state with minimal weight. In general, the problem of computing this minimal weight exactly, known as the Value problem, is undecidable. Guilmant and Ouaknine have even shown that the Value cannot be approximated. However, can the Value be approximated for weighted timed games with only positive weights? This question has remained open for more than a decade.

In this talk, I will present new results providing insights into the approximability of weighted timed games.

ABSTRACT. Current-state estimation is a fundamental method in formal verification and control science that has applications in privacy, fault diagnosis, and the verification of other state inference properties. The goal is to accurately compute all possible internal states of a system, given some observation of its behavior. For timed automata, this problem is particularly challenging because the system state consists not only of a discrete location, but also of clock valuations. Moreover, a current-state estimator has to account for both unobservable events and passing time, which may change the possible current states even in the absence of visible behavior. For general dense-time models, exact current-state estimation is undecidable. This talk considers current-state estimation for timed automata over the discrete time domain, where time is represented by sequences of tick events. While this setting makes estimator construction algorithmically tractable, standard approaches still suffer from severe state explosion. If M is the largest constant occurring in the timing constraints of the input automaton, explicit constructions may have to enumerate time successors for all values up to M. The number of states of the current-state estimator then scales exponential with M.

To address this bottleneck, we have previously proposed a new class of current-state estimators, called threshold estimators, for a subclass of discrete-timed automata. Instead of explicitly constructing all time-successor states, threshold estimators infer parts of the time evolution symbolically. In our most recent work, we have extended threshold estimators to the full class discrete-timed automata. However, our main technical contribution concerns synchronized observation timed automata (SOTA), a subclass of single-clock discrete-timed automata in which unobservable transitions do not reset the clock and all observable transitions with the same label agree on their reset behavior. We prove that threshold-estimator construction scales independently of M for SOTA. We thereby significantly improve the scalability of current-state estimation of systems that can be represented by SOTA.

The above results are part of joint work together with Prof. Kuize Zhang (Xi'an Jiaotong University) and Prof. Sabine Glesner (Technical University Berlin).

ABSTRACT. State-space explosion remains one of the central challenges in formal verification. Compositional verification addresses this challenge by reasoning about parts of a system in isolation and then combining the results to establish system-wide correctness. In assume-guarantee reasoning, one common approach is to isolate a subsystem and construct assumptions describing the environments in which it behaves correctly. Learning methods have become the dominant paradigm for automated assumption generation, yet extending these techniques beyond restricted classes of timed automata has remained surprisingly difficult.

In this talk, we revisit an earlier algorithmic approach to assumption generation that predates learning methods and show why it is particularly well suited to timed automata. We prove that, unlike for finite automata, the weakest environment assumption describing the most permissive safe environment may fail to be recognizable as a timed automaton. This unexpected result explains why existing assumption-generation techniques do not naturally extend to timed automata and motivates a different route to automated compositional verification.

Rather than constructing the weakest assumption directly, we consider its complement, the language of behaviors leading to property violations. We show that this language admits an effective representation that can be synthesized automatically. We then develop techniques to reduce its size by retaining only behavior that directly affects satisfaction of the property. The resulting framework provides sound and complete compositional verification for safety properties, supports multiple clocks and non-deterministic models, and achieves substantial reductions in the size of the state space across a range of case studies.

This talk is based on a recent paper published at 38th International Conference on Computer Aided Verification (CAV 2026) in collaboration with Hamed Kalantari, Ehsan Khamespanah, Marjan Sirjani, and Ali Movaghar.

ABSTRACT. This is an abstract of the following STTT paper https://link.springer.com/content/pdf/10.1007/s10009-026-00852-2.pdf, joint work with Neha Rino, Eugène Asarin and Florian Renkin.

Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure 𝛿 for STL, based on a new distance that we define over timed signals. In contrast with existing measures, 𝛿 provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL formula. Thus, 𝛿 is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. We obtain therefore, unlike existing robustness measures over STL, the property of equal 𝛿 of a given signal wrt formulae that are equivalent in the Boolean sense.

Though we prove that computing 𝛿 is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. We implement such algorithms in a prototype tool, and evaluate our approach on a case study of quality assessment of insulin controllers for diabetic patients.