Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00106625" target="_blank" >RIV/00216224:14330/18:00106625 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_28" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_28</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-96145-3_28" target="_blank" >10.1007/978-3-319-96145-3_28</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

Popis výsledku v původním jazyce

Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.

Název v anglickém jazyce

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

Popis výsledku anglicky

Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2018

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18)

ISBN

9783319961446

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

20

Strana od-do

527-546

Název nakladatele

Springer

Místo vydání

Netherlands

Místo konání akce

UK

Datum konání akce

1. 1. 2018

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000491481600028