Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions

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 prese...

Full description

Saved in:
Bibliographic Details
Main Authors: HANSEN, Henri, LIN, Shang-Wei, LIU, Yang, NGUYEN, Truong Khanh, SUN, Jun
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2014
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4956
https://ink.library.smu.edu.sg/context/sis_research/article/5959/viewcontent/diamonds.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-5959
record_format dspace
spelling sg-smu-ink.sis_research-59592020-02-27T03:10:16Z Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions HANSEN, Henri LIN, Shang-Wei LIU, Yang NGUYEN, Truong Khanh SUN, Jun 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. 2014-07-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4956 info:doi/10.1007/978-3-319-08867-9_26 https://ink.library.smu.edu.sg/context/sis_research/article/5959/viewcontent/diamonds.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Programming Languages and Compilers Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Programming Languages and Compilers
Software Engineering
spellingShingle Programming Languages and Compilers
Software Engineering
HANSEN, Henri
LIN, Shang-Wei
LIU, Yang
NGUYEN, Truong Khanh
SUN, Jun
Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions
description 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.
format text
author HANSEN, Henri
LIN, Shang-Wei
LIU, Yang
NGUYEN, Truong Khanh
SUN, Jun
author_facet HANSEN, Henri
LIN, Shang-Wei
LIU, Yang
NGUYEN, Truong Khanh
SUN, Jun
author_sort HANSEN, Henri
title Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions
title_short Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions
title_full Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions
title_fullStr Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions
title_full_unstemmed Diamonds are a girl's best friend: Partial order reduction for timed automata with abstractions
title_sort diamonds are a girl's best friend: partial order reduction for timed automata with abstractions
publisher Institutional Knowledge at Singapore Management University
publishDate 2014
url https://ink.library.smu.edu.sg/sis_research/4956
https://ink.library.smu.edu.sg/context/sis_research/article/5959/viewcontent/diamonds.pdf
_version_ 1770575157953298432