Skip to Main content Skip to Navigation
Journal articles

Reachability analysis for timed automata using max-plus algebra

Abstract : 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.
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Uli Fahrenberg Connect in order to contact the contributor
Submitted on : Thursday, November 27, 2014 - 10:59:25 AM
Last modification on : Thursday, January 20, 2022 - 5:33:09 PM
Long-term archiving on: : Monday, March 2, 2015 - 9:20:43 AM


Files produced by the author(s)



Qi Lu, Michael Madsen, Martin Milata, Søren Ravn, Uli Fahrenberg, et al.. Reachability analysis for timed automata using max-plus algebra. Journal of Logic and Algebraic Programming, Elsevier, 2012, 81, pp.298 - 313. ⟨10.1016/j.jlap.2011.10.004⟩. ⟨hal-01087998⟩



Record views


Files downloads