Abstract
The advent of computer-controlled embedded systems coupled to physical environments requires the development of new theories of dynamic system modeling, specification and verification. We present Timed ∀-automata, a generalization of ∀-automata [10], for the specification and verification of dynamic systems that can be discrete, continuous or hybrid. Timed ∀-automata are finite state and serve as a formal requirements specification language for dynamic systems so that (1) timed as well as temporal properties can be specified or recognized, and (2) global properties of either discrete or continuous behaviors can be characterized. In addition, we propose a formal model-checking method for behavior verification of dynamic systems. This method generalizes stability analysis of dynamic systems and can be completely automated for discrete-time finite-domain systems.
Fellow, Canadian Institute for Advanced Research
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, T. A. Henzinger, and P. Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, number 736 in Lecture Notes on Computer Science, pages 209–229. Springer-Verlag, 1993.
R. Alur and D. Dill. Automata for modeling real-time systems. In M. S. Paterson, editor, ICALP90: Automata, Languages and Programming, number 443 in Lecture Notes on Computer Science, pages 322–335. Springer-Verlag, 1990.
B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using Time Petri Nets. IEEE Transactions on Software Engineering, 17(3):259–273, March 1991.
R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors. Hybrid Systems. Number 736 in Lecture Notes on Computer Science. Springer-Verlag, 1993.
T. A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J.W. deBakker, C. Huizing, W.P. dePoever, and G. Rozenberg, editors, Real-Time: Theory in Practice, number 600 in Lecture Notes on Computer Science, pages 226–251. Springer-Verlag, 1991.
G. F. Khilmi. Qualitative Methods in the Many Body Problem. Science Publishers Inc. New York, 1961.
N. G. Leveson and P. G. Neumann, editors. IEEE Transactions on Software Engineering. IEEE Computer Society, January 1993. Special Issue on Software for Critical Systems.
D. G. Luenberger. Introduction to Dynamic Systems: Theory, Models and Applications. John Wiley & Sons, 1979.
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. deBakker, C. Huizing, W.P. dePoever, and G. Rozenberg, editors, Real-Time: Theory in Practice, number 600 in Lecture Notes on Computer Science, pages 448–484. Springer-Verlag, 1991.
Z. Manna and A. Pnueli. Specification and verification of concurrent programs by ∀-automata. In Proc. 14th Ann. ACM Symp. on Principles of Programming Languages, pages 1–12, 1987.
R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, 1971.
H. L. Royden. Real Analysis, 3rd edition. Macmillan Publishing Company, 1988.
M. Sahota and A. K. Mackworth. Can situated robots play soccer? In Proc. Artificial Intelligence 94, pages 249–254, Banff, Alberta, May 1994.
W. Thomas. Automata on infinite objects. In Jan Van Leeuwen, editor, Handbook of Theoretical Computer Science. MIT Press, 1990.
P. Wolper. Temporal logic can be more expressive. Information and Control, 56:72–99, 1983.
Y. Zhang. A foundation for the design and analysis of robotic systems and behaviors. Technical Report 94-26, Department of Computer Science, University of British Columbia, 1994. Ph.D. thesis.
Y. Zhang and A. K. Mackworth. Specification and verification of constraint-based dynamic systems. In A. Borning, editor, Principles and Practice of Constraint Programming, Lecture Notes in Computer Science 874, pages 229–242. Springer Verlag, 1994.
Y. Zhang and A. K. Mackworth. Will the robot do the right thing? In Proc. Artificial Intelligence 94, pages 255–262, Banff, Alberta, May 1994.
Y. Zhang and A. K. Mackworth. Constraint Nets: A semantic model for hybrid dynamic systems. Theoretical Computer Science, 138(1):211–239, 1995. Special Issue on Hybrid Systems.
Y. Zhang and A. K. Mackworth. Constraint programming in constraint nets. In V. Saraswat and P. Van Hentenryck, editors, Principles and Practice of Constraint Programming, pages 49–68. MIT Press, 1995.
Y. Zhang and A. K. Mackworth. Synthesis of hybrid constraint-based controllers. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, Lecture Notes in Computer Science 999, pages 552–567. Springer Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, Y., Mackworth, A.K. (1996). Specification and verification of hybrid dynamic systems with Timed ∀-automata. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020978
Download citation
DOI: https://doi.org/10.1007/BFb0020978
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61155-4
Online ISBN: 978-3-540-68334-6
eBook Packages: Springer Book Archive