Reachability analysis for timed automata using max-plus algebra

Warning

This publication doesn't include Institute of Computer Science. 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	maxplus-paper.pdf
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:	Czech Republic membership in the European Research Consortium for Informatics and Mathematics Rozsáhlé výpočetní systémy: modely, aplikace a verifikace