TY - JOUR
T1 - Reachability analysis for timed automata using max-plus algebra
AU - Lu, Qi
AU - Madsen, Michael
AU - Milata, Martin
AU - Ravn, Søren
AU - Fahrenberg, Uli
AU - Larsen, Kim Guldstrand
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84858075069&partnerID=8YFLogxK
U2 - 10.1016/j.jlap.2011.10.004
DO - 10.1016/j.jlap.2011.10.004
M3 - Journal article
SN - 2352-2208
VL - 81
SP - 298
EP - 313
JO - Journal of Logic and Algebraic Programming
JF - Journal of Logic and Algebraic Programming
IS - 3
ER -