© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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}, }