Reachability analysis for timed automata using max-plus algebra

被引：12

作者：

Lu, Qi ^{[1
]}

Madsen, Michael ^{[1
]}

Milata, Martin ^{[1
]}

Ravn, Soren ^{[1
]}

Fahrenberg, Uli ^{[1
]}

Larsen, Kim G. ^{[1
]}

机构：

[1] Aalborg Univ, Dept Comp Sci, DK-9220 Aalborg, Denmark

来源：

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING | 2012年 / 81卷 / 03期

关键词：

Timed automaton; Real-time model checking; Data structure; Max-plus algebra; Max-plus polyhedron; MODEL CHECKING; THEOREM;

D O I：

10.1016/j.jlap.2011.10.004

中图分类号：

学科分类号：

摘要：

We show that max-plus polyhedra are usable as a data structure in teachability 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. (C) 2011 Elsevier Inc. All rights reserved.

引用

页码：298 / 313

页数：16

共 50 条

[1] Reachability and invariance problems in max-plus algebra
Gaubert, S
Katz, R
[J]. POSITIVE SYSTEMS, PROCEEDINGS, 2003, 294 : 15 - 22
[2] Behaviour Equivalent Max-Plus Automata for a Class of Timed Petri Nets
Triska, Lukas
Moor, Thomas
[J]. IFAC PAPERSONLINE, 2020, 53 (04): : 75 - 82
[3] Max-plus: A network algebra
Daniel-Cavalcante, Mabia
Magalhaes, Mauricio F.
Santos-Mendes, Rafael
[J]. POSITIVE SYSTEMS, PROCEEDINGS, 2006, 341 : 375 - 382
[4] A walk on max-plus algebra
Watanabe, Sennosuke
Fukuda, Akiko
Segawa, Etsuo
Sato, Iwao
[J]. LINEAR ALGEBRA AND ITS APPLICATIONS, 2020, 598 : 29 - 48
[5] Max-plus algebra and max-plus linear discrete event systems: An introduction
De Schutter, Bart
van den Boom, Ton
[J]. WODES' 08: PROCEEDINGS OF THE 9TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, 2008, : 36 - 42
[6] On the Existence of Simulations for Max-Plus Automata
Daviaud, Berangere
Lahaye, Sebastien
Lhommeau, Mehdi
Komenda, Jan
[J]. IEEE CONTROL SYSTEMS LETTERS, 2024, 8 : 694 - 699
[7] Reachability for Interval Max-Plus Linear Systems
Wang, Cailu
Tao, Yuegang
Yang, Peng
[J]. PROCEEDINGS OF THE 36TH CHINESE CONTROL CONFERENCE (CCC 2017), 2017, : 2392 - 2396
[8] Simulations and bisimulations for max-plus automata
Ciric, Miroslav
Micic, Ivana
Matejic, Jelena
Stamenkovic, Aleksandar
[J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2024, 34 (02): : 269 - 295
[9] Polynomial convolutions in max-plus algebra
Rosenmann, Amnon
Lehner, Franz
Peperko, Aljosa
[J]. LINEAR ALGEBRA AND ITS APPLICATIONS, 2019, 578 : 370 - 401
[10] A contribution to the determinization of max-plus automata
Sébastien Lahaye
Aiwen Lai
Jan Komenda
Jean-Louis Boimond
[J]. Discrete Event Dynamic Systems, 2020, 30 : 155 - 174

← 1 2 3 4 5 →