\input zb-basic
\input zb-ioport
\iteman{io-port 05715554}
\itemau{Cheng, Peng; Kumar, Vijay}
\itemti{Sampling-based falsification and verification of controllers for continuous dynamic systems.}
\itemso{Akella, Srinivas (ed.) et al., Algorithmic foundation of robotics VII. Selected contributions of the seventh international workshop on the algorithmic foundations of robotics (WAFR 2006), New York, NJ, USA, July 16--18, 2006. Berlin: Springer (ISBN 978-3-540-68404-6/hbk; 978-3-540-68405-3/ebook). Springer Tracts in Advanced Robotics 47, 391-406 (2008).}
\itemab
Summary: We present a sampling-based verification algorithm for continuous dynamic systems with uncertainty due to adversaries, unmodeled disturbance inputs, unknown parameters, or initial conditions. The algorithm attempts to find inputs (and resulting trajectories) that falsify the specifications of the system thus providing examples of bad inputs to the system. The system is said to be verified if the algorithm cannot find falsifying inputs.  The main contribution of the paper is the analysis of the effects of discretization of the state and input spaces that are inherent to sampling-based techniques. We derive conditions that guarantee resolution completeness. These provide sufficient, although conservative, conditions for verifying Lipschitz continuous (but possibly non smooth) dynamic systems without known analytical solutions. We analyze the effects of transformations of the input and state space on these conditions. The main results of this paper are illustrated with several simple examples.
\itemrv{~}
\itemcc{}
\itemut{controllers; continuous dynamic systems; sampling-based verification algorithm; discretization of the state and input spaces}
\itemli{doi:10.1007/978-3-540-68405-3\_25}
\end