×

Safe & robust reachability analysis of hybrid systems. (English) Zbl 1400.68140

Summary: Hybrid systems – more precisely, their mathematical models – can exhibit behaviors, like Zeno behaviors, that are absent in purely discrete or purely continuous systems. First, we observe that, in this context, the usual definition of reachability – namely, the reflexive and transitive closure of a transition relation – can be unsafe, i.e., it may compute a proper subset of the set of states reachable in finite time from a set of initial states. Therefore, we propose safe reachability, which always computes a superset of the set of reachable states.
Second, in safety analysis of hybrid and continuous systems, it is important to ensure that a reachability analysis is also robust w.r.t. small perturbations to the set of initial states and to the system itself, since discrepancies between a system and its mathematical models are unavoidable. We show that, under certain conditions, the best Scott continuous approximation of an analysis \(A\) is also its best robust approximation. Finally, we exemplify the gap between the set of reachable states and the supersets computed by safe reachability and its best robust approximation.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
06B35 Continuous lattices and posets, applications
18B20 Categories of machines, automata
93B25 Algebraic methods

Software:

dReach
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abramsky, S.; Jung, A., Domain theory, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 3, (1994), Clarendon Press Oxford), 1-168
[2] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T. A.; Ho, P.-H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theoret. Comput. Sci., 138, 1, 3-34, (1995) · Zbl 0874.68206
[3] Asperti, A.; Longo, G., Categories, types and structures: an introduction to category theory for the working computer scientist, (1991), MIT Press · Zbl 0783.18001
[4] Awodey, S., Category theory, (2010), Oxford University Press · Zbl 1194.18001
[5] Clarke, E.; Fehnker, A.; Han, Z.; Krogh, B.; Stursberg, O.; Theobald, M., Verification of hybrid systems based on counterexample-guided abstraction refinement, (TACAS, (2003), Springer), 192-207 · Zbl 1031.68078
[6] Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (Computer Aided Verification, (2000), Springer), 154-169 · Zbl 0974.68517
[7] Conway, J. B., A course in functional analysis, (1990), Springer · Zbl 0706.46003
[8] Cousot, P.; Cousot, R., Abstract interpretation frameworks, J. Logic Comput., 2, 4, 511-547, (1992) · Zbl 0783.68073
[9] Cuijpers, P. J.L., On bicontinuous bisimulation and the preservation of stability, (Bemporad, A.; Bicchi, A.; Buttazzo, G., Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 4416, (2007), Springer), 676-679 · Zbl 1221.93208
[10] Cuijpers, P. J.L.; Reniers, M. A., Topological (bi-) simulation, Electron. Notes Theor. Comput. Sci., 100, 49-64, (2004) · Zbl 1271.68177
[11] Damm, W.; Pinto, G.; Ratschan, S., Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems, Internat. J. Found. Comput. Sci., 18, 01, 63-86, (2007) · Zbl 1109.68064
[12] Edalat, A., Dynamical systems, measures and fractals via domain theory, Inform. and Comput., 120, 1, 32-48, (July 1995)
[13] Fränzle, M., Analysis of hybrid systems: an ounce of realism can save an infinity of states, (Computer Science Logic, (1999), Springer), 126-139 · Zbl 0944.68119
[14] Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M. W.; Scott, D. S., Continuous lattices and domains, Encyclopedia of Mathematics and Its Applications, vol. 93, (2003), Cambridge University Press
[15] Goebel, R.; Sanfelice, R. G.; Teel, A., Hybrid dynamical systems, IEEE Control Syst. Mag., 29, 2, 28-93, (2009) · Zbl 1395.93001
[16] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., Algorithmic analysis of nonlinear hybrid systems, IEEE Trans. Automat. Control, 43, 4, 540-554, (1998) · Zbl 0918.93019
[17] Keimel, K., Domain theory its ramifications and interactions, The Seventh International Symposium on Domain Theory and Its Applications (ISDT), Electron. Notes Theor. Comput. Sci., 333, Suppl. C, 3-16, (2017)
[18] Kelley, J. L., General topology, (1975), Springer · Zbl 0306.54002
[19] Kong, S.; Gao, S.; Chen, W.; Clarke, E., Dreach: δ-reachability analysis for hybrid systems, (International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2015), Springer), 200-205
[20] Lee, E. A., Cyber physical systems: design challenges, (11th IEEE International Symposium on Object Oriented Real-Time Distributed Computing, ISORC 2008, (2008), IEEE), 363-369
[21] Platzer, A., Differential dynamic logic for hybrid systems, J. Automat. Reason., 41, 2, 143-189, (2008) · Zbl 1181.03035
[22] Rajkumar, R. R.; Lee, I.; Sha, L.; Stankovic, J., Cyber-physical systems: the next computing revolution, (Proceedings of the 47th Design Automation Conference, (2010), ACM), 731-736
[23] Zhang, J.; Johansson, K. H.; Lygeros, J.; Sastry, S., Dynamical systems revisited: hybrid systems with Zeno executions, (International Workshop on Hybrid Systems: Computation and Control, (2000), Springer), 451-464 · Zbl 0982.93046
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.