A systematic study on explicit-state non-zenoness checking for timed automata
Zeno runs, where infinitely many actions occur within finite time, may arise in Timed Automata models. Zeno runs are not feasible in reality and must be pruned during system verification. Thus it is necessary to check whether a run is Zeno or not so as to avoid presenting Zeno runs as counterexample...
Saved in:
Main Authors: | , , , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2015
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4973 https://ink.library.smu.edu.sg/context/sis_research/article/5976/viewcontent/tse2015.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-5976 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59762020-03-12T07:30:14Z A systematic study on explicit-state non-zenoness checking for timed automata WANG, Ting SUN, Jun WANG, Xinyu LIU, Yang SI, Yuanjie DONG, Jin Song YANG, Xiaohu LI, Xiaohong Zeno runs, where infinitely many actions occur within finite time, may arise in Timed Automata models. Zeno runs are not feasible in reality and must be pruned during system verification. Thus it is necessary to check whether a run is Zeno or not so as to avoid presenting Zeno runs as counterexamples during model checking. Existing approaches on non-Zenoness checking include either introducing an additional clock in the Timed Automata models or additional accepting states in the zone graphs. In addition, there are approaches proposed for alternative timed modeling languages, which could be generalized to Timed Automata. In this work, we investigate the problem of non-Zenoness checking in the context of model checking LTL properties, not only evaluating and comparing existing approaches but also proposing a new method. To have a systematic evaluation, we develop a software toolkit to support multiple non-Zenoness checking algorithms. The experimental results show the effectiveness of our newly proposed algorithm, and demonstrate the strengths and weaknesses of different approaches. 2015-01-01T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4973 info:doi/10.1109/TSE.2014.2359893 https://ink.library.smu.edu.sg/context/sis_research/article/5976/viewcontent/tse2015.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 non-Zenoness Model Checking Verification Tool 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 non-Zenoness Model Checking Verification Tool Software Engineering |
spellingShingle |
Timed Automata non-Zenoness Model Checking Verification Tool Software Engineering WANG, Ting SUN, Jun WANG, Xinyu LIU, Yang SI, Yuanjie DONG, Jin Song YANG, Xiaohu LI, Xiaohong A systematic study on explicit-state non-zenoness checking for timed automata |
description |
Zeno runs, where infinitely many actions occur within finite time, may arise in Timed Automata models. Zeno runs are not feasible in reality and must be pruned during system verification. Thus it is necessary to check whether a run is Zeno or not so as to avoid presenting Zeno runs as counterexamples during model checking. Existing approaches on non-Zenoness checking include either introducing an additional clock in the Timed Automata models or additional accepting states in the zone graphs. In addition, there are approaches proposed for alternative timed modeling languages, which could be generalized to Timed Automata. In this work, we investigate the problem of non-Zenoness checking in the context of model checking LTL properties, not only evaluating and comparing existing approaches but also proposing a new method. To have a systematic evaluation, we develop a software toolkit to support multiple non-Zenoness checking algorithms. The experimental results show the effectiveness of our newly proposed algorithm, and demonstrate the strengths and weaknesses of different approaches. |
format |
text |
author |
WANG, Ting SUN, Jun WANG, Xinyu LIU, Yang SI, Yuanjie DONG, Jin Song YANG, Xiaohu LI, Xiaohong |
author_facet |
WANG, Ting SUN, Jun WANG, Xinyu LIU, Yang SI, Yuanjie DONG, Jin Song YANG, Xiaohu LI, Xiaohong |
author_sort |
WANG, Ting |
title |
A systematic study on explicit-state non-zenoness checking for timed automata |
title_short |
A systematic study on explicit-state non-zenoness checking for timed automata |
title_full |
A systematic study on explicit-state non-zenoness checking for timed automata |
title_fullStr |
A systematic study on explicit-state non-zenoness checking for timed automata |
title_full_unstemmed |
A systematic study on explicit-state non-zenoness checking for timed automata |
title_sort |
systematic study on explicit-state non-zenoness checking for timed automata |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2015 |
url |
https://ink.library.smu.edu.sg/sis_research/4973 https://ink.library.smu.edu.sg/context/sis_research/article/5976/viewcontent/tse2015.pdf |
_version_ |
1770575163716272128 |