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

https://hal.inria.fr/hal-01087998
Contributor : Uli Fahrenberg <>
Submitted on : Thursday, November 27, 2014 - 10:59:25 AM
Last modification on : Tuesday, June 15, 2021 - 4:27:45 PM
Long-term archiving on: : Monday, March 2, 2015 - 9:20:43 AM

File

jlp.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

417

Files downloads

321