AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
The hybrid automaton has been proposed as a formal model for hybrid systems

The theory of hybrid automata

New Brunswick, NJ, pp.278-292, (1996)

Cited by: 2531|Views107
EI WOS

Abstract

We summarize several recent results about hybrid automata. Our goal is to demonstrate that concepts from the theory of discrete concurrent systems can give insights into partly continuous systems, and that methods for the verification of finite-state systems can be used to analyze certain systems with uncountable state spaces.

Code:

Data:

Introduction
  • A hybrid automaton is a formal model for a mixed discrete-continuous system. The authors classify hybrid automata acoording to what questions about their behavior can be answered algorithmically.
  • Theorem 3.1 Symbolic analysis of linear hybrid automata] 5, 9] For every linear hybrid automaton H, the set of linear H-predicates permits the symbolic analysis of the time-abstract transition system SHa .
  • Theorem 3.2 Time-abstract bisimilarity of singular automata] 6, 5] If H is a singular automaton, and is a nite set of rectangular H-predicates, the time-abstract -bisimilarity relation of H is nitary.
Highlights
  • A hybrid automaton is a formal model for a mixed discrete-continuous system
  • As embedded computing becomes ubiquitous, hybrid systems are increasingly employed in safety-critical applications, making reliability a prime concern
  • The hybrid automaton has been proposed as a formal model for hybrid systems
  • Theorem 3.1 Symbolic analysis of linear hybrid automata] 5, 9] For every linear hybrid automaton H, the set of linear H-predicates permits the symbolic analysis of the time-abstract transition system SHa
  • For discrete-time hybrid automata, veri cation questions can be answered even in the multirectangular case. This is because for every discrete-time multirectangular hybrid automaton H, the set of rectangular H-predicates permits the symbolic analysis of the time-abstract thryabnrsiidtiaountosymstaetmonSwHait.h
  • The alternative interpretation of 9U over nite pre xes of divergent trajectories requires that the underlying hybrid automaton irtsassehiulmlcecnthiopansnlnevtizthagearueonidtlafoanHt.rsotteFacaxaotonierlsndistnadeHeqinltaitinnwroizaeniHlathshrfa-oopvhrfdreymieHvbtduehrilricreadgeaesstauanenumltztptsonqe=zm-idrn,(oiatvoatheRoterneng:ndo9eHntn3thztree(aantznjiaoemd=dcldteai1onditrce^iitlaoerorsna9c.chk3oeyfHsnea)nzko)tjHruodcennamzecn,Htnt3bhnte.oz5ees it follows that this is always possible for singular and 2D rectangular automata. 2
Results
  • Corollary 3.1 Symbolic -calculus model checking for singular automata] The procedure MuApprox terminates if given the time-abstract transition system of a singular automaton H and an H-formula of the rectangular -calculus.
  • Is a 2D rectangular automaton, and is a nite set of rectangular H-predicates, the time-abstract -similarity relation of H is nitary.
  • Corollary 3.2 Symbolic -calculus model checking for 2D rectangular automata] The procedure MuApprox terminates if given the time-abstract transition system of a 2D rectangular automaton H and an existential or universal H-formula of the rectangular -calculus.
  • If H is a timed automaton, is a nite set of rectangular H-predicates, and q and r are two states of H, it can be decided if q and r are timed -similar 17, 48, 47].
  • This is because for every discrete-time multirectangular hybrid automaton H, the set of rectangular H-predicates permits the symbolic analysis of the time-abstract thryabnrsiidtiaountosymstaetmonSwHait.h
  • It follows that if H is a either bounded invariant discrete-time rectangles or multirectangular nonnegative ow rectangles, and is a nite set of rectangular H-predicates, the timeabstract -bisimilarity relation of H is nitary.
  • These transition systems, may not be directly useful forproving assertions about the behavior of a hybrid automaton H, bjeecctaouryseoefaHchattracjeercttaoinrydoisfcSreHtteapnodinStHas. only samples a piecewise-continuous traIn the following, the authors restrict themselves to the time-abstract view.
Conclusion
  • De nition 3.10 Model checking] The model-checking problem for a class H of hybrid automata and a computation tree logic L asks, given a hybrid automaton H from H and an H-formula from L, if ] contains all initial states of H.
  • Condition If H is a true, and a single hybrid automaton control switch and z is not a with the variable jump of H, the composition HkHz is called a clock extension of H.
  • The alternative interpretation of 9U over nite pre xes of divergent trajectories requires that the underlying hybrid automaton irtsassehiulmlcecnthiopansnlnevtizthagearueonidtlafoanHt.rsotteFacaxaotonierlsndistnadeHeqinltaitinnwroizaeniHlathshrfa-oopvhrfdreymieHvbtduehrilricreadgeaesstauanenumltztptsonqe=zm-idrn,(oiatvoatheRoterneng:ndo9eHntn3thztree(aantznjiaoemd=dcldteai1onditrce^iitlaoerorsna9c.chk3oeyfHsnea)nzko)tjHruodcennamzecn,Htnt3bhnte.oz5ees it follows that this is always possible for singular and 2D rectangular automata.
Funding
  • This research was supported in part by the O ce of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Air Force O ce of Scienti c Research contract F49620-93-1-0056, by the Army Research O ce MURI grant DAAH-04-961-0341, by the Advanced Research Projects Agency grant NAG2-892, and by the SemiconducytAorpRreelsiemairncahrCy ovreprsoiroantioofnthcoisnptraapcetr9a6p-pDeCa-r3e2d4i.n03t6h.e Proceedings of the 11th Annual IEEE SymzEpmosaiuilm: toanh@Leoegcics.binerCkeolmeyp.eudteur
