FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

Authors: Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri Srba

Paper Information

Title:Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Authors:Frederik M. Bønneland, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marco Muñiz and Jiri Srba
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:model checking, partial order reduction, timed systems, timed-arc Petri nets, stubborn sets
Abstract:

ABSTRACT. 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 in its latest release from January 2018. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.

Pages:19
Talk:Jul 15 12:00 (Session 103A: Runtime Verification, Hybrid and Timed Systems)
Paper: