Affordable Access

Reachability analysis for timed automata using max-plus algebra

Elsevier BV North-Holland
Publication Date
  • Computer Science


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.

There are no comments yet on this publication. Be the first to share your thoughts.