Abstract
At an abstract level hybrid systems are related to variants of Kleene algebra. Since it has recently been shown that Kleene algebras and their variants, like omega algebras, provide a reasonable base for automated reasoning, the aim of the present paper is to show that automated algebraic reasoning for hybrid system is feasible. We mainly focus on applications. In particular, we present case studies and proof experiments to show how concrete properties of hybrid systems, like safety and liveness, can be algebraically characterised and how off-the-shelf automated theorem provers can be used to verify them.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aboul-Hosn, K., Kozen, D.: KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics 16(1–2), 9–33 (2006)
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. Theoretical Comp. Sc. 138(1), 3–34 (1995)
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Hybrid Systems, pp. 209–229. Springer, Heidelberg (1993)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Comp. Sc. 126(2), 183–235 (1994)
Bergstra, J.A., Middleburg, C.A.: Process algebra for hybrid systems. Theoretical Comp. Sc. 335(2-3), 215–280 (2005)
Cho, K.-H., Johansson, K.H., Wolkenhauer, O.: A hybrid systems framework for cellular processes. Biosystems 80(3), 273–282 (2005)
Conway, J.H.: Regular Algebra and Finite Machines. Chapman & Hall, Sydney, Australia (1971)
Corbett, J.M.: Designing hybrid automated manufacturing systems: A european perspective. In: Conference on Ergonomics of Hybrid Automated Systems I, pp. 167–172. Elsevier, Amsterdam (1988)
Damm, W., Hungar, H., Olderog, E.-R.: On the verification of cooperating traffic agents. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 77–110. Springer, Heidelberg (2004)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)
Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proc. of the IEEE 88(7), 985–1010 (2000)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comp. Logic 7(4), 798–833 (2006)
Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the european train control system. In: FMCAD 2006, pp. 76–77. IEEE Press, Los Alamitos (2006)
Henzinger, T.A.: The theory of hybrid automata. In: Kemal, M. (ed.) IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292. IEEE Press, Los Alamitos (1996): Extended Version: Kemal, M.: Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol. 170, pp. 265–292. Springer, Heidelberg (2000)
Henzinger, T.A., Horowitz, B., Majumdar, R.: Rectangular hybrid games. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 320–335. Springer, Heidelberg (1999)
Henzinger, T.A., Majumdar, R.: Symbolic model checking for rectangular hybrid systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 142–156. Springer, Heidelberg (2000)
Höfner, P., Möller, B.: Towards an algebra of hybrid systems. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 121–133. Springer, Heidelberg (2006)
Höfner, P., Möller, B.: An algebra of hybrid systems. Technical Report 2007-08, Institut für Informatik, Universität Augsburg (2007)
Höfner, P., Struth, G.: January 14 (2008), http://www.dcs.shef.ac.uk/~georg/ka
Höfner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007)
Höfner, P., Struth, G.: Can refinement be automated? In: Boiten, E., Derrick, J., Smith, G. (eds.) Refine 2007. ENTCS, Elsevier, Amsterdam (to appear, 2007)
Kahl, W.: Calculational relation-algebraic proofs in Isabelle/Isar. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 179–190. Springer, Heidelberg (2004)
Kozen, D.: Kleene algebra with tests. Trans. Prog. Languages and Systems 19(3), 427–443 (1997)
McCune, W.: Prover9 and Mace4, http://www.cs.unm.edu/~mccune/prover9
Möller, B.: Kleene getting lazy. Sc. Comp. Prog. 65, 195–214 (2007)
Müller, O., Stauner, T.: Modelling and verification using linear hybrid automata – A case study. Math. and Comp. Modelling of Dynamical Systems 6(1), 71–89 (2000)
Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR: FLoC 2006, CEUR Workshop Proceedings, vol. 192, pp. 18–33 (2006)
Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)
Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol. 2561, pp. 276–290. Springer, Heidelberg (2002)
Sutcliffe, G., Yury, P.: SRASS-A semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295–310. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Höfner, P. (2008). Automated Reasoning for Hybrid Systems — Two Case Studies —. In: Berghammer, R., Möller, B., Struth, G. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2008. Lecture Notes in Computer Science, vol 4988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78913-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-78913-0_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78912-3
Online ISBN: 978-3-540-78913-0
eBook Packages: Computer ScienceComputer Science (R0)