Upgradation of Programmable Logic Controller (PLC) software is quite common to accommodate evolving industrial requirements. Verifying the correctness of such upgrades remains a significant challenge. In this paper, we propose a verification-based approach to ensure the correctness of the existing functionality in the upgraded version of a PLC software. The method converts the older and the newer versions of the sequential function chart (SFC) into two Petri net models. We then verify whether one model is contained within another, based on a novel containment checking algorithm grounded in symbolic path equivalence. For this purpose, we have developed a home-grown Petri net-based containment checker. Experimental evaluation on 80 real-world benchmarks from the OSCAT library highlights the scalability and effectiveness of the framework. We have compared our approach with verifAPS, a popular tool used for software upgradation, and observed nearly 4x performance improvement.
We present ERODE, a tool introduced in 2016 to analyze and reduce differential equations and chemical reaction networks. Over the years, it has been extended with further analysis and reduction techniques, as well as formalisms including differential algebraic equations, Boolean networks, networks, and Markov chains. ERODE can importexport towards several tools, including Matlab, BioNetGen, Modelica, PRISM, STORM, Stochkit, GINsim, SBML, and CoLoMoTo. It also has Python APIs.
This paper deals with the problem of runtime enforcement (RE) in the context of reactive systems, which consists in modifying the outputs of a system minimally to ensure its correctness. In contrast to enforcers that can postpone events via buffering, enforcers for reactive systems must operate within the same reactive cycle, always yielding a (possibly modified) output. For safety properties, an enforcer makes sure to satisfy the property at each step. However, for general regular properties, one can only expect to satisfy the property eventually. There is then a risk that even under enforcement the satisfaction is indefinitely delayed, and the property is never actually satisfied. Forcing the satisfaction of regular or ω -regular properties has been considered using bounded fairness and prompt eventuality. In this paper, we propose a new runtime enforcement framework for regular properties with prompt eventualities. Given an automaton specifying a property φ and a bound k, the enforcer should never falsify φ more than k consecutive steps. We formally define this RE problem, characterize k-enforceability of automata, and exhibit the construction of the enforcer. Rather than fixing k, we also study whether k can be computed to ensure k-enforceability or some maximal coverage of φ . We implement the k-prompt enforcement framework, and demonstrate its behaviour with varying k.
In this paper we tackle the problem of proving generic LTL properties of hybrid systems with a particular focus on liveness properties such as recurrence of regions, response to stimuli, or region stability. Although many advances have been made in the analysis of reachability and safety properties of dynamic and hybrid systems, there is a lack of tool support for the automated verification of liveness properties. We propose a fully automated approach that combines Lyapunov synthesis, reachability analysis, and SMT-based quantifier elimination to build a discrete abstraction and then applies standard model checking algorithms. A key step of the algorithm is the derivation of LTL constraints from reachable sets computations and Lyapunov-like certificates. We implemented the approach on top of the CORA and nuXmv tools and show how it can scale in the size of the discrete structure and how it can prove properties over linear and non-linear complex dynamics.
Petri nets are a modeling formalism capable of describing complex distributed systems and there exists a large number of both academic and industrial tools that enable automatic verification of model properties. Typical questions include reachability analysis and model checking against logics like LTL and CTL. However, these logics fall short when describing properties like non-interference and observational determinism that require simultaneous reasoning about multiple traces of the model and can thus only be expressed as hyperproperties. We introduce, to the best of our knowledge, the first HyperLTL model checker for Petri nets. The tool is fully integrated into the verification framework TAPAAL and we describe the semantics of the hyperlogic, present the tool's architecture and GUI, and evaluate the performance of the HyperLTL verification engine on a benchmark of problems originating from the computer networking domain.
Compositional automata learning is attracting attention as an analysis technique for complex black-box systems. It exploits a target system's internal compositional structure to reduce complexity. In this paper, we identify system integration -- the process of building a new system as a composite of potentially third-party and black-box components -- as a new application domain of compositional automata learning. Accordingly, we propose a new problem setting, where the learner has direct access to black-box components. This is in contrast with the usual problem settings of compositional learning, where the target is a legacy black-box system and queries can only be made to the whole system (but not to components). We call our problem componentwise automata learning for distinction. We identify a challenge there called component redundancies: some parts of components may not contribute to system-level behaviors, and learning them incurs unnecessary effort. We introduce a contextual componentwise learning algorithm that systematically removes such redundancies. We experimentally evaluate our proposal and show its practical relevance.
An energy game is played between two players, modeling a resource-bounded system and its environment. The players take turns moving a token along a finite graph. Each edge of the graph is labeled by an integer, describing how its traversal affects the energy level of the system. The system wins if it never runs out of energy. We introduce and study energy games with weight uncertainty (EGWUs), where the exact updates to the energy level are not a-priori known to the system. Instead, an EGWU specifies, for some subsets of edges, upper and lower bounds for their joint weight. EGWUs thus model settings in which there is only an estimation of the effect of some actions or sets of actions on the energy level, for example due to uncertainty about road conditions for an autonomous car or about the location of docking stations for a robot patrolling a warehouse. The system wins an EGWU if it has a strategy to never run out of energy, no matter what the weights are, as long as they respect the bounds. The environment wins if there are weights that respect the bounds with which it can cause the system to run out of energy. Unlike uncertainty about the exact location of the token, which persists during the interaction, the weight of an edge is revealed upon its traversal. The fact the system learns the weights during the interaction makes EGWUs interesting, and we study the memory required to the players, determinacy of the game, and the possibility of coping with uncertainty by a larger initial energy. We give tight complexity bounds to the problems of deciding whether the system or the environment wins, and we study the effect of parameters like the richness of the function estimating the weights, or the distribution of control along the interaction
This invited paper unifies our recent work on the automated synthesis of strategy templates as robust certified interfaces for interacting autonomous systems. Strategy templates are similar to classical strategies typically computed by reactive software synthesis but contain a huge set of relevant strategies in a succinct and simple data structure. This permissiveness allows efficient adaptations to new specifications as well as robustness to unexpected actuation failures during runtime. In addition to these favorable engineering properties of strategy templates for cyber-physical systems (CPS), their permissiveness, efficient computability, and adaptability enables their use for the automated synthesis of certified interfaces among different interacting CPS. This paper discusses the foundations and applications of this novel control-inspired distributed reactive synthesis framework for different cooperation and partial-observation settings common for interacting CPS.
Creating meaningful interpretations for black-box machine learning models involves balancing two often conflicting objectives: accuracy and explainability. Exploring the trade-off between these objectives is essential for developing trustworthy interpretations. While many techniques for multi-objective interpretation synthesis have been developed, they typically lack formal guarantees on the Pareto-optimality of the results. Methods that do provide such guarantees, on the other hand, often face severe scalability limitations when exploring the Pareto-optimal space. To address this, we develop a framework based on local optimality guarantees that enables more scalable synthesis of interpretations. Specifically, we consider the problem of synthesizing a set of Pareto-optimal interpretations with local optimality guarantees, within the immediate neighborhood of each solution. Our approach begins with a multi-objective learning or search technique, such as Multi-Objective Monte Carlo Tree Search, to generate a best-effort set of Pareto-optimal candidates with respect to accuracy and explainability. We then verify local optimality for each candidate as a Boolean satisfiability problem, which we solve using a SAT solver. We demonstrate the efficacy of our approach on a set of benchmarks, comparing it against previous methods for exploring the Pareto-optimal front of interpretations. In particular, we show that our approach yields interpretations that closely match those synthesized by methods offering global guarantees.
Precise and comprehensive situational awareness is a critical capability of modern autonomous systems. Deep neural networks that perceive task-critical details from rich sensory signals have become ubiquitous; however, their black-box behavior and sensitivity to environmental uncertainty and distribution shifts make them challenging to verify formally. Abstraction-based verification techniques for visionbased autonomy produce safety guarantees contingent on rigid assumptions, such as bounded errors or known unique distributions. Such overly restrictive and inflexible assumptions limit the validity of the guarantees, especially in diverse and uncertain test-time environments. We propose a methodology that unifies the verification models of perception with their offline validation. Our methodology leverages interval MDPs and provides a flexible end-to-end guarantee that adapts directly to the outof-distribution test-time conditions. We evaluate our methodology on a synthetic perception Markov chain with well-defined state estimation distributions and a mountain car benchmark. Our findings reveal that we can guarantee tight yet rigorous bounds on overall system safety. Code: https://github.com/Trustworthy- Engineered- Autonomy- Lab/ unified- perception-vnv.
For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components—a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle—a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.
This paper introduces the notion of control closure certificates ( C^3 ) to synthesize controllers for discrete-time control systems against ω -regular specifications. Typical functional approaches to synthesize controllers against ω -regular specifications rely on combining inductive invariants (for example, via barrier certificates) with proofs of well-foundedness (for example, via ranking functions). Transition invariants, provide an alternative where instead of standard well-foundedness arguments one may instead search for disjunctive well-foundedness arguments that together ensure a well-foundedness argument. Closure certificates, functional analogs of transition invariants, provide an effective, automated approach to verify discrete-time dynamical systems against linear temporal logic and ω -regular specifications. We build on this notion to synthesize controllers to ensure the satisfaction of ω -regular specifications. To do so, we first illustrate how one may construct control closure certificates to visit a region infinitely often (or only finitely often) via disjunctive well-founded arguments. We then combine these arguments to provide an argument for parity specifications. Thus, finding an appropriate C^3 over the product of the system and a parity automaton specifying a desired ω -regular specification ensures that there exists a controller κ to enforce the ω -regular specification. We propose a sum-of-squares optimization approach to synthesize such certificates and demonstrate their efficacy in designing controllers over some case studies.
This paper presents a state-merging algorithm for learning timed languages definable by Event-Recording Automata (ERA) using positive and negative samples in the form of symbolic timed words. Our algorithm, LEAP (Learning Event-recording Automata Passively), constructs a possibly nondeterministic ERA from such samples based on merging techniques. We prove that determining whether two ERA states can be merged while preserving sample consistency is an NP-complete problem, and address this with a practical SMT-based solution. Our implementation demonstrates the algorithm's effectiveness through examples. We also show that every ERA-definable language can be inferred using our algorithm with a suitable sample.
As physical realizations of quantum computers move closer towards practical applications, the need for tools to analyze and verify quantum algorithms grows. Among the algorithms and data structures used to tackle such problems, decision diagrams (DDs) have shown much success. However, an obstacle with DDs is their efficient parallelization, and while parallel speedups have been obtained for DDs used in classical applications, attempts to parallelize operations for quantum-specific DDs have yielded only limited success. In this work, we present an efficient implementation of parallel edge-valued DDs, which makes use of fine-grained task parallelism and lock-free hash tables. Additionally, we use these DDs to implement two use cases: simulation and equivalence checking of quantum circuits. In our empirical evaluation we find that our tool, Q-Sylvan, shows a single-core performance that is competitive with the state-of-the-art quantum DD tool MQT DDSIM on large instances, and moreover achieves parallel speedups of up to x18 on 64 cores.
Branch and Bound (BaB) is considered as the most efficient technique for DNN verification: it can propagate bounds over numerous branches, to accurately approximate values a given neuron can take even in large DNNs, enabling formal verification of properties such as local robustness. Nevertheless, the number of branches grows exponentially with important variables, and there are complex instances for which the number of branches is too large to handle even using BaB. In these cases, providing more time to BaB is not efficient, as the number of branches treated is linear with the time-out. Such cases arise with verification-agnostic DNNs, non-local properties (e.g. global robustness, computing Lipschitz bound), etc. To handle complex instances, we revisit a divide-and-conquer approach to break down the complexity: instead of few complex BaB calls, we rely on many small partial MILP calls. The crucial step is to select very few but very important ReLUs to treat using (costly) binary variables. The previous attempts were suboptimal in that respect. To select these important ReLU variables, we propose a novel solution-aware ReLU scoring (SAS), as well as adapt the BaB-SR and BaB-FSB branching functions as global ReLU scoring (GS) functions. We compare them theoretically as well as experimentally, and SAS is more efficient at selecting a set of variables to open using binary variables. Compared with previous attempts, SAS reduces the number of binary variables by around 6 times, while maintaining the same level of accuracy. Implemented in Hybrid MILP, calling first α ,β -CROWN with a short time-out to solve easier instances, and then partial MILP, produces a very accurate yet efficient verifier, reducing by up to 40% the number of undecided instances to low levels ( 8-15% ), while keeping a reasonable runtime ( 46s-417s on average per instance), even for fairly large CNNs with 2 million parameters.
Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety requirement changes at runtime due to changing operating conditions, the shield needs to be recomputed from scratch, causing delays that could be fatal. We introduce dynamic shields for parametric safety specifications, which are succinctly represented sets of all possible safety specifications that may be encountered at runtime. Our dynamic shields are statically designed for a given safety parameter set, and are able to dynamically adapt as the true safety specification (permissible by the parameters) is revealed at runtime. The main algorithmic novelty lies in the dynamic adaptation procedure, which is a simple and fast algorithm that utilizes known features of standard safety shields, like maximal permissiveness. We report experimental results for a robot navigation problem in unknown territories, where the safety specification evolves as new obstacles are discovered at runtime. In our experiments, the dynamic shields took a few minutes for their offline design, and took between a fraction of a second and a few seconds for online adaptation at each step, whereas the brute-force online recomputation approach was up to 5 times slower.
This paper presents (permissive) Quantitative Strategy Templates (QaSTels) to succinctly represent infinitely many winning strategies in two-player energy and mean-payoff games. This transfers the recently introduced concept of Permissive (qualitative) Strategy Templates (PeSTels) for ω -regular games to games with quantitative objectives. We provide the theoretical and algorithmic foundations of (i) QaSTel synthesis, and (ii) their (incremental) combination with PeSTels for games with mixed quantitative and qualitative objectives. Using a prototype implementation, we demonstrate empirically that QaSTels extend the advantageous properties of strategy templates over single winning strategies – known from PeSTels – to games with (additional) quantitative objectives. This includes (i) the enhanced robustness of strategies due to their runtime-adaptability, and (ii) the compositionality of templates w.r.t. incrementally arriving objectives. We use control-inspired examples to illustrate these superior properties of QaSTels for CPS design.
Runtime monitors assess whether a system is in an unsafe state based on a stream of observations. We study the problem where the system is subject to probabilistic uncertainty and described by a hidden Markov model. A stream of observations is then unsafe if the probability of being in an unsafe state is above a threshold. A correct monitor recognizes the set of unsafe observations. The key contribution of this paper is the first correct-by-construction synthesis method for such monitors, represented as finite automata. The contribution combines four ingredients: First, we establish the coNP-hardness of checking whether an automaton is a correct monitor, i.e., a monitor without misclassifications. Second, we provide a reduction that reformulates the search for misclassifications into a standard probabilistic system synthesis problem. Third, we integrate the verification routine into an active automata learning routine to synthesize correct monitors. Fourth, we provide a prototypical implementation that shows the feasibility and limitations of the approach on a series of benchmarks.
Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with constants. The parameters allow encoding dependencies between transitions, which sets pMCs apart from interval MCs. The verification problem for pMCs asks whether each MC in the corresponding family satisfies a given temporal specification. The state-of-the-art approach for this problem is parameter lifting (PL) -- an abstraction-refinement loop that abstracts the pMC to a non-parametric model analyzed with standard probabilistic model checking techniques. This paper presents two key improvements to tackle the main limitations of PL. First, we introduce generalized parameter lifting (GPL) to lift various restrictive assumptions made by PL. Second, we present a big-step transformation algorithm that reduces parameter dependencies in pMCs and, therefore, results in tighter approximations. Experiments show that GPL is widely applicable and that the big-step transformation accelerates pMC verification by up to orders of magnitude.
