Formal Modeling and Analysis of Timed Systems

Reasoning about uncertainty is one of the fundamental challenges in the real-world deployment of many cyber-physical system applications. Several models for capturing environment uncertainty have been suggested in the past, and these typically are parametric models with either Markovian assumptions on the time-evolution of the system, or Gaussian assumptions on uncertainty. In this paper, we propose a framework for creating data-driven abstractions of the environment based on Stochastic Temporal Logics. Such logics allow combining the power of temporal logic-based absractions with powerful stochastic modeling techniques. Our framework allows constructing stochastic models using generalized master equations, which can be viewed as a nonparametric model capturing the dynamic evolution of the probabilities of system variables with time. Furthermore, we show how we can automatically infer temporal logic based abstractions from such a model. We give examples of applications for such a framework, and highlight some of the open problems and challenges in this approach.

This paper analyzes the use of models for timed systems, particularly cyber-physical systems, which mix timed behavior of physical subsystems with largely untimed behavior of software. It examines how models are used in engineering and science, showing that two complementary styles for using models lead to differing conclusions about how to approach the problem of modeling timed systems. The paper argues for an increased use of an engineering style of modeling, where models are more like specifications of desired behavior and less like descriptions of some preexisting system. Finally, it argues that in the engineering style of modeling, determinism is an extremely valuable property.

We study timed systems in which some timing features are unknown parameters. First we consider Upper-bound Parametric Timed Automata (U-PTAs), one of the simplest extensions of timed automata with parameters, in which parameters are only used as clock upper bounds. Up to now, there have been several decidability results for the existence of parameter values in U-PTAs such that flat TCTL formulas are satisfied. We prove here that this does not extend to the full logic and that only one level of nesting leads to undecidability. This provides, to the best of our knowledge, the first problem decidable for Timed Automata with an undecidable parametric emptiness version for U-PTAs. Second we study Lower/Upper-bound Parametric Timed Automata (L/U-PTAs) in which parameters are used either as clock lower bound, or as clock upper bound, but not both. We prove that without invariants, flat TCTL is decidable for L/U-PTAs by resolving the last non investigated liveness properties.

We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify real-time constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the one-variable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discrete-time case. Our prototype implementation appears to outperform previous discrete-time implementations of TPTL monitoring.

We introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed automata, in the sense that the finite-state processes are replaced by timed automata, and messages inside the perfect channels are equipped with clocks representing their ages. In addition to the standard operations (resetting clocks, checking guards of clocks) each automaton can either (1) append a message to the tail of a channel with an initial age or (2) receive the message at the head of a channel if its age satisfies a set of given constraints. In this paper, we show that the reachability problem is undecidable even in the case of two timed automata connected by one unidirectional timed channel if one allows global clocks (that the two automata can check and manipulate). We prove that this undecidability still holds even for CTA consisting of three timed automata and two unidirectional timed channels (and without any global clock). However, the reachability problem becomes decidable (in \(\mathsf {EXPTIME}\)) in the case of two automata linked with one unidirectional timed channel and with no global clock. Finally, we consider the bounded-context case, where in each context, only one timed automaton is allowed to receive messages from one channel while being able to send messages to all the other timed channels. In this case we show that the reachability problem is decidable.

A transition of a (time) Petri net is persistent if once it is enabled, it can never become disabled through occurrences of other transitions until it is fired [5, 15]. It is said to be effect-persistent if it is persistent and its effect (The effect of an enabled transition t in a marking M is defined by the set of transitions newly enabled by firing t.) is not affected by firing other transitions. This paper investigates some sufficient conditions for persistency and effect-persistency of transitions, in the context of time Petri nets (TPNs for short) that depend on the marking and the static/dynamic time information of the model. Then, it shows how to use these sufficient conditions to improve the partial order reduction technique of the TPN model.

In this work, we extend the notion of branching bisimulation to weighted systems. We abstract away from singular transitions and allow for bisimilar systems to match each other using finite paths of similar behaviour and weight. We show that this weighted branching bisimulation is characterised by a weighted temporal logic. Due to the restrictive nature of quantitative behavioural equivalences, we develop a notion of relative distance between weighted processes by relaxing our bisimulation by some factor. Intuitively, we allow for transitions \(s \xrightarrow {w} s'\) to be matched by finite paths that accumulate a weight within the interval \([\frac{w}{\varepsilon }, w\varepsilon ]\), where \(\varepsilon \) is the factor of relaxation. We extend this relaxation to our logic and show that for a class of formulae, our relaxed logic characterises our relaxed bisimulation. From this notion of relaxed bisimulation, we derive a relative pseudometric and prove robustness results. Lastly, we prove certain topological properties for classes of formulae on the open-ball topology induced by our pseudometric.

Markov automata (MAs) have been introduced in [16] as a continuous-time version of Segala’s probabilistic automata (PAs) [29]. This paper defines several variants of trace equivalence for closed MA models. These trace equivalences are obtained as a result of button pushing experiments with a black box model of MA. For every class of MA scheduler, a corresponding variant of trace equivalence has been defined. We investigate the relationship among these trace equivalences and also compare them with bisimulation for MAs. Finally, we prove that the properties specified using deterministic timed automaton (DTA) specifications and metric temporal logic (MTL) formulas are preserved under some of these trace equivalences.

Markov automata (MAs) [16] extend probabilistic automata (PAs) [29] with stochastic aspects [22]. This paper defines two equivalence relations, namely, weighted Markovian equivalence (WME) and weak weighted Markovian equivalence (WWME) for the subclass of closed MAs. We define the quotient system under these relations and investigate their relationship with strong bisimulation and weak bisimulation, respectively. Next, we show that both WME and WWME can be used for repeated minimization of closed MAs. Finally, we prove that properties specified using deterministic timed automaton (DTA) specifications and metric temporal logic (MTL) formulas are preserved under WME and WWME quotienting.

We introduce and study a new (pseudo) metric on timed words having several advantages:

We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal w that match a given temporal pattern \(\varphi \). As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by \(\varphi \) and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads w, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated.

We propose an automatic synthesis technique to generate provably correct controllers of stochastic linear dynamical systems for Signal Temporal Logic (STL) specifications. While formal synthesis problems can be directly formulated as exists-forall constraints, the quantifier alternation restricts the scalability of such an approach. We use the duality between a system and its proof of correctness to partially alleviate this challenge. We decompose the controller synthesis into two subproblems, each addressing orthogonal concerns - stabilization with respect to the noise, and meeting the STL specification. The overall controller is a nested controller comprising of the feedback controller for noise cancellation and an open loop controller for STL satisfaction. The correct-by-construction compositional synthesis of this nested controller relies on using the guarantees of the feedback controller instead of the controller itself. We use a linear feedback controller as the stabilizing controller for linear systems with bounded additive noise and over-approximate its ellipsoid stability guarantee with a polytope. We then use this over-approximation to formulate a mixed-integer linear programming (MILP) problem to synthesize an open-loop controller that satisfies STL specifications.

We present a method based on the Hamilton-Jacobi framework that is able to compute over- and under-approximations of reachable sets for autonomous dynamical systems beyond polynomial dynamics. The method does not resort to user-supplied candidate polynomials, but rather relies on an expansion of the evolution function whose convergence in compact state space is guaranteed. Over- and under-approximations of the reachable state space up to any designated precision can consequently be obtained based on truncations of that expansion. As the truncations used in computing over- and under-approximations as well as their associated error bounds agree, double-sided enclosures of the true reach-set can be computed in a single sweep. We demonstrate the precision of the enclosures thus obtained by comparison of benchmark results to related simulations.

This paper describes the development of finite abstractions of Max-Plus-Linear (MPL) systems using tropical operations. The idea of tropical abstraction is inspired by the fact that an MPL system is a discrete-event model updating its state with operations in the tropical algebra. The abstract model is a finite-state transition system: we show that the abstract states can be generated by operations on the tropical algebra, and that the generation of transitions can be established by tropical multiplications of matrices. The complexity of the algorithms based on tropical algebra is discussed and their performance is tested on a numerical benchmark against an existing alternative abstraction approach.