Complete formal verification of neural networks is crucial for their deployment in safety-critical domains. A key bottleneck stems from encoding complexity: traditional methods assign one binary variable per unstable ReLU neuron. We propose the Sign-Absolute Reformulation Theory (SART), which fundamentally breaks the conventional one-to-one mapping between unstable neurons and binary variables by establishing formal reducibility criteria. This allows for finer-grained modeling, where each unstable neuron corresponds on average to fewer than one binary variable, thereby reducing verification complexity at its source. Based on SART, we derive a theoretical lower bound on the number of binary variables required for complete verification and, under the assumption that 𝑃 ≠ 𝑁𝑃, prove that variables in the final layer can be compressed by 50%, while the number of variables in intermediate layers cannot be further reduced. To overcome the apparent “last-layer-only” limitation, we recast verification as a sequential process and, crucially, show that the gain lifts to the entire network: LayerABS, a SART-based progressive tightening verifier, iteratively treats intermediate layers as temporary final layers and propagates tight bounds that shrink the global search space and binaryvariable counts. Furthermore, we reveal a structural law influencing verification complexity: when the signs of weights of unstable neurons satisfy numerical symmetry, with positive and negative weights equal or differing by at most one, the worst-case verification complexity achieves the theoretical optimum, offering theoretical guidance for the design of verification-friendly architectures. As a general-purpose underlying encoding, the value of SART is independent of specific algorithms. To comprehensively evaluate its effectiveness, we first evaluate the abstraction-free SART encoding, and then integrate it with abstraction techniques to construct the complete verifier LayerABS and its incomplete variant Incomplete-LayerABS. Across benchmarks, our methods surpass state-of-the-art baselines, validating SART’s practical impact.

Abstract Simulation-based compositional abstraction effectively mitigates state space explosion in model checking, particularly for timed systems. However, existing approaches do not support broadcast synchronization, an important mechanism for modeling non-blocking one-to-many communication in multi-component systems. Consequently, they also lack a parallel composition operator that simultaneously supports broadcast synchronization, binary synchronization, shared variables, and committed locations. To address this, we propose a simulation-based compositional abstraction framework for timed systems, which supports these modeling concepts and is compatible with the popular UPPAAL model checker. Our framework is general, with the only additional restriction being that the timed automata are prohibited from updating shared variables when receiving broadcast signals. Through two case studies, our framework demonstrates superior verification efficiency compared to traditional monolithic methods.

In real-time and safety-critical cyber-physical systems (CPSs), control synthesis must guarantee that generated policies meet stringent timing and correctness requirements under uncertain and dynamic conditions. Signal temporal logic (STL) has emerged as a powerful formalism of expressing realtime constraints, with its semantics enabling quantitative assessment of system behavior. Meanwhile, reinforcement learning (RL) has become an important method for solving control synthesis problems in unknown environments. Recent studies incorporate STL-based reward functions into RL to automatically synthesize control policies. However, the automatically inferred rewards obtained by these methods represent the global assessment of a whole or partial path but do not accumulate the rewards of local changes accurately, so the sparse global rewards may lead to non-convergence and unstable training performances. In this paper, we propose an online reward generation method guided by the online causation monitoring of STL. Our approach continuously monitors system behavior against an STL specification at each control step, computing the quantitative distance toward satisfaction or violation and thereby producing rewards that reflect instantaneous state dynamics. Additionally, we provide a smooth approximation of the causation semantics to overcome the discontinuity of the causation semantics and make it differentiable for using deep-RL methods. We have implemented a prototype tool and evaluated it in the Gym environment on a variety of continuously controlled benchmarks. Experimental results show that our proposed STL-guided RL method with online causation semantics outperforms existing relevant STLguided RL methods, providing a more robust and efficient reward generation framework for deep-RL.

Timed regular expressions serve as a formalism for specifying real-time behaviors of Cyber-Physical Systems. In this paper, we consider the synthesis of timed regular expressions, focusing on generating a timed regular expression consistent with a given set of system behaviors including positive and negative examples, i.e., accepting all positive examples and rejecting all negative examples. We first prove the decidability of the synthesis problem through an exploration of simple timed regular expressions. Subsequently, we propose our method of generating a consistent timed regular expression with minimal length, which unfolds in two steps. The first step is to enumerate and prune candidate parametric timed regular expressions. In the second step, we encode the requirement that a candidate generated by the first step is consistent with the given set into a Satisfiability Modulo Theories (SMT) formula, which is consequently solved to determine a solution to parametric time constraints. Finally, we evaluate our approach on benchmarks, including randomly generated behaviors from target timed models and a case study.

