Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2014
Abstract
A major obstacle for using partial order reduction in the context of real time verification is that the presence of clocks and clock constraints breaks the usual diamond structure of otherwise independent transitions. This is especially true when information of the relative values of clocks is preserved in the form of diagonal constraints. However, when diagonal constraints are relaxed by a suitable abstraction, some diamond structure is re-introduced in the zone graph. In this article, we introduce a variant of the stubborn set method for reducing an abstracted zone graph. Our method works with all abstractions, but especially targets situations where one abstract execution can simulate several permutations of the corresponding concrete execution, even though it might not be able to simulate the permutations of the abstract execution. We define independence relations that capture this “hidden” diamond structure, and define stubborn sets using these relations. We provide a reference implementation for verifying timed language inclusion, to demonstrate the effectiveness of our method.
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 26th International Conference, CAV 2014, Vienna, Austria, July 18–22
First Page
391
Last Page
406
ISBN
9783319088662
Identifier
10.1007/978-3-319-08867-9_26
Publisher
Springer Link
City or Country
Vienna, Austria
Citation
HANSEN, Henri; LIN, Shang-Wei; LIU, Yang; NGUYEN, Truong Khanh; and SUN, Jun.
Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions. (2014). Proceedings of the 26th International Conference, CAV 2014, Vienna, Austria, July 18–22. 391-406.
Available at: https://ink.library.smu.edu.sg/sis_research/4956
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-319-08867-9_26