Publication details

<< back
 

Reachability analysis for timed automata using max-plus algebra

Basic information
Original title:Reachability analysis for timed automata using max-plus algebra
Authors:Qi Lu, Michael Madsen, Martin Milata, Soren Ravn, Uli Fahrenberg, Kim G. Larsen
Further information
Citation:LU, Qi, Michael MADSEN, Martin MILATA, Søren RAVN, Uli FAHRENBERG and Kim G. LARSEN. Reachability analysis for timed automata using max-plus algebra. Journal of Logic and Algebraic Programming, Holland: Elsevier, 2012, vol. 81, No 3, p. 298-313. ISSN 1567-8326. doi:10.1016/j.jlap.2011.10.004.Export BibTeX
@article{974570,
author = {Lu, Qi and Madsen, Michael and Milata, Martin and Ravn, Søren and Fahrenberg, Uli and Larsen, Kim G.},
article_location = {Holland},
article_number = {3},
doi = {http://dx.doi.org/10.1016/j.jlap.2011.10.004},
keywords = {Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron},
language = {eng},
issn = {1567-8326},
journal = {Journal of Logic and Algebraic Programming},
title = {Reachability analysis for timed automata using max-plus algebra},
url = {http://www.sciencedirect.com/science/article/pii/S156783261100097X},
volume = {81},
year = {2012}
}
Original language:English
Field:Informatics
WWW:link to a new windowhttp://www.sciencedirect.com/science/article/pii/S156783261100097X
Type:Article in Periodical
Keywords:Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron

We show that max-plus polyhedra are usable as a data structure in reachability analysis of timed automata. Drawing inspiration from the extensive work that has been done on difference bound matrices, as well as previous work on max-plus polyhedra in other areas, we develop the algorithms needed to perform forward and backward reachability analysis using max-plus polyhedra. To show that the approach works in practice and theory alike, we have created a proof-of-concept implementation on top of the model checker opaal.

Related projects:

 
 
top