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: | WANG, Ting, SUN, Jun, WANG, Xinyu, LIU, Yang, SI, Yuanjie, DONG, Jin Song, YANG, Xiaohu, LI, Xiaohong |
---|---|
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!
|
Similar Items
-
Language inclusion checking of timed automata with non-Zenoness
by: WANG, Xinyu, et al.
Published: (2017) -
Parametric model checking timed automata under non-Zenoness assumption
by: ANDRE, Étienne, et al.
Published: (2017) -
Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties
by: Dang, Van Hung, et al.
Published: (2017) -
A systematic study on explicit-state non-zenoness checking for timed automata
by: Wang, T., et al.
Published: (2016) -
Model checking with fairness assumptions using PAT
by: Si, Y., et al.
Published: (2014)