TY - GEN
T1 - Urgent Partial Order Reduction for Extended Timed Automata
AU - Larsen, Kim Guldstrand
AU - Mikučionis, Marius
AU - Rodriguez, Marco Antonio Muniz
AU - Srba, Jiri
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2020
Y1 - 2020
N2 - We propose a partial order reduction method for reachability analysis of networks of timed automata interacting via synchronous channel communication and via shared variables. Our method is based on (classical) symbolic delay transition systems and exploits the urgent behavior of a system, where time does not introduce dependencies among actions. In the presence of urgent behavior in the network, we apply partial order reduction techniques for discrete systems based on stubborn sets. We first describe the framework in the general setting of symbolic delay time transition systems and then instantiate it to the case of timed automata. We implement our approach in the model checker Uppaal and observe a substantial reduction in the reachable state space for case studies that exhibit frequent urgent behaviour and only a moderate slowdown on models with limited occurrence of urgency.
AB - We propose a partial order reduction method for reachability analysis of networks of timed automata interacting via synchronous channel communication and via shared variables. Our method is based on (classical) symbolic delay transition systems and exploits the urgent behavior of a system, where time does not introduce dependencies among actions. In the presence of urgent behavior in the network, we apply partial order reduction techniques for discrete systems based on stubborn sets. We first describe the framework in the general setting of symbolic delay time transition systems and then instantiate it to the case of timed automata. We implement our approach in the model checker Uppaal and observe a substantial reduction in the reachable state space for case studies that exhibit frequent urgent behaviour and only a moderate slowdown on models with limited occurrence of urgency.
UR - http://www.scopus.com/inward/record.url?scp=85093853604&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-59152-6_10
DO - 10.1007/978-3-030-59152-6_10
M3 - Article in proceeding
AN - SCOPUS:85093853604
SN - 9783030591519
T3 - Lecture Notes in Computer Science
SP - 179
EP - 195
BT - Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
A2 - Hung, Dang Van
A2 - Sokolsky, Oleg
PB - Springer
T2 - 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
Y2 - 19 October 2020 through 23 October 2020
ER -