Branching time controllers for discrete event systems

P. Madhusudan, P. S. Thiagarajan

Research output: Contribution to journalConference articlepeer-review


We study the problem of synthesizing controllers for discrete event systems in a branching time framework. We use a class of labelled transition systems to model both plants and specifications. We use first simulations and later bisimulations to capture the role of a controller; the controlled behaviour of the plant should be related via a simulation (bisimulation) to the specification. For both simulations and bisimulations we show that the problem of checking if a pair of finite transition systems - one modelling the plant and the other the specification - admits a controller is decidable in polynomial time. We also show that the size of the controller, if one exists, can be bounded by a polynomial in the sizes of the plant and the specification and can be effectively constructed in polynomial time. Finally, we prove that in the case of simulations, the problem of checking for the existence of a controller is undecidable in a natural concurrent setting.

Original languageEnglish (US)
Pages (from-to)117-149
Number of pages33
JournalTheoretical Computer Science
Issue number1-2
StatePublished - Mar 6 2002
Externally publishedYes
Event9th International Conference on Concurrency Theory 1998 CONCUR'98 - Nice, France
Duration: Sep 8 1998Sep 11 1998


  • Asynchronous transition systems
  • Bisimulations
  • Controller synthesis
  • Discrete-event systems
  • Simulations
  • Supervisor synthesis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Branching time controllers for discrete event systems'. Together they form a unique fingerprint.

Cite this