Discrete Event Dynamic Systems

, Volume 17, Issue 2, pp 211–232 | Cite as

Modal Specifications for the Control Theory of Discrete Event Systems

  • Guillaume Feuillade
  • Sophie Pinchinat


We propose a logical framework for the control theory of reactive systems modeled by discrete event systems. The logic is the conjunctive nu-calculus, an expressive fragment of the powerful mu-calculus. Conjunctive nu-calculus possesses an alternative presentation based on modal specifications, with simple graphical representations. We exploit modal specification to specify and to solve the basic centralized control problem: our class of control objectives strictly subsumes the class of regular languages, normally used in the classic control theory of discrete-event systems, but the existence of maximally permissive solutions is however preserved.


Reactive systems Control theory Logics Mu-calculus Conjunctive nu-calculus Modal specifications Maximally permissive solutions 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Arnold A, Niwinski D (2001) Rudiments of Mu-calculus. North-HollandGoogle Scholar
  2. Arnold A, Vincent A, Walukiewicz I (2003) Games for synthesis of controllers with partial observation, Theoretical Computer Science. 303(1): 7–34. JuneMATHCrossRefMathSciNetGoogle Scholar
  3. Briand X (2006) Sur la décidabilité de certains problèmes de synthèse de contrôleursm, Ph.D. Thesis, Université de Bordeaux I, JuneGoogle Scholar
  4. Cassandras CG, Lafortune S (1999) Introduction to discrete event systems. Boston, MA:KluwerMATHGoogle Scholar
  5. Gohari P, Murray Wonham W (2000) On the complexity of supervisory control design in the RW framework. IEEE Transactions on Systems, Man, and Cybernetics, Part B, 30(5):643–652CrossRefGoogle Scholar
  6. Harel D, Pnueli A (1984) On the development of reactive systems. In: Krzysztof R. Apt (ed) logic and model of concurrent systems, NATO ASI, Volume 13. Springer Berlin Heidelberg New York, pp 477–498, OctoberGoogle Scholar
  7. Jiang S, Kumar R (2005) Supervisory control of discrete event systems with ctl* temporal logic specifications. SIAM Journal on Control and Optimization 44(6), JanuaryGoogle Scholar
  8. Kumar R, Garg VK (1995) Modeling and Control of Logical Discrete Event Systems. Kluwer, Boston, MAMATHGoogle Scholar
  9. Kozen D (1983) Results on the propositional Mu-calculus. Theoretical Computer Science 27: 333–354MATHCrossRefMathSciNetGoogle Scholar
  10. Larsen KG (1989) Modal specifications. In: Proc. workshop automatic verification methods for finite state systems, Grenoble, LNCS 407. Springer, Berlin Heidelberg New York, pp. 232–246, JuneGoogle Scholar
  11. Pinchinat S, Riedweg S (2005) A decidable class of problems for control under partial observation. Information Processing Letters 95(4): 454–460CrossRefMathSciNetGoogle Scholar
  12. Riedweg S, Pinchinat S (2003) Quantified Mu-calculus for control synthesis. In: Mathematical foundations of computer science, Bratislava. Slovak Republic, AugustGoogle Scholar
  13. Riedweg S, Pinchinat S (2004) Maximally permissive controllers in all contexts. In: Workshop on discrete event systems, Reims, France, SeptemberGoogle Scholar
  14. Raclet JB, Pinchinat S (2005) The control of non-deterministic systems: a logical approach. In: Pavel Piztek, editor, Proceedings of the 16th IFAC Word Congress, Prague, Czech Republic, Elsevier, Amsterdam, JulyGoogle Scholar
  15. Ramadge PJG, Wonham WM (1989) The control of discrete event systems, Proceedings of the IEEE, 77: 81–98CrossRefGoogle Scholar
  16. Tabuada P, Pappas GJ (2003) Model checking ltl over controllable linear systems is decidable. In: O. Maler, A. Pnueli (eds.), HSCC, Lecture Notes in Computer Science, Volume 2623. Springer, Berlin Heidelberg New York, pp 498–513Google Scholar
  17. Wonham WM (1989) On the control of discrete-event systems. Springer New York, Inc, New York, NY, USAGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2007

Authors and Affiliations

  1. 1.IRIT-Univ. Paul SabatierToulouse Cedex 9France
  2. 2.IRISACampus de BeaulieuRennesFrance

Personalised recommendations