Urgent Partial Order Reduction for Extended Timed Automata

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
TitelAutomated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
RedaktørerDang Van Hung, Oleg Sokolsky
Antal sider17
ForlagSpringer
Publikationsdato2020
Sider179-195
ISBN (Trykt)9783030591519
ISBN (Elektronisk)978-3-030-59152-6
DOI
StatusUdgivet - 2020
Begivenhed18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 - Hanoi, Vietnam
Varighed: 19 okt. 202023 okt. 2020

Konference

Konference18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
LandVietnam
ByHanoi
Periode19/10/202023/10/2020
NavnLecture Notes in Computer Science
Vol/bind12302
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Urgent Partial Order Reduction for Extended Timed Automata'. Sammen danner de et unikt fingeraftryk.

Citationsformater