Signal Temporal Logic (STL) is a powerful formal language for specifying real-time specifications of Cyber-Physical Systems (CPS). Transforming specifications written in natural language into STL formulas automatically has attracted increasing attention. Existing rule-based methods depend heavily on rigid pattern matching and domain-specific knowledge, limiting their generalizability and scalability. Recently, Supervised Fine-Tuning (SFT) of large language models (LLMs) has been successfully applied to transform natural language into STL. However, the lack of fine-grained supervision on atomic proposition correctness, semantic fidelity, and formula readability often leads SFT-based methods to produce formulas misaligned with the intended meaning. To address these issues, we propose RESTL, a reinforcement learning (RL)-based framework for the transformation from natural language to STL. RESTL introduces multiple independently trained reward models that provide fine-grained, multi-faceted feedback from four perspectives, i.e., atomic proposition consistency, semantic alignment, formula succinctness, and symbol matching. These reward models are trained with a curriculum learning strategy to improve their feedback accuracy, and their outputs are aggregated into a unified signal that guides the optimization of the STL generator via Proximal Policy Optimization (PPO). Experimental results demonstrate that RESTL significantly outperforms state-of-the-art methods in both automatic metrics and human evaluations.

Stochastic dynamical systems have emerged as fundamental models across numerous application domains, providing powerful mathematical representations for capturing uncertain system behavior. In this paper, we address the problem of runtime safety and reach-avoid probability prediction for discrete-time stochastic systems with online observations, i.e., estimating the probability that the system satisfies a given safety or reach-avoid specification. Unlike traditional approaches that rely solely on offline models, we propose a framework that incorporates real-time observations to dynamically refine probability estimates for safety and reach-avoid events. By introducing observation-aware barrier functions, our method adaptively updates probability bounds as new observations are collected, combining efficient offline computation with online backward iteration. This approach enables rigorous and responsive prediction of safety and reach-avoid probabilities under uncertainty. In addition to the theoretical guarantees, experimental results on benchmark systems demonstrate the practical effectiveness of the proposed method.

Abstract Moment estimation for stochastic differential equations (SDEs) is fundamental to the formal reasoning and verification of stochastic dynamical systems, yet remains challenging and is rarely available in closed form. In this paper, we study time-homogeneous SDEs with polynomial drift and diffusion, and investigate when their moments can be computed exactly. We formalize the notion of moment-solvable SDEs and propose a generic symbolic procedure that, for a given monomial, attempts to construct a finite-dimensional linear ordinary differential equation (ODE) system governing its moment, thereby enabling exact computation. We introduce a syntactic class of pro-solvable SDEs, characterized by a block-triangular structure, and prove that all polynomial moments of any pro-solvable SDE admit such finite ODE representations. This class strictly generalizes linear SDEs and includes many nonlinear models. Experimental results demonstrate the effectiveness of our approach.

Abstract Modern cyber-physical systems are complex, and requirements are often written in Signal Temporal Logic (STL). Writing the right STL is difficult in practice; engineers benefit from concrete executions that illustrate what a specification actually admits. Trace synthesis addresses this need, but a single witness rarely suffices to understand intent or explore edge cases—diverse satisfying behaviors are far more informative. We introduce diversified trace synthesis: the automatic generation of sets of behaviorally diverse traces that satisfy a given STL formula. Building on a MILP encoding of STL and system model, we formalize three complementary diversification objectives—Boolean distance, random Boolean distance, and value distance—all captured by an objective function and solved iteratively. We implement these ideas in STLts-Div, a lightweight Python tool that integrates with Gurobi.

In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth , a parameter that measures the graph’s tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.

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.