We present an algorithm for active learning of deterministic timed automata with multiple clocks. The algorithm is within the querying framework of Angluin’s L* algorithm and follows the idea proposed in existing work on the active learning of deterministic one-clock timed automata. We introduce an equivalence relation over the reset-clocked language of a timed automaton and then transform the learning problem into learning the corresponding reset-clocked language of the target automaton. Since a reset-clocked language includes the clocks reset information which is not observable, we first present the approach of learning from a powerful teacher who can provide reset information by answering reset information queries from the learner. Then we extend the algorithm in a normal teacher situation in which the learner can only ask standard membership query and equivalence query while the learner guesses the reset information. We prove that the learning algorithm terminates and returns a correct deterministic timed automaton. Due to the need of guessing whether the clocks reset at the transitions, the algorithm is of exponential complexity in the size of the target automaton.

Abstract Compositional verification, such as the technique of assume-guarantee reasoning (AGR), is to verify a property of a system from the properties of its components. It is essential to address the state explosion problem associated with model checking. However, obtaining the appropriate assumption for AGR is always a highly mental challenge, especially in the case of timed systems. In this paper, we propose a learning-based compositional verification framework for deterministic timed automata. In this framework, a modified learning algorithm is used to automatically construct the assumption in the form of a deterministic one-clock timed automaton, and an effective scheme is implemented to obtain the clock reset information for the assumption learning. We prove the correctness and termination of the framework and present two kinds of improvements to speed up the verification. We discuss the results of our experiments to evaluate the scalability and effectiveness of the framework. The results show that the framework we propose can reduce state space effectively, and it outperforms traditional monolithic model checking for most cases.

In recent years, machine learning has demonstrated impressive performance in many real-world tasks, especially in computer vision and natural language processing.However, to apply them in safety-critical systems one needs formal guarantees on the neural network outputs.The Reluplex tool is proposed to verify the safety of deep neural networks (DNNs), and in case the DNN fails to give a correct output, can generate adversarial examples.Since the tool can only handle DNNs, it is necessary to extend the tool to process image data.Therefore, in this paper, we propose the Conv-Reluplex framework, which is designed to verify the convolutional layer and pooling layer in convolutional neural networks(CNNs), and generate adversarial examples when classification is misguided.We conduct several experiments on MNIST to evaluate our approaches.The results show that the original CNN is improved using the adversarial examples generated by our tool, and the precision of classification can be increased significantly.

Abstract Identification of dynamical and hybrid systems using trajectory data is an important way to construct models for complex systems where derivation from first principles is too difficult. In this paper, we study the identification problem for switched dynamical systems with polynomial ODEs. This is a difficult problem as it combines estimating coefficients for nonlinear dynamics and determining boundaries between modes. We propose two different algorithms for this problem, depending on whether to perform prior segmentation of trajectories. For methods with prior segmentation, we present a heuristic segmentation algorithm and a way to classify themodes using clustering. Formethods without prior segmentation, we extend identification techniques for piecewise affine models to our problem. To estimate derivatives along the given trajectories, we use Linear MultistepMethods. Finally, we propose a way to evaluate an identified model by computing a relative difference between the predicted and actual derivatives. Based on this evaluation method, we perform experiments on five switched dynamical systems with different parameters, for a total of twenty cases. We also compare with three baseline methods: clustering with DBSCAN, standard optimization methods in SciPy and identification of ARX models in Matlab, as well as with state-of-the-art identification method for piecewise affine models. The experiments show that our two methods perform better across a wide range of situations.

We present an active learning algorithm named NRTALearning for nondeterministic real-time automata (NRTAs). Real-time automata (RTAs) are a subclass of timed automata with only one clock which resets at each transition. First, we prove the corresponding Myhill-Nerode theorem for real-time languages. Then we show that there exists a unique minimal deterministic real-time automaton (DRTA) recognizing a given real-time language, but the same does not hold for NRTAs. We thus define a special kind of NRTAs, named residual real-time automata (RRTAs), and prove that there exists a minimal RRTA to recognize any given real-time language. This transforms the learning problem of NRTAs to the learning problem of RRTAs. After describing the learning algorithm in detail, we prove its correctness and polynomial complexity. In addition, based on the corresponding Myhill-Nerode theorem, we extend the existing active learning algorithm NL* for nondeterministic finite automata to learn RRTAs. We evaluate and compare the two algorithms on two benchmarks consisting of randomly generated NRTAs and rational regular expressions. The results show that NRTALearning generally performs fewer membership queries and more equivalence queries than the extended NL* algorithm, and the learnt NRTAs have much fewer locations than the corresponding minimal DRTAs. We also conduct a case study using a model of scheduling of final testing of integrated circuits.

