ABSTRACT. Recent work demonstrated that using Koopman surrogate models for the falsification of black-box models against signal temporal logic specifications is highly effective. However, the bottleneck of this approach arises from the mixed-integer linear program optimization used to synthesize the falsifying trajectory. The complexity of mixed-integer linear programming can be prohibitive, exhibiting exponential increases with the number of binary variables. In this work, we introduce a new weighted robustness encoding which removes the need for binary variables altogether. Moreover, we also propose a new weighting scheme for Koopman operator linearization, which aims to compensate for inaccuracies in the learned model. We evaluate our approach on a set of benchmarks from the ARCH falsification competition. Our weighting methods significantly improve computational efficiency and reduce the number of simulations needed to find falsifying traces.

ABSTRACT. Inspired by the local search framework for SMT over the theory of Non-linear Real Arithmetic (NRA) in \cite{li2023local}, we propose in this paper a local search algorithm for SMT over an extended theory of NRA, denoted as NTA-, which admits the sine function. To establish a key operation, called {\em cell-jump}, for updating variable assignments in local search, we design an algorithm for isolating real roots of mixed trigonometric-polynomials with {\em real} coefficients. The new local search algorithm is implemented as a tool, called LS(NTA-). Experiments are carried out to evaluate LS(NTA-) on four classes of benchmarks. The results show that LS(NTA-) performs better than state-of-the-art SMT solvers on these benchmarks. It possesses the capability to handle simple transcendental equation constraints, and is good at solving NTA- formulas with inequality constraints of high degrees.

ABSTRACT. Hybrid CTL (HCTL) extends the branching-time temporal logic CTL with hybrid operators that refer to states, thus mixing first-order and modal logic features. The extended expressiveness of HCTL allows for the specification of properties that play a crucial role in analysing various dynamical systems describing complex physical or biological processes. Often, not all interactions in such processes are precisely known. An appropriate semantic structure is a collection of Kripke structures called a coloured Kripke structure. The paper proposes an entirely symbolic BDD-based algorithm for model-checking HCTL on coloured Kripke structures. We discuss the correctness and complexity of the algorithm and consider some optimisations of the algorithm reflecting the structure of hybrid formulas. Finally, we evaluate the algorithm on several real-world cases.

ABSTRACT. Time-Sensitive Networking (TSN) has become a favorable option for real-time communication in Cyber-Physical Systems (CPSs), such as intelligent vehicles and industrial control systems, due to its capability of providing bounded end-to-end latencies. However, designing CPSs on a TSN network can be an NP-hard combinatorial optimization problem. Therefore, a formal and efficient approach is desired to explore the design space with different combinations of data flow periods. Accordingly, we propose a novel design flow that preemptively generates a set of schedulable period lists, guaranteeing that all data flow deadlines can be met. We further employ Deep Reinforcement Learning (DRL) to optimize the collecting process of these period lists. The experimental result demonstrates remarkable success where 97.02% solutions are found with 4.85X speed higher than the method based on Satisfiability Modulo Theories. The result of large-scale scenarios also reveals that our approach outperforms any other comparative method by at least 3.93X more schedulable period lists collected.

ABSTRACT. LeoParDS is a new tool for learning broadcast protocols (BPs) from a set of positive and negative example traces. It is the first tool that enables learning of a distributed computational model in a parameterized setting, i.e., with a parametric number of processes running the BP concurrently. We describe the tool along a running example, discuss some implementation details, and present experimental results on randomly generated BPs.

ABSTRACT. In this paper, we revisit the active learning of timed languages recognizable by event-recording automata. Our framework employs a method known as greybox learning, which enables the learning of event-recording automata with a minimal number of control states. This approach avoids learning the region automaton associated with the language, contrasting with existing methods. We have implemented our greybox learning algorithm with various heuristics to maintain low computational complexity. The efficacy of our approach is demonstrated through several examples.

ABSTRACT. The observable behavior of a system usually carries useful information about its internal state, properties, and potential future behaviors. In this paper, we introduce configuration monitoring to determine an unknown configuration of a running system based on observations of its behavior. We develop a modular and generic pipeline to synthesize automata-theoretic configuration monitors from a featured transition system model of the configurable system to be monitored. The pipeline further allows synthesis under partial observability and network-induced losses as well as predictive configuration monitors taking the potential future behavior of a system into account. Beyond the novel application of configuration monitoring, we show that our approach also generalizes and unifies existing work on runtime monitoring and fault diagnosis, which aim at detecting the satisfaction or violation of properties and the occurrence of faults, respectively. We empirically demonstrate the efficacy of our approach with a case study on configuration monitors synthesized from configurable systems community benchmarks.

ABSTRACT. Reactive synthesis is the process of generating correct con- trollers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLT specifications (i.e., LTL with propositions replaced by literals from a theory T ), into equi-realizable LTL specifications. In this paper we extend these results into a full synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory T and outputs valuations of system variables from T . We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLT specification. We also show that our method allows adaptive responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full synthesis method for LTLT and, moreover, is more predictable and faster than previous approaches.

ABSTRACT. Markov decision processes (MDPs) provide a fundamental model for sequential decision making under process uncertainty. A classical synthesis task is to compute for a given MDP a winning policy that achieves a desired specification. However, at design time, one typically needs to consider a family of MDPs modelling various system variations. For a given family, we study synthesising (1) the subset of MDPs where a winning policy exists and (2) a preferably small number of winning policies that together cover this subset. We introduce policy trees that concisely capture the synthesis result. The key ingredient for synthesising policy trees is a recursive application of a game-based abstraction. We combine this abstraction with an efficient refinement procedure and a post-processing step. An extensive empirical evaluation demonstrates superior scalability of our approach compared to naive baselines. For one of the benchmarks, we find 246 winning policies covering 94 million MDPs. Our algorithm requires less than 30 minutes, whereas the naive baseline only covers 3.7% of MDPs in 24 hours.