Paper Info
Title
From non-zenoness verification to termination
Abstract
We investigate the problem of verifying the absence of zeno executions in a hybrid system. A zeno execution is one in which there are infinitely many discrete transitions in a finite time interval. The presence of zeno executions poses challenges towards implementation and analysis of hybrid control systems. We present a simple transformation of the hybrid system which reduces the non-zenoness verification problem to the termination verification problem, that is, the original system has no zeno executions if and only if the transformed system has no non-terminating executions. This provides both theoretical insights and practical techniques for non-zenoness verification. Further, it also provides techniques for isolating parts of the hybrid system and its initial states which do not exhibit zeno executions. We illustrate the feasibility of our approach by applying it on hybrid system examples.
Year
DOI
Venue
2015
10.1109/MEMCOD.2015.7340490
MEMOCODE
Keywords
Field
DocType
Hybrid System, Non-Zenoness, Verification
Zeno's paradoxes,Functional verification,Computer science,Automaton,Real-time computing,Theoretical computer science,Software,If and only if,Control system,Hybrid system,Trajectory
Conference
Citations 
PageRank 
References 
0
0.34
22
Authors
4
Name
Order
Citations
PageRank
Pierre Ganty124220.29
Samir Genaim289144.31
Ratan Lal341.78
Pavithra Prabhakar421925.69