Abstract Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure $\delta $ δ for STL, based on a new distance that we define over timed signals. In contrast with existing measures, $\delta $ δ provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL property. Thus, $\delta $ δ is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing $\delta $ δ is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. This paper is an extension of (Rino et al. in Joint International Conference on Quantitative Evaluation of SysTems & International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), 2024), published at QEST+FORMATS 2024. The extension includes implementation of algorithms to compute $\delta $ δ in a prototype tool, and an evaluation of our approach on a case study of quality assessment of insulin controllers for diabetic patients.

In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise.

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.

Timed formalisms such as Timed Automata (TA), Signal Temporal Logic (STL) and Timed Regular expressions (TRE) have been previously applied as behaviour specifications for monitoring or runtime verification, in particular, under the form of pattern-matching, i.e. computing the set of all the segments of a given system run that satisfy the specification.

Quantitative properties of timed regular languages, such as information content (growth rate, entropy) are explored. The approach suggested by the same authors is extended to languages of timed automata with punctual (equalities) and non-punctual (non-equalities) transition guards. Two size measures for such languages are identified: mean dimension and volumetric entropy. The former is the linear growth rate of the dimension of the language; it is characterized as the spectral radius of a max-plus matrix associated to the automaton. The latter is the exponential growth rate of the volume of the language; it is characterized as the logarithm of the spectral radius of a matrix integral operator on some Banach space associated to the automaton. Relation of the two size measures to classical information-theoretic concepts is explored.

We propose a subclass of timed game automata(TGA), called Task TGA, representing networks of communicating tasks where the system can choose when to start the task and the environment can choose the duration of the task. We search to solve finite-horizon reachability games on Task TGA by building strategies in the form of Simple Temporal Networks with Uncertainty (STNU). Such strategies have the advantage of being very succinct due to the partial order reduction of independent tasks.We show that the existence of such strategies is an NP-complete problem. A practical consequence of this result is a fully forward algorithm for building STNU strategies.Potential applications of this work are planning and scheduling under temporal uncertainty.

In this article, we definetimed regular expressions, a formalism for specifying discrete behaviors augmented with timing information, and prove that its expressive power is equivalent to thetimed automataof Alur and Dill. This result is the timed analogue of Kleene Theorem and, similarly to that result, the hard part in the proof is the translation from automata to expressions. This result is extended from finite to infinite (in the sense of Büchi) behaviors. In addition to these fundamental results, we give a clean algebraic framework for two commonly accepted formalisms for timed behaviors, time-event sequences and piecewise-constant signals.

Investigates the computational power of several models of dynamical systems under infinitesimal perturbations of their dynamics. We consider models for both discrete- and continuous-time dynamical systems: Turing machines, piecewise affine maps, linear hybrid automata and piecewise-constant derivative systems (a simple model of hybrid systems). We associate with each of these models a notion of perturbed dynamics by a small /spl epsi/ (w.r.t. to a suitable metric), and define the perturbed reachability relation as the intersection of all reachability relations obtained by /spl epsi/-perturbations, for all possible values of /spl epsi/. We show that, for the four kinds of models we consider, the perturbed reachability relation is co-recursively enumerable (co-r.e.), and that any co-r.e. relation can be defined as the perturbed reachability relation of such models. A corollary of this result is that systems that are robust (i.e. whose reachability relation is stable under infinitesimal perturbation) are decidable.

In this paper, we suggest a novel methodology for synthesizing switching controllers for continuous and hybrid systems whose dynamics are defined by linear differential equations. We formulate the synthesis problem as finding the conditions upon which a controller should switch the behavior of the system from one "mode" to another in order to avoid a set of bad states and propose an abstract algorithm that solves the problem by an iterative computation of reachable states. We have implemented a concrete version of the algorithm, which uses a new approximation scheme for reachability analysis of linear systems.

In this paper we define timed regular expressions, and extension of regular expressions for specifying sets of dense-time discrete-valued signals. We show that this formalism is equivalent in expressive power to the timed automata of Alur and Dill by providing a translation procedure from expressions to automata and vice versa. the result is extended to /spl omega/-regular expressions (Buchi's theorem).