Language inclusion checking of timed automata with non-Zenoness
Given a timed automaton P modeling an implementation and a timed automaton S as a specification, the problem of language inclusion checking is to decide whether the language of P is a subset of that of S. It is known to be undecidable. The problem gets more complicated if non-Zenoness is taken into...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2017
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4701 https://ink.library.smu.edu.sg/context/sis_research/article/5704/viewcontent/Non_Zenoness_av.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-5704 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-57042020-04-01T05:31:16Z Language inclusion checking of timed automata with non-Zenoness WANG, Xinyu SUN, Jun WANG, Ting QIN, Shengchao Given a timed automaton P modeling an implementation and a timed automaton S as a specification, the problem of language inclusion checking is to decide whether the language of P is a subset of that of S. It is known to be undecidable. The problem gets more complicated if non-Zenoness is taken into consideration. A run is Zeno if it permits infinitely many actions within finite time. Otherwise it is non-Zeno. Zeno runs might present in both P and S. It is necessary to check whether a run is Zeno or not so as to avoid presenting Zeno runs as counterexamples of language inclusion checking. In this work, we propose a zone-based semi-algorithm for language inclusion checking with non-Zenoness. It is further improved with simulation reduction based on LU-simulation. Though our approach is not guaranteed to terminate, we show that it does in many cases through empirical study. Our approach has been incorporated into the PAT model checker, and applied to multiple systems to show its usefulness. 2017-11-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4701 info:doi/10.1109/TSE.2017.2653778 https://ink.library.smu.edu.sg/context/sis_research/article/5704/viewcontent/Non_Zenoness_av.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 Timed automata language inclusion non-Zenoness Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Timed automata language inclusion non-Zenoness Software Engineering |
spellingShingle |
Timed automata language inclusion non-Zenoness Software Engineering WANG, Xinyu SUN, Jun WANG, Ting QIN, Shengchao Language inclusion checking of timed automata with non-Zenoness |
description |
Given a timed automaton P modeling an implementation and a timed automaton S as a specification, the problem of language inclusion checking is to decide whether the language of P is a subset of that of S. It is known to be undecidable. The problem gets more complicated if non-Zenoness is taken into consideration. A run is Zeno if it permits infinitely many actions within finite time. Otherwise it is non-Zeno. Zeno runs might present in both P and S. It is necessary to check whether a run is Zeno or not so as to avoid presenting Zeno runs as counterexamples of language inclusion checking. In this work, we propose a zone-based semi-algorithm for language inclusion checking with non-Zenoness. It is further improved with simulation reduction based on LU-simulation. Though our approach is not guaranteed to terminate, we show that it does in many cases through empirical study. Our approach has been incorporated into the PAT model checker, and applied to multiple systems to show its usefulness. |
format |
text |
author |
WANG, Xinyu SUN, Jun WANG, Ting QIN, Shengchao |
author_facet |
WANG, Xinyu SUN, Jun WANG, Ting QIN, Shengchao |
author_sort |
WANG, Xinyu |
title |
Language inclusion checking of timed automata with non-Zenoness |
title_short |
Language inclusion checking of timed automata with non-Zenoness |
title_full |
Language inclusion checking of timed automata with non-Zenoness |
title_fullStr |
Language inclusion checking of timed automata with non-Zenoness |
title_full_unstemmed |
Language inclusion checking of timed automata with non-Zenoness |
title_sort |
language inclusion checking of timed automata with non-zenoness |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2017 |
url |
https://ink.library.smu.edu.sg/sis_research/4701 https://ink.library.smu.edu.sg/context/sis_research/article/5704/viewcontent/Non_Zenoness_av.pdf |
_version_ |
1770574983870808064 |