Skip to main content

Efficient Detection of Zeno Runs in Timed Automata

Gomez, Rodolfo and Bowman, Howard (2007) Efficient Detection of Zeno Runs in Timed Automata. In: Raskin, J.-F. and Thiagarajan, P.S., eds. Formal Modeling and Analysis of Timed Systems 5th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 195-210. ISBN 978-3-540-75453-4. E-ISBN 978-3-540-75454-1. (doi:10.1007/978-3-540-75454-1_15)

Abstract

Zeno runs, where infinitely many actions occur in finite time, may inadvertently arise in timed automata specifications. Zeno runs may compromise the reliability of formal verification, and few model-checkers provide the means to deal with them: this usually takes the form of liveness checks, which are computationally expensive. As an alternative, we describe here an efficient static analysis to assert absence of Zeno runs on Uppaal networks; this is based on Tripakis's strong non-Zenoness property, and identifies all loops in the automata graphs where Zeno runs may possibly occur. If such unsafe loops are found, we show how to derive an abstract network that over-approximates the loop behaviour. Then, liveness checks may assert absence of Zeno runs in the original network, by exploring the reduced state space of the abstract network. Experiments show that this combined approach may be much more efficient than running liveness checks on the original network.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-540-75454-1_15
Uncontrolled keywords: Zeno Runs, Timed Automata, Model-checking, Uppaal
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Computational Intelligence Group
Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:04 UTC
Last Modified: 29 May 2019 13:35 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/14538 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year