Reference
  • 1] M. Abadi and L. Lamport. An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems, 16(5):1543{1571, 1994.
    Google ScholarLocate open access versionFindings
  • 2] R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2{34, 1993.
    Google ScholarLocate open access versionFindings
  • 3] R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3{34, 1995.
    Google ScholarLocate open access versionFindings
  • 4] R. Alur, C. Courcoubetis, and T.A. Henzinger. Computing accumulated delays in real-time systems. Formal Methods in System Design, 11(2):137{ 156, 1997.
    Google ScholarLocate open access versionFindings
  • 5] R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the speci cation and veri cation of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I, Lecture Notes in Computer Science 736, pages 209{229. Springer-Verlag, 1993.
    Google ScholarLocate open access versionFindings
  • 6] R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183{235, 1994.
    Google ScholarLocate open access versionFindings
  • 7] R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74{106. Springer-Verlag, 1992.
    Google ScholarLocate open access versionFindings
  • 8] R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In A. Mazurkiewicz and J. Winkowski, editors, CONCUR 97: Concurrency Theory, Lecture Notes in Computer Science 1243, pages 74{8SpringerVerlag, 1997.
    Google ScholarLocate open access versionFindings
  • 9] R. Alur, T.A. Henzinger, and P.-H. Ho. Automatic symbolic veri cation of embedded systems. IEEE Transactions on Software Engineering, 22(3):181{201, 1996.
    Google ScholarLocate open access versionFindings
  • 10] R. Alur, T.A. Henzinger, and M.Y. Vardi. Parametric real-time reasoning. In Proceedings of the 25th Annual Symposium on Theory of Computing, pages 592{601. ACM Press, 1993.
    Google ScholarLocate open access versionFindings
  • Henzinger, and E.D. Sontag, editors, Hybrid Systems III, Lecture Notes in Computer Science 1066, pages 220{231. Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 12] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Uppaal: a tool-suite for automatic veri cation of real-time systems. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, Lecture Notes in Computer Science 1066, pages 232{243. Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 13] D. Bosscher, I. Polak, and F. Vaandrager. Veri cation of an audio-control protocol. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science 863, pages 170{192. Springer-Verlag, 1994.
    Google ScholarLocate open access versionFindings
  • 14] A. Bouajjani, R. Echahed, and R. Robbana. Veri cation of context-free timed systems using linear hybrid observers. In D.L. Dill, editor, CAV 94: Computer-aided Veri cation, Lecture Notes in Computer Science, pages 118{131. Springer-Verlag, 1994.
    Google ScholarLocate open access versionFindings
  • 15] A. Bouajjani, R. Echahed, and J. Sifakis. On model checking for real-time properties with durations. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science, pages 147{159. IEEE Computer Society Press, 1993.
    Google ScholarLocate open access versionFindings
  • 16] A. Bouajjani and R. Robbana. Verifying !-regular properties for subclasses of linear hybrid systems. In P. Wolper, editor, CAV 95: Computeraided Veri cation, Lecture Notes in Computer Science 939, pages 437{450. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 17] K. Cerans. Decidability of bisimulation equivalence for parallel timer processes. In G. von Bochmann and D.K. Probst, editors, CAV 92: Computeraided Veri cation, Lecture Notes in Computer Science 663, pages 302{315. Springer-Verlag, 1992.
    Google ScholarLocate open access versionFindings
  • 18] J.C. Corbett. Timing analysis of Ada tasking programs. IEEE Transactions on Software Engineering, 22(7):461{483, 1996.
    Google ScholarLocate open access versionFindings
  • R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, Lecture Notes in Computer Science 1066, pages 208{2Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 20] D.L. Dill. Timing assumptions and veri cation of nite-state concurrent systems. In J. Sifakis, editor, CAV 89: Automatic Veri cation Methods for Finite-state Systems, Lecture Notes in Computer Science 407, pages 197{212. Springer-Verlag, 1989.
    Google ScholarLocate open access versionFindings
  • 21] R. Gawlick, R. Segala, J.F. Sogaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. In S. Abiteboul and E. Shamir, editors, ICALP 94: Automata, Languages, and Programming, Lecture Notes in Computer Science 820, pages 166{177. Springer-Verlag, 1994.
    Google ScholarLocate open access versionFindings
  • 22] V. Gupta, T.A. Henzinger, and R. Jagadeesan. Robust timed automata. In O. Maler, editor, HART 97: Hybrid and Real-time Systems, Lecture Notes in Computer Science 1201, pages 331{345. Springer-Verlag, 1997.
    Google ScholarLocate open access versionFindings
  • 23] M.R. Henzinger, T.A. Henzinger, and P.W. Kopke. Computing simulations on nite and in nite graphs. In Proceedings of the 36rd Annual Symposium on Foundations of Computer Science, pages 453{462. IEEE Computer Society Press, 1995.
    Google ScholarLocate open access versionFindings
  • 24] T.A. Henzinger. Sooner is safer than later. Information Processing Letters, 43(3):135{141, 1992.
    Google ScholarLocate open access versionFindings
  • 25] T.A. Henzinger. Hybrid automata with nite bisimulations. In Z. Fulop and F. Gecseg, editors, ICALP 95: Automata, Languages, and Programming, Lecture Notes in Computer Science 944, pages 324{335. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 26] T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In P. Wolper, editor, CAV 95: Computer-aided Veri cation, Lecture Notes in Computer Science 939, pages 225{238. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 27] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 56{65. IEEE Computer Society Press, 1995.
    Google ScholarLocate open access versionFindings
  • E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, and B. Ste en, editors, TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1019, pages 41{71. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 29] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. In O. Grumberg, editor, CAV 97: Computer-aided Veri cation, Lecture Notes in Computer Science 1254, pages 460{463. SpringerVerlag, 1997.
    Google ScholarLocate open access versionFindings
  • 30] T.A. Henzinger and P.W. Kopke. State equivalences for rectangular hybrid automata. In U. Montanari and V. Sassone, editors, CONCUR 96: Concurrency Theory, Lecture Notes in Computer Science 1119, pages 530{545. Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 31] T.A. Henzinger and P.W. Kopke. Discrete-time control for rectangular hybrid automata. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, ICALP 97: Automata, Languages, and Programming, Lecture Notes in Computer Science 1256, pages 582{593. Springer-Verlag, 1997.
    Google ScholarLocate open access versionFindings
  • 32] T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proceedings of the 27th Annual Symposium on Theory of Computing, pages 373{382. ACM Press, 1995.
    Google ScholarLocate open access versionFindings
  • 33] T.A. Henzinger, P.W. Kopke, and H. Wong-Toi. The expressive power of clocks. In Z. Fulop and F. Gecseg, editors, ICALP 95: Automata, Languages, and Programming, Lecture Notes in Computer Science 944, pages 417{428. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 34] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193{ 244, 1994.
    Google ScholarLocate open access versionFindings
  • 35] T.A. Henzinger and H. Wong-Toi. Linear phase-portrait approximations for nonlinear hybrid systems. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, Lecture Notes in Computer Science 1066, pages 377{388. Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 36] T.A. Henzinger and H. Wong-Toi. Using HyTech to synthesize control parameters for a steam boiler. In J.-R. Abrial, E. Borger, and H. Langmaack, editors, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science 1165, pages 265{282. Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 37] P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, CAV 95: Computer-aided Veri cation, Lecture Notes in Computer Science 939, pages 381{394. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 38] Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration graphs: a class of decidable hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science 736, pages 179{208. Springer-Verlag, 1993.
    Google ScholarLocate open access versionFindings
  • 39] N.A. Lynch, R. Segala, F. Vaandrager, and H.B. Weinberg. Hybrid I/O Automata. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, Lecture Notes in Computer Science 1066, pages 496{510. Springer-Verlag, 1996.
    Google ScholarLocate open access versionFindings
  • 40] O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 447{484. Springer-Verlag, 1992.
    Google ScholarLocate open access versionFindings
  • 41] O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In E.W. Mayr and C. Puech, editors, STACS 95: Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 900, pages 229{242. Springer-Verlag, 1995.
    Google ScholarLocate open access versionFindings
  • 42] S. Nadjm-Tehrani and J.-E. Stromberg. Proving dynamic properties in an aerospace application. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 2{10. IEEE Computer Society Press, 1995.
    Google ScholarLocate open access versionFindings
  • 43] X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. An approach to the description and analysis of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I, Lecture Notes in Computer Science 736, pages 149{178. Springer-Verlag, 1993.
    Google ScholarLocate open access versionFindings
  • 44] A. Puri, V. Borkar, and P. Varaiya. "-approximation of di erential inclusions. In R. Alur, T.A. Henzinger, and E.D. Sontag, editors, Hybrid Systems III, Lecture Notes in Computer Science 1066, pages 362{376. SpringerVerlag, 1996.
    Google ScholarLocate open access versionFindings
  • 45] A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular di erential inclusions. In D.L. Dill, editor, CAV 94: Computer-aided Veri cation, Lecture Notes in Computer Science 818, pages 95{104. SpringerVerlag, 1994.
    Google ScholarLocate open access versionFindings
  • 46] T. Stauner, O. Muller, and M. Fuchs. Using HyTech to verify an automotive control system. In O. Maler, editor, HART 97: Hybrid and Realtime Systems, Lecture Notes in Computer Science 1201, pages 139{153. Springer-Verlag, 1997.
    Google ScholarLocate open access versionFindings
  • 47] S. Tasiran, R. Alur, R.P. Kurshan, and R.K. Brayton. Verifying abstractions of timed systems. In U. Montanari, editor, CONCUR 96: Concurrency Theory, Lecture Notes in Computer Science, pages 546{562. SpringerVerlag, 1996.
    Google ScholarLocate open access versionFindings
  • 48] K. Cerans, J.C. Godskesen, and K.G. Larsen. Timed modal speci cation: Theory and tools. In C. Courcoubetis, editor, CAV 93: Computeraided Veri cation, Lecture Notes in Computer Science 697, pages 253{267. Springer-Verlag, 1993.
    Google ScholarLocate open access versionFindings
  • 49] F. Wang. Timing behavior analysis for real-time systems. In Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 112{ 122. IEEE Computer Society Press, 1995.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科