Urgent Partial Order Reduction for Extended Timed Automata

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
EditorsDang Van Hung, Oleg Sokolsky
Number of pages17
Publication date2020
ISBN (Print)9783030591519
ISBN (Electronic)978-3-030-59152-6
Publication statusPublished - 2020
Event18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 - Hanoi, Viet Nam
Duration: 19 Oct 202023 Oct 2020


Conference18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
Country/TerritoryViet Nam
SeriesLecture Notes in Computer Science

Bibliographical note

Publisher Copyright:
© 2020, Springer Nature Switzerland AG.

Copyright 2020 Elsevier B.V., All rights reserved.


Dive into the research topics of 'Urgent Partial Order Reduction for Extended Timed Automata'. Together they form a unique fingerprint.

Cite this