Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the 16th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2018, held in Beijing, China, in September 2018.

The 14 papers presented in this volume were carefully reviewed and selected from 29 submissions. The papers are organized in the following topical sections: invited papers, temporal logics, distributed timed systems, behavioral equivalences, timed words, and continuous dynamical systems. The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share interests in modeling and analysis of timed systems and, as a generalization, hybrid systems.

Inhaltsverzeichnis

Frontmatter

Invited Papers

Frontmatter

Stochastic Temporal Logic Abstractions: Challenges and Opportunities

Abstract
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.
Jyotirmoy V. Deshmukh, Panagiotis Kyriakis, Paul Bogdan

Models of Timed Systems

Abstract
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.
Edward A. Lee

Temporal Logics

Frontmatter

TCTL Model Checking Lower/Upper-Bound Parametric Timed Automata Without Invariants

Abstract
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.
Étienne André, Didier Lime, Mathias Ramparison

Monitoring Temporal Logic with Clock Variables

Abstract
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.
Adrián Elgyütt, Thomas Ferrère, Thomas A. Henzinger

Reactive Synthesis for Robotic Swarms

Abstract
We consider the problem of reactive synthesis for systems with non-instantaneous actions, i.e., it may take an arbitrary amount of time for the actions of the system to complete, and meanwhile the input from the environment may also change, possibly requiring a different response from the system. The problem can be modeled as a typical reactive synthesis problem by introducing auxiliary propositions and fairness assumptions, at the expense of additional computational complexity. We develop new realizability and synthesis algorithms that address the problem without adding auxiliary propositions or assumptions. We discuss the complexity of both approaches. We then apply our algorithms to synthesize controllers for a swarm robotic system. We implement both approaches and compare them using a specific swarm task.
Salar Moarref, Hadas Kress-Gazit

Distributed Timed Systems

Frontmatter

Perfect Timed Communication Is Hard

Abstract
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.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna

On Persistency in Time Petri Nets

Abstract
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.
Kamel Barkaoui, Hanifa Boucheneb

A Relational Model for Probabilistic Connectors Based on Timed Data Distribution Streams

Abstract
Connectors have shown their great potential for coordination of concurrent activities encapsulated as components and services in large-scale distributed applications. In this paper, we develop a formal model for a probabilistic extension of the channel-based coordination language Reo. The model formalizes connectors with probabilistic behavior as relations on Timed Data Distribution Streams (TDDSs), which specifies properties of primitive channels and complex connectors with probabilistic behavior properly. Furthermore, the implementation of this probabilistic model has been developed in Coq, which serves to demonstrate how the model can be used to prove probabilistic connectors’ properties.
Meng Sun, Xiyue Zhang

Behavioral Equivalences

Frontmatter

Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations

Abstract
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.
Mathias Claus Jensen, Kim Guldstrand Larsen, Radu Mardare

Trace Relations and Logical Preservation for Markov Automata

Abstract
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.
Arpit Sharma

Non-bisimulation Based Behavioral Relations for Markov Automata

Abstract
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.
Arpit Sharma

Timed Words

Frontmatter

Distance on Timed Words and Applications

Abstract
We introduce and study a new (pseudo) metric on timed words having several advantages:
  • it is global: it applies to words having different number of events;
  • it is realistic and takes into account imprecise observation of timed events; thus it reflects the fact that the order of events cannot be observed whenever they are very close to each other;
  • it is suitable for quantitative verification of timed systems: we formulate and solve quantitative model-checking and quantitative monitoring in terms of the new distance, with reasonable complexity;
  • it is suitable for information-theoretical analysis of timed systems: due to its pre-compactness the quantity of information in bits per time unit can be correctly defined and computed.
Eugene Asarin, Nicolas Basset, Aldric Degorre

Online Timed Pattern Matching Using Automata

Abstract
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.
Alexey Bakhirkin, Thomas Ferrère, Dejan Nickovic, Oded Maler, Eugene Asarin

Continuous Dynamical Systems

Frontmatter

Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems

Abstract
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.
Susmit Jha, Sunny Raj, Sumit Kumar Jha, Natarajan Shankar

Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems

Abstract
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.
Meilun Li, Peter N. Mosaad, Martin Fränzle, Zhikun She, Bai Xue

Tropical Abstractions of Max-Plus Linear Systems

Abstract
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.
Muhammad Syifa’ul Mufid, Dieky Adzkiya, Alessandro Abate

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise