CONCUR 2004 START ConferenceManager    

Open maps, alternating simulations and control synthesis

Paulo Tabuada

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


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 from specifications 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 trough bisimulation, alternating simulation or simply 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 large range of concurrency models. This is achieved by developing our study within the framework of open maps. We illustrate our results on transition systems throughout the paper and also show how they can be applied to timed transition systems.

START Conference Manager (V2.47.4)