Abstract
This paper presents algorithms for the automatic synthesis of real-time controllers by finding a winning strategy for certain games defined by the timed-automata of Alur and Dill. In such games, the outcome depends on the players' actions as well as on their timing. We believe that these results will pave the way for the application of program synthesis techniques to the construction of real-time embedded systems from their specifications.
This research was supported in part by the France-Israel project for cooperation in Computer Science and by the European Community ESPRIT Basic Research Action Projects REACT (6021). Verimag is a joint laboratory of cnrs, inpg, ujf and verilog sa. spectre is a project of inria.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur and D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183–235, 1994.
R. Alur, C. Courcoubetis, and D.L. Dill, Model Checking in Dense Real Time, Information and Computation 104, 2–34, 1993.
M. Abadi, L. Lamport, and P. Wolper, Realizable and Unrealizable Concurrent Program Specifications. In Proc. 16th Int. Collog. Aut. Lang. Prog., volume 372 of Lect. Notes in Comp. Sci., pages 1–17. Springer-Verlag, 1989.
B.A. Brandin and W.M. Wonham, Supervisory Control of Timed Discreteevent Systems, IEEE Transactions on Automatic Control, 39, 329–342, 1994.
J.R. Büchi and L.H. Landweber, Solving Sequential Conditions by Finite-state Operators, Trans. of the AMS 138, 295–311, 1969.
E.A. Emerson and C.J. Jutla, Tree Automata, μ-calculus and Determinacy, Proc. 32nd FOCS, 1991.
Y. Gurevich and L. Harrington, Trees, Automata and Games, Proc. 14th STOC, 1982.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Modelchecking for Real-time Systems, Information and Computation 111, 193–244, 1994.
M. Le Borgne, Dynamical Systems over Finite Fields, Ph.D. thesis, Univ. Rennes 1, 1993 (In French).
A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module, In Proc. 16th ACM Symp. Princ. of Prog. Lang., pages 179–190, 1989.
M.O. Rabin, Automata on Infinite Objects and Church's Problem, AMS, 1972.
P.J. Ramadge and W.M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. of Control and Optimization 25, 206–230, 1987.
P.J. Ramadge and W.M. Wonham, The Control of Discrete Event Systems, Proc. of the IEEE 77, 81–98, 1989.
J.G. Thistle and W.M. Wonham, Control of Infinite Behavior of Finite Automata, SIAM J. of Control and Optimization 32, 1075–1097, 1994.
W. Thomas, On the Synthesis of Strategies in Infinite Games, These proceedings.
B.A. Trakhtenbrot and Y.M. Barzdin, Finite Automata: Behavior and Synthesis, North-Holland, Amsterdam, 1973.
M.Y. Vardi, Personal communication.
H. Wong-Toi and G. Hoffmann, The Control of Dense Real-Time Discrete Event Systems, Technical report STAN-CS-92-1411, Stanford University, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maler, O., Pnueli, A., Sifakis, J. (1995). On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds) STACS 95. STACS 1995. Lecture Notes in Computer Science, vol 900. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59042-0_76
Download citation
DOI: https://doi.org/10.1007/3-540-59042-0_76
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59042-2
Online ISBN: 978-3-540-49175-0
eBook Packages: Springer Book Archive