Abstract Techniques of light-weight formal methods, such as monitoring and falsification, are attracting attention for quality assurance of cyber-physical systems. The techniques require formal specs, however, and writing right specs is still a practical challenge. Commonly one relies ontrace synthesis—i.e. automatic generation of a signal that satisfies a given spec—to examine the meaning of a spec. In this work, motivated by 1) complex STL specs from an automotive safety standard and 2) the struggle of existing tools in their trace synthesis, we introduce a novel trace synthesis algorithm for STL specs. It combines the use of MILP (inspired by works on controller synthesis) and avariable-interval encodingof STL semantics (previously studied for SMT-based STL model checking). The algorithm solves model checking, too, as the dual of trace synthesis. Our experiments show that only ours has realistic performance needed for the interactive examination of STL specs by trace synthesis.

Abstract Opacity serves as a critical security and confidentiality property, which concerns whether an intruder can unveil a system’s secret based on structural knowledge and observed behaviors. Opacity in timed systems presents greater complexity compared to untimed systems, and it has been established that opacity for timed automata is undecidable. However, the original proof cannot be applied to decide the opacity of one-clock timed automata directly. In this paper, we explore three types of opacity within timed automata: language-based timed opacity, initial-location timed opacity, and current-location timed opacity. We begin by formalizing these concepts and establishing transformation relations among them. Subsequently, we demonstrate the undecidability of the opacity problem for one-clock timed automata. Furthermore, we offer a constructive proof for the conjecture regarding the decidability of opacity for timed automata in discrete-time semantics. Additionally, we present a sufficient condition and a necessary condition for the decidability of opacity in specific subclasses of timed automata.

Abstract In this paper, we present a tool for monitoring the traces of cyber-physical systems (CPS) at runtime, with respect to Signal Temporal Logic (STL) specifications. Our tool is based on the recent advances of causation monitoring, which reports not only whether an executing trace violates the specification, but also how relevant the increment of the trace at each instant is to the specification violation. In this way, it can deliver more information about system evolution than classic online robust monitors. Moreover, by adapting two dynamic programming strategies, our implementation significantly improves the efficiency of causation monitoring, allowing its deployment in practice. The tool is implemented as a executable and can be easily adapted to monitor CPS in different formalisms. We evaluate the efficiency of the proposed monitoring tool, and demonstrate its superiority over existing robust monitors in terms of the information it can deliver about system evolution.

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 Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL) . The classic STL monitoring is performed by computing a robustness interval that specifies, at each instant, how far the monitored signals are from violating and satisfying the specification. However, since a robustness interval monotonically shrinks during monitoring, classic online monitors may fail in reporting new violations or in precisely describing the system evolution at the current instant. In this paper, we tackle these issues by considering the causation of violation or satisfaction, instead of directly using the robustness. We first introduce a Boolean causation monitor that decides whether each instant is relevant to the violation or satisfaction of the specification. We then extend this monitor to a quantitative causation monitor that tells how far an instant is from being relevant to the violation or satisfaction. We further show that classic monitors can be derived from our proposed ones. Experimental results show that the two proposed monitors are able to provide more detailed information about system evolution, without requiring a significantly higher monitoring cost.

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.

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.

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.

Opacity is an important property on information flow to guarantee that a system under attack keeps its “secrets”, possibly subsets of traces (language-based opacity) or subsets of states (state-based opacity), opaque to the outside intruder with partial observability. In this paper, we investigate the opacity problems of real-time automata (RTA), which is a popular model for real-time systems. In order to prove that the language-opacity problem of RTA is decidable, we introduce the notion of trace-equivalence and then translate RTA into finite-state automata (FA) with timed alphabets. Besides, we also introduce the notions of partitioned timed alphabet and language to guarantee trace equivalence is preserved by complementation and product operations over FA with timed alphabets. Thus, our decision procedure can be sketched as follows: first, translate the RTA to model a system under attack and the RTA to specify the secret behavior of the system into FA, respectively; then, compute another FA, which accepts all traces accepted by the first FA, but not by the second one; afterwards, project these FA onto the given observable set; finally, unify the alphabets of these FA such that for any two timed actions with the same event, their time parts do not have any overlap. Thus, whether the original system is language-opaque with respect to the secret RTA and the observable set is reduced to the inclusion problem of regular languages. Similarly, we can show decidability of initial-opacity of RTA.