In recent years, Deep Neural Networks (DNNs) have been experiencing rapid development and have been widely used in various fields. However, while DNNs have shown strong capabilities, their security problems have gradually been exposed. Therefore, the formal guarantee of neural network output is needed. Prior to the appearance of the Reluplex algorithm, the verification of DNNs was always a difficult problem. Reluplex algorithm is specially used to verify DNNs with ReLU activation function. This is an excellent and effective algorithm, but it cannot verify more activation functions. ReLU activation function will bring about "Dead Neuron" problem, and Leaky ReLU activation function can solve this problem, so it is necessary to verify DNNs based on Leaky ReLU activation function. Therefore, we propose the Leaky-Reluplex algorithm, which is based on the Reluplex algorithm. Leaky-Reluplex algorithm can verify DNNs based on Leaky ReLU activation function.

We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin’s $$L^*$$ algorithm and inspired by existing work on the active learning of symbolic automata. Due to the need of guessing for each transition whether it resets the clock, the algorithm is of exponential complexity in the size of the learned automata. Before presenting this algorithm, we propose a simpler version where the teacher is assumed to be smart in the sense of being able to provide the reset information. We show that this simpler setting yields a polynomial complexity of the learning process. Both of the algorithms are implemented and evaluated on a collection of randomly generated examples. We furthermore demonstrate the simpler algorithm on the functional specification of the TCP protocol.

In this article, we present a novel model checking approach to finite-time safety verification of black-box continuous-time dynamical systems within the framework of probably approximately correct (PAC) learning. The black-box dynamical systems are the ones, for which no model is given but whose states changing continuously through time within a finite-time interval can be observed at some discrete-time instants for a given input. The new model checking approach is termed as the PAC model checking due to the incorporation of learned models with correctness guarantees expressed using the terms error probability and confidence. Based on the error probability and confidence level, our approach provides statistically formal guarantees that the time-evolving trajectories of the black-box dynamical system over finite-time horizons fall within the range of the learned model plus a bounded interval, contributing to insights on the reachability of the black-box system and thus on the satisfiability of its safety requirements. The learned model together with the bounded interval is obtained by scenario optimization, which boils down to a linear programming problem. Three examples demonstrate the performance of our approach.

As a widely used modeling language, AADL (Architecture Analysis and Design Language) plays an important role in designing safety-critical systems. It provides abundant components for describing system architecture and supports the early prediction and repetitive analysis of performance-critical attributes. However, the approach used by AADL to describe the system behavior is based mainly on automata theory; thus, encountering the state space explosion problem when modeling and verifying large and complex systems is inevitable. Furthermore, due to the lack of means to describe the behavior details, it is also difficult for AADL to support the accurate analysis and verification of functional and non-functional requirements. In this paper, we propose a language called RBML that supports refined behavior modeling to compensate for the behavior modeling and verification deficiencies of AADL. This new language is based on AADL but extends the ability to detail various behaviors and allows SMT (Satisfiability Modulo Theories) solvers to verify the constructed refined behavior model, thus alleviating the state space explosion problem to some extent. Experiments on Baidu Apollo are presented to demonstrate the feasibility of our proposed approach.

Neural network is one of the key technologies for deep learning. Experiments on some standard test datasets show that their recognition ability has reached the level of human beings. However, they are extremely vulnerable to adversarial examples, that is, adding some subtle perturbations to the input example can cause the model to give a wrong output with high confidence. In this paper, we propose a non-contact approach based on neural network and adversarial training to recognize the high-speed rail operating environment. We first built the environment dataset and trained neural network models to do the recognition. We found that our model had high prediction accuracy, but with poor security since it was easy to attack our model using Basic Iterative Methods (BIM). To improve its security, we performed adversarial training based on the adversarial training dataset we built. The evaluation experiments indicated that this approach could improve the security of our model at the same time ensuring the prediction accuracy on the original test dataset.

Extended Linear Duration Invariants (ELDI), an important subset of Duration Calculus, extends well-studied Linear Duration Invariants with logical connectives and the chop modality. It is known that the model checking problem of ELDI is undecidable with both the standard continuous-time and discrete-time semantics [12, 13], but it turns out to be decidable if only bounded execution fragments of timed automata are concerned in the context of the discrete-time semantics [36]. In this paper, we prove that this problem is still decidable in the continuous-time semantics, although it is well-known that model-checking Duration Calculus with the continuous-time semantics is much more complicated than the one with the discrete-time semantics. This is achieved by reduction to the validity of Quantified Linear Real Arithmetic (QLRA). Some examples are provided to illustrate the efficiency of our approach.

