Publication details
Reachability analysis for timed automata using max-plus algebra
| Authors | |
|---|---|
| Year of publication | 2012 |
| Type | Article in Periodical |
| Magazine / Source | Journal of Logic and Algebraic Programming |
| MU Faculty or unit | |
| 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: |