Abstract
We identify a new class of decidable hybrid automata: namely, parallel compositions of semi-algebraic o-minimal automata. The class we consider is fundamental to hierarchical modeling in many exemplar systems, both natural and engineered. Unfortunately, parallel composition, which is an atomic operator in such constructions, does not preserve the decidability of reachability. Luckily, this paper is able to show that when one focuses on the composition of semi-algebraic o-minimal automata, it is possible to translate the decidability problem into a satisfiability problem over formulæinvolving both real and integer variables. While in the general case such formulæ would be undecidable, the particular format of the formulæ obtained in our translation allows combining decidability results stemming from both algebraic number theory and first-order logic over (ℝ, 0, 1, + , *, < ) to yield a novel decidability algorithm. From a more general perspective, this paper exposes many new open questions about decidable combinations of real/integer logics.
This work is partially supported by PRIN ”BISCA” 2006011235, FIRB ”LIBI” RBLA039M7M, two NSF ITR grants, and one NSF EMT grant.
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.
Similar content being viewed by others
References
Casagrande, A., Corvaja, P., Piazza, C., Mishra, B.: Composing semi-algebraic o-minimal automata. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 668–671. Springer, Heidelberg (2007)
Casagrande, A., Corvaja, P., Piazza, C., Mishra, B.: Parallel composition of semi-algebraic o-minimal automata (January 2008), http://www.dimi.uniud.it/piazza/PAPERS/parallel.pdf
Alur, R., Henzinger, T.A., Ho, P.H.: Automatic Symbolic Verification of Embedded Systems. In: IEEE Real-Time Systems Symposium 1993, pp. 2–11. IEEE Press, Los Alamitos (1993)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proc. of Symp. on Theory of Computing (STOCS 1995), pp. 373–382 (1995)
Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal Hybrid Systems. Mathematics of Control, Signals, and Systems 13, 1–21 (2000)
Brihaye, T., Michaux, C., Rivière, C., Troestler, C.: On O-Minimal Hybrid Systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 219–233. Springer, Heidelberg (2004)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Univ. California Press (1951)
van den Dries, L.: Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series, vol. 248. Cambridge University Press, Cambridge (1998)
Casagrande, A., Piazza, C., Mishra, B.: Semi-Algebraic Constant Reset Hybrid Automata - SACoRe. In: Proc. of the 44rd Conference on Decision and Control (CDC 2005), pp. 678–683. IEEE Press, Los Alamitos (2005)
Henzinger, T.A.: The Theory of Hybrid Automata. In: Proc. of IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278–292. IEEE Press, Los Alamitos (1996)
Miller, J.S.: Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 296–309. Springer, Heidelberg (2000)
Pottier, L.: Minimal solutions of linear diophantine systems: Bounds and algorithms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 162–173. Springer, Heidelberg (1991)
Bourbaki, N.: Elements of Mathematics. General topology II. Springer, Heidelberg (1989)
Cohen, H.: A Course in Computational Algebraic Number Theory. Graduate Texts in Mathematics, vol. 138. Springer, Heidelberg (1993)
Casagrande, A., Corvaja, P., Piazza, C., Mishra, B.: Synchronized product of semi-algebraic o-minimal hybrid automata. Technical report, University of Udine (October 2006), http://fsv.dimi.uniud.it/papers/syncro.pdf
Casagrande, A., Casey, K., Falchi, R., Piazza, C., Ruperti, B., Vizzotto, G., Mishra, B.: Translating Time-Course Gene Expression Profiles into Semi-algebraic Hybrid Automata Via Dimensionality Reduction. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) AB 2007. LNCS, vol. 4545, pp. 51–65. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Casagrande, A., Corvaja, P., Piazza, C., Mishra, B. (2008). Decidable Compositions of O-Minimal Automata. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)