Denotational semantics of hybrid automata. (English) Zbl 1123.68056
Summary: We introduce a denotational semantics for non-linear hybrid automata and relate it to the operational semantics given in terms of hybrid trajectories. The semantics is defined as least fixpoint of an operator on the continuous domain of functions of time that take values in the lattice of compact subsets of \(n\)-dimensional Euclidean space. The semantic function assigns to every point in time the set of states the automaton can visit at that time, starting from one of its initial states. Our main results are the correctness and computational adequacy of the denotational semantics with respect to the operational semantics given in terms of hybrid trajectories. Moreover, we show that our denotational semantics can be effectively computed, which allows for the effective analysis of a large class of non-linear hybrid automata.
Software:
HyTechReferences:
| [1] | Abramsky, S.; Jung, A., Domain theory, (Abramsky, S.; Gabbay, D.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 3 (1994), Clarendon Press) · Zbl 0829.68111 |
| [2] | Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T.; 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] | Alur, R.; Henzinger, T.; Ho, P.-H., Automatic symbolic verification of embedded systems, IEEE Trans. Softw. Eng., 22, 3, 181-201 (1996) |
| [4] | Aubin, J.-P., Viability Theory (1991), Birkhäuser · Zbl 0755.93003 |
| [5] | Coddington, E. A.; Levinson, N., Theory of Ordinary Differential Equations (1955), McGraw-Hill · Zbl 0042.32602 |
| [6] | Czipszer, J.; Gehér, L., Extension of functions satisfying a Lipschitz condition, Acta Math. Hungar., 6, 1-2 (1955) · Zbl 0064.05406 |
| [7] | Edalat, A., Dynamical systems, measures and fractals via domain theory, Inform. and Comput., 120, 1, 32-48 (1995) · Zbl 0834.58029 |
| [8] | Edalat, A., Power domains and iterated function systems, Inform. and Comput., 124, 182-197 (1996) · Zbl 0916.54014 |
| [9] | Edalat, A.; Krznarić, M.; Lieutier, A., Domain-theoretic solution of differential equations (scalar fields), Proceedings of MFPS XIX. Proceedings of MFPS XIX, Electron. Notes Theor. Comput. Sci., 83 (2004) · Zbl 1337.68300 |
| [10] | Edalat, A.; Lieutier, A., Domain theory and differential calculus (functions of one variable), Math. Structures Comput. Sci., 14 (2004) · Zbl 1062.03037 |
| [11] | Edalat, A.; Pattinson, D., A domain theoretic account of Euler’s method for solving initial value problems, Proceedings of PARA 2004. Proceedings of PARA 2004, Lecture Notes in Comput. Sci., 3732, 112-121 (2004) |
| [12] | Edalat, A.; Pattinson, D., A domain theoretic account of Picard’s theorem, Proceedings of ICALP 2004. Proceedings of ICALP 2004, Lecture Notes in Comput. Sci., 3142, 494-505 (2004) · Zbl 1098.65078 |
| [13] | Edalat, A.; Pattinson, D.; Escardó, M., Domain theoretic solutions of initial value problems for unbounded vector fields, Proceedings of MFPS XXI. Proceedings of MFPS XXI, Electron. Notes Theoret. Comput. Sci., 155, 565-581 (2005) · Zbl 1273.65097 |
| [14] | Erker, T.; Escardò, M.; Keimel, K., The way-below relation of function spaces over semantic domains, Topology Appl., 89, 1-2, 61-74 (1998) · Zbl 0922.06009 |
| [15] | Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M.; Scott, D., Continuous Lattices and Domains (2003), Cambridge University Press · Zbl 1088.06001 |
| [16] | Henzinger, T.; Inan, M.; Kurshan, R., The theory of hybrid automata, Verification of Digital and Hybrid Systems. Verification of Digital and Hybrid Systems, NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., 170, 265-292 (2000) · Zbl 0959.68073 |
| [17] | Henzinger, T.; Ho, P.-H.; Wong-Toi, H., HYTECH: a model checker for hybrid systems, Internat. J. Softw. Tools for Tech. Transf., 1, 1-2, 110-122 (1997) · Zbl 1060.68603 |
| [18] | Henzinger, T.; Ho, P.-H.; Wong-Toi, H., Algorithmic analysis of nonlinear hybrid systems, IEEE Trans. Automat. Control, 43, 540-554 (1998) · Zbl 0918.93019 |
| [19] | Henzinger, T.; Horowitz, B.; Majumdar, R.; Wong-Toi, H., Beyond HYTECH: hybrid systems analysis using interval numerical methods, Proceedings of HSCC 2000. Proceedings of HSCC 2000, Lecture Notes in Comput. Sci., 1790, 130-144 (2000) · Zbl 0938.93552 |
| [20] | Hutchinson, J. E., Fractals and self-similarity, Indiana Univ. Math. J., 30, 713-747 (1981) · Zbl 0598.28011 |
| [21] | Lygeros, J.; Godbole, D.; Sastry, S., Verified hybrid controllers for automated vehicles, IEEE Trans. Automat. Control, 43, 4, 522-539 (1998) · Zbl 0904.90057 |
| [22] | Müller, O.; Stauner, T., Modelling and verification using linear hybrid automata – a case study, Math. Comp. Model. Dyn., 6, 1, 71-89 (2000) · Zbl 0938.93568 |
| [23] | Simic, S.; Johansson, K.; Sastry, S.; Lygeros, J.; Lynch, N.; Krogh, B., Towards a geometric theory of hybrid systems, Proceedings of HSCC 2000. Proceedings of HSCC 2000, Lecture Notes in Comput. Sci., 1790, 421-436 (2000) · Zbl 0963.93044 |
| [24] | Tomlin, C.; Pappas, G.; Sastry, S., Conflict resolution for air traffic management: a study in muti-agent hybrid systems, IEEE Trans. Automat. Control, 43, 4, 509-521 (1998) · Zbl 0904.90113 |
| [25] | Varaiya, P., Smart cars on smart roads: problems of control, IEEE Trans. Automat. Control, 38, 2 (1993) |
| [26] | Weihrauch, K., Computable Analysis (2000), Springer · Zbl 0956.68056 |
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.
