QuantFormal

Active automata learning is a key technique in formal methods, particularly for model inference and verification. In the classical setting introduced by Angluin's L* algorithm, a learner interacts with a teacher through membership and equivalence queries to infer a minimal deterministic finite automaton for an unknown regular language L. Membership queries check word inclusion in L, while equivalence queries verify whether a proposed hypothesis dfa matches L, returning a counter-example if not. This approach requires only semantic information about L and runs in time polynomial in the minimal dfa size and the longest counterexample.

In this talk, we extend this framework to deterministic one-counter automata (doca). doca are finite-state machines equipped with a non-negative integer counter that can be incremented, decremented, or reset. The presence of the counter allows doca to recognise certain non-regular, context-free languages, making them a natural candidate for modelling program behaviours that arise in formal verification.

We first present an active learning algorithm for doca called OL*. This is the first polynomial time algorithm. However, this algorithm is not scalable in practice. We then present a few practical algorithms for learning doca. Though exponential in the worst case, these algorithms scale better than OL* in data sets.

In the end, we will discuss approaches and challenges to extending these results to weighted/probabilistic models.

Learning-based methods, such as reinforcement learning, are receiving increasing attention for solving challenging control tasks. However, the lack of safety assurances about learned controllers poses a significant barrier to their practical deployment. In this talk, we will present a framework for learning and formally verifying neural controllers. The framework is applicable to stochastic control systems, thus also considering environment uncertainty. Given a specification, the framework jointly learns and formally verifies a controller together with a formal certificate of the specification being satisfied, both parametrized as neural networks. Certificates are supermartingale-like objects that can be effectively used to formally reason about stochastic systems in a fully automated fashion. We will show how the framework can be applied to solve reachability, safety, reach-avoidance and stability tasks, as well as a compositional framework allowing us to reason about a more expressive logic of specifications.

Runtime monitors (RM) are essential for ensuring the safety and reliability of cyber-physical systems (CPS) throughout their operational lifetime. They play a crucial role in detecting irregularities during execution and in assessing system performance. In modern autonomous cyber‑physical systems RMs become even more essential to ensure safety, in particular when integrating machine learning (ML) components whose behavior may be difficult to predict or verify formally. A central challenge in designing effective runtime monitors lies in achieving robustness to uncertainty in the information obtained from the environment. Monitors rely on sensor data, which is often noisy or incomplete, and with system dynamics that are typically probabilistic, the true state of the environment may only be partially observable. Consequently, runtime monitors must account for these uncertainties when predicting potential safety violations.

In this talk, we address the problem of runtime monitoring under uncertainty, focusing on settings where uncertainty is modeled using Markov models. We present recent results, including algorithmic approaches for monitoring in such probabilistic settings and methods for learning uncertainty models to enhance monitoring accuracy and robustness.

Timed logics provide a foundational framework for specifying and verifying quantitative properties of real time systems. This talk discusses recent progress on the expressive power, decidability, and verification algorithms for such logics, with an emphasis on metric temporal formalisms and their extensions. We examine the relationships between metric temporal logic (MTL), its past‑time and Pnueli‑modality variants, and freeze‑time extensions that enable binding and comparing time values. I will briefly talk about expressive equivalence and separation theorems for these formalisms. On the algorithmic front, I will touch upon an automata‑based model‑checking procedure for MITL with past and Pnueli modalities over finite and infinite timed words. The corresponding implementation is significantly faster than the state-of-the-art MightyL tool on instances involving only future modalities.

Cyber‑physical systems (CPS), which integrate computational control with physical processes, require high reliability because they are often deployed in safety-critical domains. Ensuring that such systems satisfy their formal specifications is challenging, since modern CPS often contain complex or opaque components, such as deep neural networks, whose internal structures are not fully accessible. Black‑box checking (BBC) is a workflow for systematic testing of black‑box systems by approximating the system under test as an automaton by active automata learning and verifying the approximate automaton by model checking. This talk presents how to utilize BBC for specification-based testing of CPS, several techniques to improve its efficiency, and a Java toolkit FalCAuN for applying BBC of CPS. FalCAuN is publicly available: https://github.com/MasWag/FalCAuN. An extension of BBC for probabilistic systems will also be discussed.

The goal is to lift to the quantitative setting the famous equivalences between

1. Aperiodic languages (AP)
2. Star-free languages (SF)
3. Languages definable in first-order logic (FO)
4. Languages definable in linear temporal logic (LTL)

In this talk, we define weighted first-order logic (wFO) and aperiodic weighted automata (wA). We give examples showing that, surprisingly, aperiodic wA are more expressive than wFO over various classical semirings (natural numbers with (+,×) operations, or (min,+) operations, or (max,+) operations). To recover equivalence with wFO we have to restrict to polynomially ambiguous aperiodic wA. We also study fragments with lower ambiguity. Then, we introduce a weighted extension of linear temporal logic (wLTL). We discuss some of its properties and explain the difficulties that arise when trying to extend Kamp's theorem (FO=LTL) to the weighted setting.

