Abstract
Control synthesis is slowly transcending its traditional application domain within engineering to find interesting and useful applications in computer science. Synthesis of interfaces, distributed network monitors or reactive programs are some examples that benefit from this design paradigm. In this paper we shed new light on the interplay between the fundamental notion of bisimulation and the control synthesis problem. We first revisit the notion of alternating simulation introduced by Alur and co-workers as it naturally captures important ingredients of the control synthesis problem. We then show that existence of controllers enforcing specifications through bisimulation, alternating simulation or simulation can be characterized by the existence of certain alternating simulations and bisimulations between the specification and the system to be controlled. These results highlight and unify the role of simulations and bisimulations in the control synthesis setting for a wide range of concurrency models. This is achieved by developing our study within the framework of open maps. We illustrate our results on transition systems and timed transition systems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ramadge, P., Wonham, W.M.: The control of discrete event systems. Proceedings of IEEE 77, 81–98 (1989)
de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001)
Benveniste, A., Haar, S., Fabre, E., Jard, C.: Distributed monitoring of concurrent and asynchronous systems. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 1–26. Springer, Heidelberg (2003)
Tabuada, P., Pappas, G.J.: Linear time logic control of linear systems, Submitted for publication (2004), Available at: www.nd.edu/~ptabuada
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pp. 170–190 (1989)
Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Press, I. (ed.) Proceedings of the 31st Annual Symposium on Foundations of Computer Sience, St. Louis, Missouri, pp. 746–757 (1990)
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266 (1982)
Manna, Z., Wolper, P.: Synthesis of communication processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems 6, 68–93 (1984)
Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127, 164–185 (1996)
Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, Gabbay, Maibaum (eds.) Handbook of Logic and Foundations of Theoretical Computer Science, vol. 4. Oxford University Press, London (1994)
Nielsen, M., Cheng, A.: Observing behaviour categorically. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 263–278. Springer, Heidelberg (1995)
Haghverdi, E., Tabuada, P., Pappas, G.: Bisimulation relations for dynamical and control systems. In: Blute, R., Selinger, P. (eds.) Electronic Notes in Theoretical Computer Science, vol. 69. Elsevier, Amsterdam (2003)
Alur, R., Henzinger, T.A., Kupferman, O., Y. Vardi, M.: Alternating Refinement Relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Madhusudan, P., Thiagarajan, P.: Branching time controllers for discrete event systems. Theoretical Computer Science 274, 117–149 (2002)
Barret, G., Lafortune, S.: Bisimulation, the supervisor control problem and strong model matching for finite state machines. Journal of Discrete Event Systems 8, 337–429 (1998)
Rutten, J.: Coalgebra, concurrency, and control. In: Kluwer (ed.) Proceedings of the 5th Workshop on Discrete Event Systems (WODES 2000), pp. 31–38 (2000)
Overkamp, A.: Supervisory control using failure semantics and partial specifications. IEEE Transactions on Automatic Control 42, 498–510 (1997)
Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Y. Vardi, M.: Open systems in reactive environments: Control and synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92–107. Springer, Heidelberg (2000)
Antoniotti, M., Mishra, B.: NP-completeness of the supervisor synthesis problem for unrestricted CTL specifications. In: Smedinga, R., Spathopoulos, M., Kozk, P. (eds.) Proceedings on the International Workshop on Discrete Event Systems, WODES 1996, Edinburgh, Scotland, UK (1996)
Shengbing, J., Kumar, R.: Supervisory control of discrete event systems with CTL* temporal logic specifications. In: Proceedings of the 40th IEEE Conference on Decision and Control, vol. 5, pp. 4122–4127 (2001)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Borceux, F.: Handbook of Categorical Algebra. Cambridge University Press, Cambridge (1994)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Nielsen, M., Hune, T.S.: Bisimulation and open maps for timed transition systems. Fundamenta Informaticae 38, 61–77 (1999)
Moody, J.O., Antsaklis, P.J.: Supervisory Control of Discrete Event Systems Using Petri Nets. Kluwer Academic Publishers, Dordrecht (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tabuada, P. (2004). Open Maps, Alternating Simulations and Control Synthesis. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive