Reachability analysis for timed automata using max-plus algebra

详细信息	查看全文 | 推荐本文 |

• 作者：Qi Lu ^{qlu09@student.aau.dk} ; Michael Madsen ^{msma09@student.aau.dk} ; Martin Milata¹ ; ^{xmilata@fi.muni.cz} ; Sø ; ren Ravn ^{sravn06@student.aau.dk} ; Uli Fahrenberg ; ^{ulrich.fahrenberg@irisa.fr} ; Kim G. Larsen ^{kgl@cs.aau.dk}
• 关键词：Timed automaton ; Real-time model checking ; Data structure ; Max-plus algebra ; Max-plus polyhedron
• 刊名：Journal of Logic and Algebraic Programming
• 出版年：2012
• 期刊代码：73_15678326
• 类别：cp
• 出版时间：April, 2012
• 卷：81
• 期：3
• 页码：298-313
• 文件大小：532 K

摘要

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.