Uncertainties occur in different forms: data may be noisy, mechanisms may be inherently randomised, the visibility (of e.g. a robot) may not be optimal, and the environment in which a system needs to operate may behave in an unknown manner. The central question that we will address is “Can we guarantee that AI systems are safe and resilient in the presence of such uncertainty?” We advocate using model-based, formal verification and synthesis with a particular focus on automation. We will present techniques to (a) verify uncertainty aspects modeled as randomness and to (b) use formal synthesis to complete partial designs. Several example AI models—Bayesian networks, partially observable Markov decision processes, and probabilistic programs – will illustrate the capabilities of these approaches.
Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.
Compared to semantics with preemptively executing threads, ones with cooperative threads permit easier specification of atomicity in concurrent programs. We introduce a semantics of cooperative programs, and a simulation notion compatible with rely-guarantee proofs. We prove our simulation composes in parallel and sequentially, and that it can establish a standard trace-based notion of refinement.
Runtime verification of temporal properties over timed observations is essential in cyber-physical systems such as autonomous vehicles, smart grids, and medical devices. This talk presents recent advances in predicting property satisfaction or violation in continuous real-time settings. We focus on monitoring properties expressed in Metric Interval Temporal Logic (MITL) or Timed Büchi Automata [2, 4]. Our symbolic online algorithms exploit zone-based techniques from Timed Automata model checking, enabling efficient handling of challenges like time divergence, timing uncertainty, and fluctuating parametric delays–without relying on costly parametric verification. Assumptions about system behavior, expressed as Timed Automata, can further enhance monitoring [1]. We propose an assumption-based runtime verification framework and discuss its extension to probabilistic settings using Stochastic Timed Automata. Implemented in UPPAAL, our algorithms show promising initial results. Finally [3], we also present new findings on monitorability, showing decidability and computable verdict bounds for deterministic Timed Muller Automata, while proving undecidability for nondeterministic Timed Büchi Automata. In addition we introduce and settle decidability of step- and time-bounded monitorability.
We present a summary of a domain analysis description method. Domains are the realm in which [large scale] software is embedded – in order to serve human actions in predominantly man-made “surroundings”. The method, with its principles, procedures, techniques and tools, are outlined. A main principle is that of delineating observable phenomena into describable entities; these into endurants and perdurants, i.e., roughly speaking “statically” and “dynamically” observable entities; entities into endurants and perdurants; endurants into solids and fluids; solids into parts and living species; parts into atomic and compound parts; and compound parts into Cartesians and part sets. Endurants are then “endowed” with unique identities, mereologies, attributes and intentional “pull”. Endurants are then, by transcendental deduction, “morphed” into perdurants: behaviours that communicate, and where unique identities, mereologies and attributes serve as possible updateable behaviour arguments.
Ulam’s metric defines the minimal number of moves (extraction followed by re-insertion of permutation elements) to go between a given pair of permutations, and determination of moved elements resolves the Longest Common Subsequence problem. The extensive research that followed Ulam’s work provided many influential discoveries in computer science, mathematics, statistics and physics. In this paper, motivated by successful industrial applications of k-tuples of permutations, we extend Ulam’s original definition to provide a framework of multidimensional metric and study its complexity and approximability.
We generalize the classic multi-agent DeGroot framework for opinion dynamics by incorporating the Spiral of Silence theory from political science, which posits that individuals may withhold their opinions when they perceive them to be in the minority. As in the original DeGroot model, the social network is represented as a weighted directed graph encoding how agents influence one another. However, agents holding minority opinions become silent, meaning they do not express their views. We introduce two families of models. In Silence Opinion Memoryless ( SOM^- ) models, agents update their opinions by averaging those of their non-silent neighbors. In Silence Opinion Memory-based ( SOM^+ ) models, agents average the opinions of all neighbors, but for silent ones, only the most recently expressed opinion is used. We show that SOM^- models guarantee consensus on clique graphs but, unlike the classic DeGroot model, not on all strongly connected aperiodic graphs. For SOM^+ models, even cliques may fail to reach consensus, illustrating that even minimal memory can significantly affect opinion dynamics. Finally, we validate our models through large-scale simulations on small-world networks with over two million agents. The results support the Spiral of Silence theory and reveal inherent limitations to consensus in more realistic settings.
Unfolding colored Petri nets into place/transition (P/T) nets is a standard approach for model-checking, leveraging established tools and techniques for basic Petri nets. However, the unfolding process often leads to a combinatorial explosion in the number of places and transitions, creating a significant bottleneck in analyzing complex colored Petri nets. We introduce a new verification engine for Petri nets with finite color domains that bypasses the costly unfolding process. Our engine employs an explicit, on-the-fly state-space exploration, utilizing an optimized binding generator and linear programming-based approximation techniques to enhance performance. Integrated into the open-source TAPAAL model checker, our engine is evaluated on an extensive benchmark from the Model Checking Contest (MCC) 2024. It demonstrates superior performance over the state-of-the-art unfolding approaches.
Craig interpolation is a foundational concept in logic with broad applications in formal verification, automated reasoning, and modular system design. While Maehara’s lemma enables interpolant extraction from cut-free proofs, extending interpolation to proofs with cuts has remained challenging. In this paper, we propose a generalization of Maehara’s lemma to admissible cuts – a class of cut-formulas satisfying structural constraints defined via end-sequent partitions. Our approach leverages the Ceres cut-elimination framework to identify cut-free components critical for interpolation. We show that this method not only generalizes previous results on atomic cuts but also reduces the asymptotic complexity of interpolant extraction from cubic to quadratic, thus enhancing the scalability of interpolation techniques in proof-theoretic reasoning.
The Lean proof assistant features a typechecker kernel that makes use of a set of “definitional equalities” for identifying terms under certain syntactic and typing conditions. While providing for convenient formalization, some definitional equalities in particular complicate meta-theoretical analyses and the export of Lean proofs to other proof assistants via logical frameworks such as Dedukti. In this paper, we describe a translation from Lean to a smaller theory “ Lean^- ” with fewer such definitional equalities, specifically eliminating uses of proof irrelevance and “K-like reduction” in the typing of Lean terms. We adapt a general translation from extensional to intensional type theory, making Lean’s implicit use of these definitional equalities explicit through the use of type casts and a corresponding proof irrelevance axiom. The translation has been implemented in Lean itself in a tool called Lean4Less ( https://github.com/rish987/Lean4Less ), which is able to successfully translate certain libraries (e.g. the Lean standard library) to Lean^- . The methods developed for this translation may also be transferrable to other proof assistants based on dependent type theory.
Testing is in practice commonly performed by executing carefully planned scripts, which exercise particular planned scenarios. Fuzz testing can be applied as a complementary approach, to exercise a system outside the boundaries of the expected. However, fuzz testing can be too random. In this work, we explore an approach to fuzz testing using an expressive temporal logic named MaTL (Matching Temporal Logic) for expressing constraints on tests, restricting generated tests to only such that satisfy the provided constraints. MaTL is a linear temporal logic that supports future and past time operators and a match construct that selects argument values from events, similar to pattern matching in functional programming languages. Constraint solving is performed using the Z3 SMT solver.
Contract theory is an appealing framework for rigorous component-based design of highly dynamic and distributed cyber-physical systems. Formally, a contract is a specification consisting of pairs of assumptions and guarantees. A guarantee describes the task that the component must fulfill when its environment (made of other components and of the external environment) satisfies the associated assumption. Assume-guarantee contracts make it possible to design components that can adapt under dynamic and uncertain working conditions. Moreover, compositional reasoning makes it possible to prove properties of a system based on the contracts satisfied by its components. In this presentation, we will explore the connections between assume-guarantee contracts and set invariance, a concept which forms one of the cornerstones of modern control theory. We will introduce a class of assume-guarantee contracts whose satisfaction can be characterized through invariant sets of an auxiliary dynamical system. We will discuss theoretical and computational aspects of the proposed framework and show illustrative applications in the design of hierarchical and distributed control systems.
In card-based cryptography for performing secure computation, after each player places an input commitment consisting of two face-down cards, all players cooperate to manipulate a sequence of cards according to a protocol. In the presence of a malicious player who does not follow the protocol, prior work has considered the active card-revealing attack and defined the t-secureness as the ability to prevent information about the input from being leaked even if at most t cards are turned over illegally. In this paper, we first propose an efficient 1-secure AND protocol: our proposed protocol uses only eight cards and one shuffle, whereas the existing protocol requires 16 cards and eight shuffles. Our 1-secure AND protocol is quite simple and easy to implement. We next design a committed-format 1-secure AND protocol by adding four more cards; a committed-format protocol produces its output in the same format as its inputs.
Ensuring the safe operation of neural network-controlled systems in the presence of uncertain measurements is a critical challenge. Inaccurate state estimation can lead to unsafe controller behavior, necessitating safety guarantees that can effectively handle measurement errors. Existing methods rely on pre-determining the measurement error bound ϵ and synthesizing ϵ -robust barrier certificates based on this bound. However, in practical applications, ϵ is often unavailable during the design phase, which limits the applicability of existing techniques. This paper addresses the problem from a novel perspective by proposing an iterative method for synthesizing robust barrier certificates. First, we synthesize a barrier certificate for a given system, and then the maximum tolerable error bound and the most vulnerable region is calculated through an optimization problem. Second, we design an iterative optimization framework that progressively strengthens the barrier certificate by repairing its most vulnerable regions, resulting in certificates with increasingly larger tolerable error bounds. Experiments on benchmark examples demonstrate that the proposed approach can generate barrier certificates that are more robust than those of state-of-the-art work.
Cyber-Physical Systems (CPSs) are increasingly used in safety-critical tasks like search and rescue missions. They are often combined with machine-learning algorithms like Reinforcement Learning (RL) for improved performance and accuracy. There is a pressing need to ensure the safety of such learning-enabled CPSs. In recent research, the Runtime Enforcement (RE) approach has been very successful in formally ensuring the safety of learning-enabled CPS. RE is a formal verification technique that dynamically guarantees the safety of a system. We present a runtime enforcement mechanism for safeguarding a Multi-Agent Reinforcement Learning (MARL) enabled drone swarm CPS. We discuss the enforcement strategies that prevent drones from collision and boundary breach. We show how RE combined with MARL, in addition to guaranteeing safety, improves the overall performance of the swarm system.
Complex coordination protocols are necessary to manage complex organisations. The healthcare management sector is no exception, since different authorities, users, and systems have to interact with each other in order to achieve their organisational goals. In this paper we consider a case study on the authorisation and accreditation of healthcare structures in the Emilia Romagna region in Italy. We specify the case study using global choreographies so to enable the analysis of the correctness of its communication patterns using the tool. This requires to refine and its underlying theoretical framework. First, we extend to support not only asynchronous communication, but also synchronous one. Moreover, in both the cases, we provide a more efficient algorithm to check closure properties ensuring realisability of choreographies. The new algorithm allows us to check realisability of larger pomsets than before, which makes our approach viable for complex systems such as our case study.
Ordered matchings, defined as graphs with linearly ordered vertices, where each vertex is connected to exactly one edge, play a crucial role in the area of ordered graphs and their homomorphisms. Therefore, we consider related problems from the complexity point of view and determine their corresponding computational and parameterized complexities. We show that the subgraph of ordered matchings problem is NP-complete and we prove that the problem of finding ordered homomorphisms between ordered matchings is NP-complete as well, implying NP-completeness of more generic problems. In parameterized complexity setting, we consider a natural choice of parameter - a number of vertices of the image ordered graph. We show that in contrast to the complexity context, finding homomorphisms if the image ordered graph is an ordered matching, this problem parameterized by the number of vertices of the image ordered graph is FPT, which is known to be W[1]-hard for the general problem. We also determine that the problem of core for ordered matchings is solvable in polynomial time which is again in contrast to the NP-completeness of the general problem. We provide several algorithms and generalize some of these problems into ordered graphs with colored edges.
Multiparty session types (MPST) are a robust typing framework that ensures safe and deadlock-free communication within distributed protocols. As these protocols grow in complexity, compositional modeling becomes increasingly important for scalable verification. Therefore, we propose using refinement through subtyping to facilitate the modularity needed for compositional verification. We present a probabilistic extension for MPST with a novel, flexible subtyping system which allows one channel (the interface) to be substituted by several channels (the refinement). Our subtyping is very expressive; any selection of well-typed channels as the refinement has a corresponding interface in a single channel type. To facilitate this generality, we base our system on a powerful variant of MPST, mixed choice multiparty session types, which offers greater flexibility in communication choices.
We propose ^*_M —an active learning algorithm that learns symbolic Mealy automata, which support infinite input alphabets and multiple output characters. Each of these two features has been addressed separately in prior work. Combining these two features poses a challenge in learning the outputs corresponding to potentially infinite sets of input characters at each state. To address this challenge, we introduce the notion of essential input characters, a finite set of input characters that is sufficient to learn the output function of a symbolic Mealy automaton. ^*_M maintains an underapproximation of the essential input characters and refines this set during learning. We prove that ^*_M terminates under certain assumptions. Moreover, we provide upper and lower bounds for the query complexity. Their similarity suggests the tightness of the bounds. We empirically demonstrate that ^*_M is i) efficient regarding the number of queries on practical benchmarks and ii) scalable according to evaluations with randomly generated benchmarks.
