Tomlin, Claire J.; Mitchell, Ian M.; Bayen, Alexandre M.; Oishi, Meeko K. M. Computational techniques for the verification and control of hybrid systems. (English) Zbl 1074.93014 Capasso, Vincenzo (ed.) et al., Multidisciplinary methods for analysis optimization and control of complex systems. Lectures of the summer school Jacques Louis Lions, Montecatini, Italy, March 17–22, 2003. Berlin: Springer (ISBN 3-540-22310-X/hbk). Mathematics in Industry 7. The European Consortium for Mathematics in Industry, 151-175 (2004). The purpose of this paper is to deal with some verification techniques for hybrid systems, a software toolkit for efficient application of these techniques, and the use of these tools in the analysis and control of large scale systems. Starting with a summary of the available methods (a detailed set of references is also given), it is observed that all rely on the ability to compute reachable sets of hybrid systems and they differ mainly in the assumptions made about the representation of sets, and evolution of the continuous state dynamics. The proposed algorithm uses an implicit surface function representation of the reachable set, and a differential game theoretic method for its evolution. Then it is illustrated how this reachable set computation may be embedded as the key component in safety verification of hybrid systems. The algorithm represents a set implicitly as the zero sublevel set of a given function, and computes its evolution through the hybrid dynamics using a combination of constrained level set methods and discrete mappings through transition functions. The algorithm is currently constrained by computational complexity, but an improved variant is taken into consideration. Two examples in the verification of protocols for aircraft collision avoidance, and of mode switching logic in autopilots finally illustrate the obtained results.For the entire collection see [Zbl 1056.00010]. Reviewer: Mihail Voicu (Iaşi) Cited in 3 Documents MSC: 93B40 Computational methods in systems theory (MSC2010) 93B03 Attainable sets, reachability 90B25 Reliability, availability, maintenance, inspection in operations research 93B12 Variable structure systems 93A15 Large-scale systems 93C65 Discrete event control/observation systems 93-04 Software, source code, etc. for problems pertaining to systems and control theory Keywords:hybrid systems; verification techniques; reachable set computation; differential game method; software toolkit; large scale systems; implicit surface function representation; safety; constrained level set methods; aircraft collision avoidance; autopilots Software:SPIN; Kronos; PVS; Uppaal; HyTech PDFBibTeX XMLCite \textit{C. J. Tomlin} et al., Math. Ind. 7, 151--175 (2004; Zbl 1074.93014)