Abstract
We present novel techniques for eficient controller synthesis for untimed and timed systems with respect to invariance and reachability properties. In the untimed case, we give algorithms for controller synthesis in the context of finite graphs with ticontrollable and uncontrollable edges, distinguishing between the actions of the system and its environment, respectively. The algorithms are tion-the-fly, since they return a controller as soon as one is found, which avoids the generation of the whole state space.
In the timed case, we use the model of titimed automata extended with controllable and uncontrollable discrete transitions. Our controller-synthesis method here is only half on-the-fly, since it relies on the a-priori generation of a finite model (graph) of the timed automaton, as quotient of the titime-abstracting bisimulation. The quotient graph is essentially an untimed graph, upon which we can apply the untimed on-the-fly algorithms to compute a timed controller.
Chapter PDF
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2–34, 1993.
K. Altisen. Généeration automatique d’ordonnancements pour systéemes temporisées. Technical report, Méemoire de DEA, Ensimag, Grenoble, 1998.In french.
Rajeev Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Department of Computer Science, Stanford University, 1991.
E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems.In Hybrid Systems II, 1995.
M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a model-checking tool for real-time systems. In CAV’98, 1998.
D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, pages 197–212. Springer-Verlag, 1989.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, Verification and Control, volume 1066 of LNCS, pages 208–219. Springer-Verlag, 1996.
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.
G. Hoffmann and H. Wong Toi. The input-output control of real-time discrete event systems. In 30th IEEE Conf. on Decision and Control, 1991.
G. Hoffmann and H. Wong Toi. Symbolic synthesis of supervisory controllers. In American Control Conference, 1992.
M. Le Borgne. Dynamical Systems over finite fields. PhD thesis, Université de Rennes, 1993. In French.
O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In STACS’ 95, 1995.
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In ACM Symp. POPL, 1989.
P. Ramadge and W. Wonham. Supervisory control of a class of discrete event processes. SIAM J. Control Optim., 25(1), January 1987.
S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourrier de Grenoble, 1998.
S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Proc. 8th Conference Computer-Aided Verification, CAV’96, Rutgers, NJ, volume 1102 of LNCS, pages 232–243. Springer-Verlag, July 1996.
W. Wonham and C. Meder. The TTCT tool. Personal communication, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tripakis, S., Altisen, K. (1999). On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_15
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive