School of Computing

Efficient Detection of Zeno Runs in Timed Automata

Rodolfo Gomez and Howard Bowman

In J.-F. Raskin and P.S. Thiagarajan, editors, 5th International Conference FORMATS 2007 (Formal Modelling and Analysis of Timed Systems), volume 4763 of LNCS, pages 182-196, Salzburg, Austria, October 2007. Springer.

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.

Download publication 192 kbytes

Bibtex Record

@inproceedings{2626,
author = {Rodolfo Gomez and Howard Bowman},
title = {Efficient {D}etection of {Z}eno {R}uns in {T}imed {A}utomata},
month = {October},
year = {2007},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2007/2626},
    publication_type = {inproceedings},
    submission_id = {1357_1191924984},
    booktitle = {5th International Conference FORMATS 2007 (Formal Modelling and Analysis of Timed Systems)},
    editor = {J.-F. Raskin and P.S. Thiagarajan},
    volume = {4763},
    series = {LNCS},
    address = {Salzburg, Austria},
    publisher = {Springer},
    ISSN = {0302-9743},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014