Abstract Cyber-physical systems are complex environments that combine physical devices (i.e., sensors and actuators) with a software controller. The ubiquity of these systems and dangers associated with their failure require the implementation of mechanisms to monitor, verify and guarantee their correct behaviour. This paper presents ParetoLib 2.0, a Python tool for offline monitoring and specification mining of cyber-physical systems. ParetoLib 2.0 uses signal temporal logic (STL) as the formalism for specifying properties on time series. ParetoLib 2.0 builds upon other tools for evaluating and mining STL expressions, and extends them with new functionalities. ParetoLib 2.0 implements a set of new quantitative operators for trace analysis in STL, a novel mining algorithm and an original graphical user interface. Additionally, the performance is optimised with respect to previous releases of the tool via data-type annotations and multi core support. ParetoLib 2.0 allows the offline verification of STL properties as well as the specification mining of parametric STL templates. Thanks to the implementation of the new quantitative operators for STL, the tool outperforms the expressiveness and capabilities of similar runtime monitors.

Sampling timed words out of a timed language described as a timed automaton may seem a simple task: start from the initial state, choose a transition and a delay and repeat until an accepting state is reached. Unfortunately, simple approach based on local, on-the-fly rules produces timed words from distributions that are biased in some unpredictable ways. For this reason, approaches have been developed to guarantee that the sampling follows a more desirable distribution defined over the timed language and not over the automaton. One such distribution is the maximal entropy distribution, whose implementation requires several non-trivial computational steps. In this paper, we present Wordgen which combines those different necessary steps into a lightweight standalone tool. The resulting timed words can be mapped to signals used for model-based testing and falsification of cyber-physical systems thanks to a simple interface with the Breach tool.

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.

In this paper we present ShapEx, a tool that generates random behaviors from shape expressions, a formal specification language for describing sophisticated temporal behaviors of CPS. The tool samples a random behavior in two steps: (1) it first explores the space of qualitative parameterized shapes and then (2) instantiates parameters by sampling a possibly non-linear constraint. We implement several sampling strategies in the tool that we present in the paper and demonstrate its applicability on two use scenarios.

An appealing feature of Signal Temporal Logic (STL) is the existence of efficient monitoring algorithms both for Boolean and real-valued robustness semantics, which are based on computing an aggregate function (conjunction, disjunction, min, or max) over a sliding window. On the other hand, there are properties that can be monitored with the same algorithms, but that cannot be directly expressed in STL due to syntactic restrictions. In this paper, we define a new specification language that extends STL with the ability to produce and manipulate real-valued output signals and with a new form of until operator. The new language still admits efficient offline monitoring, but also allows to express some properties that in the past motivated researchers to extend STL with existential quantification, freeze quantification, and other features that increase the complexity of monitoring.

Admissible strategies, i.e. those that are not dominated by any other strategy, are a typical rationality notion in game theory. In many classes of games this is justified by results showing that any strategy is admissible or dominated by an admissible strategy. However, in games played on finite graphs with quantitative objectives (as used for reactive synthesis), this is not the case. We consider increasing chains of strategies instead to recover a satisfactory rationality notion based on dominance in such games. We start with some order-theoretic considerations establishing sufficient criteria for this to work. We then turn our attention to generalised safety/reachability games as a particular application. We propose the notion of maximal uniform chain as the desired dominance-based rationality concept in these games. Decidability of some fundamental questions about uniform chains is established.

We call network of automata a family of partially synchronised automata, i.e. a family of deterministic automata which are synchronised via shared letters, and evolve independently otherwise. We address the problem of uniform random sampling of words recognised by a network of automata. To that purpose, we define the reduced automaton of the model, which involves only the product of the synchronised part of the component automata. We provide uniform sampling algorithms which are polynomial with respect to the size of the reduced automaton, greatly improving on the best known algorithms. Our sampling algorithms rely on combinatorial and probabilistic methods and are of three different types: exact, Boltzmann and Parry sampling.