School of Computing

Compositional detection of Zeno behavior in Timed Automata with Deadlines

Rodolfo Gomez

Technical report 3-09, Computing Laboratory, University of Kent, June 2009.

Abstract

We present a compositional analysis to detect Zeno behavior in Timed Automata with Deadlines. A syntactic analysis is defined, based on Tripakis' strong non-Zenoness property, which identifies all elementary cycles where Zeno behavior may occur. This analysis is complemented by TCTL reachability properties, which characterize the occurrence Zeno behavior in potentially unsafe cycles.

Download publication 216 kbytes (PDF)

Bibtex Record

@techreport{2932,
author = {Rodolfo Gomez},
title = {Compositional detection of {Z}eno behavior in {T}imed {A}utomata with {D}eadlines},
month = {June},
year = {2009},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2009/2932},
    publication_type = {techreport},
    submission_id = {12707_1245947740},
    institution = {Computing Laboratory, University of Kent},
    type = {Technical report},
    number = {3-09},
}

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

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

Last Updated: 21/03/2014