Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation

S Akshay, Paul Gastin, R Govind, Aniruddha R Joshi, B Srivathsan

TL;DR

The main contribution is a new simulation-based zone algorithm for checking reachability in this unified model of generalized timed automata, which is the first effective implementation not just for the unified model, but even just for automata with timers or for event-clock automata without going through a costly translation.

Abstract

In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models.

A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation

TL;DR

The main contribution is a new simulation-based zone algorithm for checking reachability in this unified model of generalized timed automata, which is the first effective implementation not just for the unified model, but even just for automata with timers or for event-clock automata without going through a costly translation.

Abstract

In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models.
Paper Structure (15 sections, 5 theorems, 6 equations, 4 figures)

This paper contains 15 sections, 5 theorems, 6 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Generalized Timed Automata
  3. Extending clocks and constraints
  4. Extending valuations
  5. Extending resets
  6. Extending guards and transitions
  7. Extending the automaton model
  8. Expressivity of GTA and examples
  9. Timed automata
  10. Event-clock automata
  11. Automata with timers
  12. The reachability problem for GTA
  13. $X_D$-Safe GTA
  14. Symbolic enumeration
  15. A concrete simulation relation for GTA

Key Result

Theorem 9

Reachability for GTA is undecidable.

Figures (4)

  • Figure 1: An automaton with clocks on left, and timers on right for same constraints.
  • Figure 2: Representation of valuations in generalized timed automata. Here, $v' = v+ \delta$.
  • Figure 3: A transition of TA (left) and of a GTA (right)
  • Figure 4: Example of a GTA

Theorems & Definitions (14)

  • Definition 1: Weights
  • Remark 2
  • Definition 3: Valuation
  • Definition 4
  • Remark 5
  • Definition 6: generalized timed automata
  • Definition 7: Semantics of GTA
  • Definition 8: Reachability problem for GTA
  • Theorem 9
  • Definition 10
  • ...and 4 more