The rise of machine learning and cloud technologies has led to a remarkable influx of data within modern cyber-physical systems. However, extracting meaningful information from this data has become a significant challenge due to its volume and complexity. Timed pattern matching has emerged as a powerful specification-based runtime verification and temporal data analysis technique to address this challenge. In this paper, we provide a comprehensive tutorial on timed pattern matching that ranges from the underlying algebra and pattern specification languages to performance analyses and practical case studies. Analogous to textual pattern matching, timed pattern matching is the task of finding all time periods within temporal behaviors of cyber-physical systems that match a predefined pattern. Originally we introduced and solved several variants of the problem using the name of match sets, which has evolved into the concept of timed relations over the past decade. Here we first formalize and present the algebra of timed relations as a standalone mathematical tool to solve the pattern matching problem of timed pattern specifications. In particular, we show how to use the algebra of timed relations to solve the pattern matching problem for timed regular expressions and metric compass logic in a unified manner. We experimentally demonstrate that our timed pattern matching approach performs and scales well in practice. We further provide in-depth insights into the similarities and fundamental differences between monitoring and matching problems as well as regular expressions and temporal logic formulas. Finally, we illustrate the practical application of timed pattern matching through two case studies, which show how to extract structured information from temporal datasets obtained via simulations or real-world observations. These results and examples show that timed pattern matching is a rigorous and efficient technique in developing and analyzing cyber-physical systems.

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers. L’archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d’enseignement et de recherche français ou étrangers, des laboratoires publics ou privés. Kronos: a model-checking tool for real-time systems Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine

We present Mixed-time Signal Temporal Logic (STL-mx), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL-mx, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example.

The understanding of biological systems and processes requires the development of dynamical models characterized by nonlinear laws and often intricate regulation architectures. Differential and difference equations are common formalisms to characterize such systems. Hybrid dynamical systems come in handy when the modeled system combines continuous and discrete evolutions or different evolution modes such as where slow evolution phases are interrupted by fast ones. Biological data with kinetic content are often scarce, thus it can be appropriate to reason in terms of sets of (parametrized) models and sets of trajectories. In doing so, uncertainties and lack of knowledge are explicitly taken into account and more reliable predictions can be made. A crucial problem in Systems Biology is thus to identify regions of parameter space for which model behavior is consistent with experimental observations. In this chapter, we investigate the use of set-based analysis techniques, designed to compute on sets of behaviors, for the validation of biological models under uncertainties and perturbations. In addition, these techniques can be used for the synthesis of model parameter sets, so that the execution of the considered biological model under the influence of the synthesized parameters is guaranteed to satisfy a given constraint or property. The proposed approach is illustrated by several case studies, namely a model of iron homeostasis in mammalian cells and some epidemic models.

We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.

This report documents the program and the outcomes of Dagstuhl Seminar 19071 Specification Formalisms for Modern Cyber-Physical Systems. Specifications play a major role in evaluating behaviors of modern cyber-physical systems (CPS). There is currently no specification language that allows joint description of safety, performance, security, privacy, and reliability aspects of CPS applications. The Dagstuhl seminar brought together researchers and practitioners from formal methods, control theory, machine learning and robotics to discuss the state-of-the-art and open challenges in specifying properties of modern CPS. Special attention was given to exploring the intersection of machine learning and formal specification languages, where formal specifications can serve as a bridge between the world of verification and the world of learning and data-mining.

We introduce in this paper AMT 2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance.

The term Cyber-Physical Systems (CPS) typically refers to engineered, physical and biological systems monitored and/or controlled by an embedded computational core. The behaviour of a CPS over time is generally characterised by the evolution of physical quantities, and discrete software and hardware states. In general, these can be mathematically modelled by the evolution of continuous state variables for the physical components interleaved with discrete events. Despite large effort and progress in the exhaustive verification of such hybrid systems, the complexity of CPS models limits formal verification of safety of their behaviour only to small instances. An alternative approach, closer to the practice of simulation and testing, is to monitor and to predict CPS behaviours at simulation-time or at runtime. In this chapter, we summarise the state-of-the-art techniques for qualitative and quantitative monitoring of CPS behaviours. We present an overview of some of the important applications and, finally, we describe the tools supporting CPS monitoring and compare their main features.

This report documents the program and the outcomes of Dagstuhl Seminar 18082 "Formal Methods for the Synthesis of Biomolecular Circuits". Synthetic biology aims for the rational bottom-up engineering of new biological functionalities. Recent years have witnessed an increase in the degree of "rationality" in the design of synthetic biomolecular circuits. With it, fewer design-build-test cycles were necessary to achieve a desired circuit performance. Most of these success stories reported the realization of logic circuits, typically operating via regulation of gene expression and/or direct manipulation of DNA sequences with recombinases, executing combinatorial and sometimes sequential logic. This was often achieved with the help of two ingredients, a library of previously well-characterized parts and some computational modeling. Hence, although circuits in synthetic biology are still by far less understood and characterized than electronic circuits, the opportunity for the formal synthesis of circuit designs with respect to a behavioral specification starts to emerge in synthetic biology.

Timed pattern matching consists in finding all segments of a dense-time Boolean signal that match a pattern defined by a timed regular expression. This problem has been formulated and solved in [17] via an offline algorithm that takes the signal and expression as inputs and produces the set of all matches, represented as a finite union of two-dimensional zones. In this work we develop an online version of this approach where the input signal is presented incrementally and the matching is computed incrementally as well. Naturally, the concept of derivatives of regular expressions due to Brzozowski [6] can play a role in defining what remains to match after having read a prefix of the signal. However the adaptation of this concept is not a straightforward for two reasons: the dense infinite-state nature of timed behaviors and the fact that we are interested in matching, not only in prefix acceptance. To resolve these issues we develop an alternative theory of signals and expressions based on absolute time and show how derivatives are defined and computed in this setting. We then implement an online timed pattern matching algorithm based on these results.

Monitoring system behaviors using formal specifications appears to be an effective technique in analyzing cyber-physical systems. However, to achieve intended results in monitoring, specification languages need to be intuitive, elegant, and expressive at the first place. In this paper, we propose a metric extension of well-known Halpern-Shoham (hs) logic, called Metric Compass Logic (mcl), for monitoring purposes. Originally proposed for high-level temporal reasoning, the logic hs is very expressive and enables users to specify many temporal patterns in an intuitive and elegant way. As our main contribution, we present an offline monitoring technique for timed patterns specified in mcl. Our solution is built upon the framework developed for timed regular expressions (TRE) matching but explores a different (logical) direction. We finally study several practical features concerning atomic formulas and discuss a combined timed pattern speciication language with TRE.

We present a generic algorithmic scheme for learning languages defined over large or infinite alphabets such as bounded subsets of N and R, or Boolean vectors of high dimension. These languages are accepted by deterministic symbolic automata that use predicates to label transitions, forming a finite partition of the alphabet for every state. Our learning algorithm, an adaptation of Angluin's L*, combines standard automaton learning by state characterization, with the learning of the static predicates that define the alphabet partitions. We do not assume a helpful teacher who provides minimal counter-examples when the conjectured automaton is incorrect. Instead we use random sampling to obtain PAC (probably approximately correct) learnability. We have implemented the algorithm for numerical and Boolean alphabets and the preliminary performance results show that languages over large or infinite alphabets can be learned under more realistic assumptions.

We define a new notion of satisfaction of a temporal logic formula \(\varphi \) by a behavior w. This notion, denoted by \((w,t,t')\,\models \, \varphi \), is characterized by two time parameters: the position t from which satisfaction is considered, and the end of the (finite) behavior \(t'\) which indicates how much do we know about the behavior. We define this notion in dense time where \(\varphi \) is a formula in the future fragment of metric temporal logic (MTL) and w is a Boolean signal of bounded variability. We show that the set of all pairs \((t,t')\) such that \((w,t,t')\,\models \, \varphi \) can be expressed as a finite union of two-dimensional zones and give an effective procedure to compute it.

Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems.

The term Cyber-Physical Systems (CPS) typically refers to to engineering, physical and biological systems monitored and/or controlled by an embedded computational core. The behavior of a CPS over time is generally characterized by the evolution of physical quantities and discrete software and hardware states. In general, these can be mathematically modeled by the evolution of continuous state variables for the physical components interleaved with discrete events. Despite large effort and progress in the exhaustive verification of such hybrid systems, the complexity of CPS models limits formal verification of their safe behavior only to small instances. An alternative approach, closer to the practice of simulation and testing, is to monitor and to predict CPS behaviors at simulation-time or at runtime. In this chapter we attempt to summarize the state-of-the-art techniques for qualitative and quantitative monitoring of CPS behaviors. We present an overview of some of the important applications and, finally, we describe the tools supporting CPS monitoring and compare their main features.

Some reflections on verification and runtime verification in general and of cyber-physical systems in particular.

This book constitutes the thoroughly refereed post-workshop proceedings of the Second International Workshop on Hybrid Systems Biology, HSB 2013, held as part of the ECAL 2013 event, in Taormina, Ital

We propose a declarative measurement specification language for quantitative performance evaluation of hybrid (discrete-continuous) systems based on simulation traces. We use timed regular expressions with events to specify patterns that define segments of simulation traces over which measurements are to be taken. In addition, we associate measure specifications over these patterns to describe a particular type of performance evaluation (maximization, average, etc.) to be done over the matched signal segments. The resulting language enables expressive and versatile specification of measurement objectives. We develop an algorithm for our measurement framework, implement it in a prototype tool, and apply it in a case study of an automotive communication protocol. Our experiments demonstrate that the proposed technique is usable with very low overhead to a typical (computationally intensive) simulation.

We develop a generic tool for approximating the Pareto front of multicriteria optimization problems using stochastic local search algorithms. Our algorithmic scheme handles problems that the multi-criteria context introduces into the local search framework such as the non-uniqueness of the best neighbor and the potentially large size of the Pareto front. We demonstrate the performance of our algorithm under different configurations and parameters on multi-criteria variants of the quadratic assignment and 0-1 knapsack problems. The adaptation of our scheme to new problems involves a minimal investment.