Partially Observable Markov Decision Processes (POMDPs) are a central model for decision-making under uncertainty. While sampling-based techniques achieve scalability in solving them, they provide no formal correctness guarantees and are thus less suitable for safety-critical settings. Conversely, formal synthesis methods offer correctness by construction but typically do not scale to realistic POMDPs. To combine the strengths of these two approaches, we propose a synthesis framework that integrates sampling, automata learning, and model checking. Inspired by Angluin's L* algorithm, our approach uses sampling as a membership oracle and model checking as an equivalence oracle, enabling the synthesis of finite-state controllers with formal guarantees whenever the sampling-induced policy is regular. We establish a relative completeness result and demonstrate that our method effectively solves threshold-safety problems.

This talk is based on joint work (currently under submission) with Debraj Chakraborty (Nanyang Technological University, Singapore), Sayan Mukherjee (INRIA Rennes, France), and Jean-François Raskin (Université Libre de Bruxelles, Belgium).

The model checking problem for real-time systems asks whether a system (modelled as a network of automata) satisfies a logical specification. Metric Interval Temporal Logic (MITL) is one of the most widely used formalisms for expressing real-time properties, and a central challenge lies in obtaining efficient translations from MITL formulas to automata. Recently, we introduced Generalized Timed Automata (GTAs), a unified model that incorporates features of several established automata formalisms for real-time systems such as timed automata, event-clock automata, and automata with timers. Despite these powerful features, GTAs still support zone-based reachability and liveness with the same complexity as in classical timed automata.

In this talk, we present a new direct concise translation from MITL to GTAs. A key feature of our translation is that they are largely deterministic: the past fragment of MITL translates in linear time into synchronous networks of deterministic timed automata, while determinism is also preserved under certain top-level future modalities. Moreover, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. We implement our translation in a prototype tool which supports both satisfiability checking and model checking over finite and infinite timed words, and experimental evaluation demonstrates that it significantly outperforms the current state-of-the-art tool.

Weighted Model Integration (WMI) has emerged as a powerful unifying framework for probabilistic inference, allowing complex probabilistic reasoning tasks to be reduced to the integration of weight functions over regions defined by logical constraints. While existing WMI methods provide strong support for linear and polynomial weight functions, many real-world applications naturally give rise to rational or radical functions, for which current tools offer limited applicability and often no formal guarantees.

In this talk, I will present our recent work that significantly broadens the expressive reach of WMI by introducing a novel approximation algorithm that handles general semi-algebraic weight functions, including rational and radical forms. Our method leverages classical results from real algebraic geometry, like Farkas’ lemma and Handelman’s theorem, to reduce WMI queries to a sequence of linear programming problems, yielding an approximation with a formally controlled error bound that can be made arbitrarily small.

To illustrate the necessity of this extended expressiveness, I will discuss a simple example of Lévy flights used in describing asset price dynamics. Even in this simple probabilistic program, the inference queries naturally involve rational functions, highlighting the limitations of current polynomial-only methods and emphasizing the importance of our generalization.

This talk is based on our paper accepted at IJCAI 2025, a joint work with S. Akshay, Supratik Chakraborty, Soroush Farokhnia, Amir Goharshady, and Đorđe Žikelić.

Machine-learning models are increasingly being deployed in safety-critical and high-stakes environments- such as healthcare, finance, transportation, and legal decision-making- where even small errors can lead to serious real-world consequences. Thus, ensuring the reliability and trustworthiness of these models is essential to guarantee consistent and fair behavior.

In this talk, we present a data-aware and scalable framework for sensitivity analysis, which enables us to understand how model predictions change when specific input features vary and generate meaningful counterexamples. We then shift our focus to glitches, a newly identified class of output inconsistencies that reveal abrupt and unexpected behavior in ML models. Together, these methods enable us to formally reason about reliability in machine-learning systems and contribute to the pursuit of trustworthy AI.

Alternating Timed Automata (ATA) are an extension of timed automata where the effect of each transition is described by a positive boolean combination of (state-reset) pairs. Unlike classical timed automata, ATAs are closed under complementation and are therefore better suited for logic-to-automata translations. Several timed logics can be converted to equivalent 1-clock ATA (1-ATAs). But currently, model-checking tools do not use 1-ATAs directly for analysis, and instead use sophisticated conversions of logical fragments to timed automata. A reason for this could be that zone-based methods do not exist for 1-ATAs, unlike those extensively studied for timed automata.

In this talk, we present a direct zone-based algorithm for model-checking timed automata models against 1-ATA specifications. A key ingredient in zone-based algorithms is an entailment relation between zones that guarantees termination of the algorithm. We study this entailment relation closely, prove NP-hardness in general, and identify subclasses of models and specifications that result in a polynomial-time complexity.

This is joint work with Patricia Bouyer and B. Srivathsan.