Abstract
In a trace-based world, the modular specification, verification, and control of live systems require each module to be receptive; that is, each module must be able to meet its liveness assumptions no matter how the other modules behave. In a real-time world, liveness is automatically present in the form of diverging time. The receptiveness condition, then, translates to the requirement that a module must be able to let time diverge no matter how the environment behaves. We study the receptiveness condition for real-time systems by extending the model of reactive modules to timed and hybrid modules. We define the receptiveness of such a module as the existence of a winning strategy in a game of the module against its environment. By solving the game on region graphs, we present an (optimal) Exptime algorithm for checking the receptiveness of prepositional timed modules. By giving a fixpoint characterization of the game, we present a symbolic procedure for checking the receptiveness of linear hybrid modules. Finally, we present an assume-guarantee principle for reasoning about timed and hybrid modules, and a method for synthesizing receptive controllers of timed and hybrid modules.
This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.
R. Alur, D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
K.R. Apt, N. Francez, S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226–241, 1988.
R. Alur, T.A. Henzinger. Local liveness for compositional modeling of fair reactive systems. In Computer-aided Verification, Springer LNCS 939, pp. 166–179, 1995.
R. Alur, T.A. Henzinger. Reactive modules. In Proc. IEEE Symp. Logic in Computer Science, pp. 207–218, 1996.
R. Alur, T.A. Henzinger, P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Trans. Software Engineering, 22:181–201, 1996.
R. Alur, T.A. Henzinger, E.D. Sontag, eds. Hybrid Systems III: Verification and Control. Springer LNCS 1066, 1996.
M. Abadi, L. Lamport. Composing specifications. ACM Trans. Programming Languages and Systems, 15:73–132, 1993.
M. Abadi, L. Lamport. An old-fashioned recipe for real time. In Real Time: Theory in Practice, Springer LNCS 600, pp. 1–27, 1992.
E. Asarin, O. Maler, A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems II, Springer LNCS 999, pp. 1–20, 1995.
P. Antsaklis, A. Nerode, W. Kohn, S. Sastry, eds. Hybrid Systems II. Springer LNCS 999, 1995.
J.W. de Bakker, K. Huizing, W.-P. de Roever, G. Rozenberg, eds. Real Time: Theory in Practice. Springer LNCS 600, 1992.
D.L.Dili. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, 1989.
C. Daws, A. Olivero, S. Tripakis, S. Yovine. The tool Kronos. In Hybrid Systems III, Springer LNCS 1066, pp. 208–219, 1996.
E.A. Emerson, C. Jutla. The complexity of tree automata and logics of programs. In Proc. IEEE Symp. Foundations of Computer Science, pp. 328–337, 1988.
R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel, eds. Hybrid Systems. Springer LNCS 736, 1993.
R. Gawlick, R. Segala, J.F. Sogaard-Andersen, N.A. Lynch. Liveness in timed and untimed systems. In Automata, Languages, and Programming, Springer LNCS 820, pp. 166–177, 1994.
T.A. Henzinger. Sooner is safer than later. Information Processing Letters, 43:135–141, 1992.
T.A. Henzinger, P.-H. Ho, H. Wong-Toi. HyTech: the next generation. In Proc. IEEE Real-time Systems Symp., pp. 56–65,1995.
T.A. Henzinger, P.W. Kopke. Discrete-time control for rectangular hybrid automata. In Automata, Languages, and Programming, Springer LNCS, 1997.
T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111:193–244, 1994.
G. Hoffmann, H. Wong-Toi. The input-output control of real-time discrete-event systems. In Proc. IEEE Real-time Systems Symp., pp. 256–265, 1992.
N.A. Lynch, R. Segala, F. Vaandrager, H.B. Weinberg. Hybrid I/O Automata. In Hybrid Systems III, Springer LNCS 1066, pp. 496–510, 1996.
O. Maler, A. Pnueli, J. Sifakis. On the synthesis of discrete controllers for timed systems. In Theoretical Aspects of Computer Science, Springer LNCS 900, pp. 229–242, 1995.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, Springer LNCS, pp. 123–144, 1984.
P.J. Ramadge, W.M. Wonham. Supervisory control of a class of discrete-event processes. SIAM J. Control and Optimization, 25:206–230, 1987.
S. Tasiran, R. Alur, R.P. Kurshan, R.K. Brayton. Verifying abstractions of timed systems. In Concurrency Theory, Springer LNCS 1119, pp. 546–562, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Henzinger, T.A. (1997). Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds) CONCUR '97: Concurrency Theory. CONCUR 1997. Lecture Notes in Computer Science, vol 1243. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63141-0_6
Download citation
DOI: https://doi.org/10.1007/3-540-63141-0_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63141-5
Online ISBN: 978-3-540-69188-4
eBook Packages: Springer Book Archive