Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1109/TSE.2014.2359893 | IEEE Trans. Software Eng. |
Keywords | Field | DocType |
automata theory,non-zenoness,timed automata,model checking ltl properties,model checking,software toolkit,systematic evaluation,timed automata models,timed modeling languages,verification tool,clocks,system verification,zone graphs,graph theory,explicit-state nonzenoness checking,zeno runs,real-time systems,formal verification,automata,systematics,cost accounting | Zeno's paradoxes,Abstraction model checking,Model checking,Computer science,Automaton,Modeling language,Theoretical computer science,Timed automaton,Software,Counterexample | Journal |
Volume | Issue | ISSN |
41 | 1 | 0098-5589 |
Citations | PageRank | References |
0 | 0.34 | 28 |
Authors | ||
8 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ting Wang | 1 | 11 | 1.34 |
| Jun Sun | 2 | 1407 | 120.35 |
| xinyu | 3 | 590 | 30.19 |
| Yang Liu | 4 | 2194 | 188.81 |
| yuanjie | 5 | 36 | 3.57 |
| Jin Song Dong | 6 | 1369 | 107.12 |
| Xiaohu Yang | 7 | 125 | 8.71 |
| Xiaohong Li | 8 | 173 | 44.41 |