Reachability analysis for timed automata using max-plus algebra

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

LU Qi MADSEN Michael MILATA Martin RAVN Soren FAHRENBERG Uli LARSEN Kim G.

Year of publication 2012
Type Article in Periodical
Magazine / Source Journal of Logic and Algebraic Programming
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.sciencedirect.com/science/article/pii/S156783261100097X
Doi http://dx.doi.org/10.1016/j.jlap.2011.10.004
Field Informatics
Keywords Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron
Attached files
Description 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:

You are running an old browser version. We recommend updating your browser to its latest version.