Publication Type
Journal Article
Version
publishedVersion
Publication Date
1-2015
Abstract
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.
Keywords
Timed Automata, non-Zenoness, Model Checking, Verification Tool
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
IEEE Transactions on Software Engineering
Volume
41
Issue
1
First Page
3
Last Page
18
ISSN
0098-5589
Identifier
10.1109/TSE.2014.2359893
Publisher
Institute of Electrical and Electronics Engineers (IEEE)
Citation
WANG, Ting; SUN, Jun; WANG, Xinyu; LIU, Yang; SI, Yuanjie; DONG, Jin Song; YANG, Xiaohu; and LI, Xiaohong.
A systematic study on explicit-state non-zenoness checking for timed automata. (2015). IEEE Transactions on Software Engineering. 41, (1), 3-18.
Available at: https://ink.library.smu.edu.sg/sis_research/4973
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.1109/TSE.2014.2359893