For modelling hybrid systems, we have extended Event B based on its framework with the differential event. The differential event describes continuous behaviors of hybrid systems by differential equations and evolution constraint, whose proof obligations provide dynamical properties of a model. In order to ensure the safety and reliability of a model, proof obligations should be proved. It is difficult to prove proof obligation in state space, because there is no a complete method to solve differential equations in the field of mathematics. Thus we proposed an approach to proving proof obligation based on differential invariants. It is to avoid uncontrollable computation on solving differential equation. The main result is that we prove some theorems for proving proof obligations involving differential events within the framework of refinement calculus. Lastly, through the case of the Train Control System, we further show that the approach is well suited.

Fraenzle and Hansen investigated the model-checking problem of the subset of Duration Calculus without individual variables and quantifications w.r.t. some approximation semantics by reduction to the decision problem of Presburger Arithmetic, thus obtained a model-checking algorithm with 4-fold exponential complexity [6,7]. As an alternative, inspired by their work, we consider the bounded model-checking problem of the subset in the context of the standard discrete-time semantics in this paper. Based on our previous work [20], we reduce this problem to the reachability problem of timed automata. The complexity of our approach is singly exponential in the size of formulas and quadratic in the number of states of models. We implement our approach using UPPAAL and demonstrate its efficiency by some examples.

The specification of Modeling and Analysis of Real-time and Embedded Systems (MARTE) is an extension of UML in the domain of real-time and embedded Systems. However, unified modeling of continuous and discrete variables in MARTE is still an unsolved problem for hybrid real-time system development. In this paper we propose an extended statechart, Hybrid MARTE statechart, for modeling and analyzing of hybrid real-time and embedded systems. In Hybrid MARTE Statecharts, we unify the logical time and the chronometric time variables. The improvement of MARTE statechart is based on hybrid automata. Formal syntax and semantics of Hybrid MARTE statecharts are given based on labeled transition systems. At the end of this paper, a case study is given to show how to model the behavior of a Train Control System with Hybrid MARTE statecharts.

The model checker Uppaal is used to formally model and analyze parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that has been defined in RFC 3927 of the IETF. Our goal has been to construct a model that (a) is easy to understand by engineers, (b) comes as close as possible to the informal text (for each transition in the model there should be a corresponding piece of text in the RFC), and (c) may serve as a basis for formal verification. Our modeling efforts revealed several errors (or at least ambiguities) in the RFC that no one else spotted before. We present two proofs of the mutual exclusion property for Zeroconf (for an arbitrary number of hosts and IP addresses): a manual, operational proof, and a proof that combines model checking with the application of a new abstraction relation that is compositional with respect to committed locations. The model checking problem has been solved using Uppaal and the abstractions have been checked by hand.

In this paper we propose an approach to check the compatibility of two services. The models of the services are built in finite state machine (FSM) and the behavior of services is described with the process of communicating sequential processes (CSP). An operator named corresponding position concurrency is defined to facilitate the calculation of composability of the paths which are obtained from processes, thus we can determine whether the two services are compatible or not. Simple examples are introduced to illustrate how to use this approach.

In this paper, we introduce an extension of Duration Calculus called Simple Probabilistic Duration Calculus (SPDC) to express dependability requirements for real-time systems, and address the problem to decide if a probabilistic timed automaton satisfies a SPDC formula. We prove that the problem is decidable for a class of SPDC called probabilistic linear duration invariants, and provide a model checking algorithm for solving this problem.

We report on a case study in which the model checker Uppaal is used to formally model parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that has been defined in RFC 3927 of the IETF. Our goal has been to construct a model that (a) is easy to understand by engineers,(b) comes as close as possible to the informal text (for each transition in the model there should be a corresponding piece of text in the RFC), and (c) may serve as a basis for formal verification. Our conclusion is that Uppaal which combines extended finite state machines, C-like syntax and concepts from timed automata theory, is able to model Zeroconf in a faithful and intuitive manner, using notations that are familiar to protocol engineers. Our modeling efforts revealed several errors (or at least ambiguities) in the RFC that no one else spotted before. We also identify a number of points where Uppaal still can be improved. After applying a number of abstractions, Uppaal is able to fully explore the state space of an instance of our model with three hosts.