Supervisory control of finite state machines

  • A. Aziz
  • F. Balarin
  • R. K. Brayton
  • M. D. DiBenedetto
  • A. Saldanha
  • A. L. Sangiovanni-Vincentelli
Session 8: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


We address a problem of finding a finite state machine (FSM), which composed with a given FSM, satisfies a given specification. The composition we use is the standard synchronous automata composition restricted to cases which correctly model hardware interconnection. For the satisfaction relation, we use language containment. We present a procedure that will generate a solution (if one exists) which is maximal, i.e. contains behaviors of all other solutions.


Finite State Machine Regular Language Supervisory Control Maximal Solution Discrete Event System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Adnan Aziz and Robert K. Brayton. Synthesizing interacting finite state machines. Technical Report UCB/ERL M94/96, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, December 1994.Google Scholar
  2. 2.
    S. Balemi, G. Hoffmann, P. Gyugyi, H. Wong-Toi, and G. Franklin. Supervisory control of a rapid thermal multiprocessor. IEEE Transactions on Automatic Control, 38(7):1040–1059, July 1993.Google Scholar
  3. 3.
    J. Richard Buchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311, April 1969.Google Scholar
  4. 4.
    J.R. Burch, D.L. Dill, E. Wolf, and G. DeMicheli. Modeling hierarcical combinational circuits. In Digest of Technical Papers of the 1993 IEEE International Conference on CAD, pages 612–617, November 1993.Google Scholar
  5. 5.
    M.D. DiBenedetto, A. Saldanha, and A. Sangiovanni-Vincentelli. Model matching for finite state machines. In Proceedings of the IEEE Conference on Decision and Control, December 1994.Google Scholar
  6. 6.
    M.D. DiBenedetto, A. Saldanha, and A. Sangiovanni-Vincentelli. Strong model matching for finite state machines. In Proc. of Euorpean Control Conference, September 1995.Google Scholar
  7. 7.
    C.H. Golaszewski and R.P. Kurshan. Task-driven supervisory control of discrete event systems. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of the Workshop on Computer-Aided Verification, volume 531 of LNCS, pages 282–291. Springer-Verlag, June 1990.Google Scholar
  8. 8.
    J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, languages and Computation. Addison Wesley, 1979.Google Scholar
  9. 9.
    O.H. Jensen, J.T. Lang, C. Jeppesen, and K.G. Larsen. Model construction for implicit specifications in modal logic. Lecture Notes in Computer Science, 715, 1993.Google Scholar
  10. 10.
    B. Jonsson and K.G. Larsen. On the complexity of equation solving in process algebra. Lecture Notes in Computer Science, 493, 1991. In Proceedings of TAPSOET'91.Google Scholar
  11. 11.
    T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli. A fully implicit algorithm for exact state minimization. In Proceedings of the 31th ACM/IEEE Design Automation Conference, pages 684–690, June 1994.Google Scholar
  12. 12.
    J. Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68, 1989.Google Scholar
  13. 13.
    Amir Pneuli and Roni Rosner. On the synthesis of a reactive module. In Proc. Principles of Programming Languages, 1989.Google Scholar
  14. 14.
    M.O. Rabin. Automata on infinite trees an Church's problem, volume 13 of Regional Conference Series in Mathematics. American Mathematical Society, 1972.Google Scholar
  15. 15.
    P. Ramadge and W. Wonham. The control of discrete event systems. Proceedings of the IEEE, 77(1):81–98, January 1989.Google Scholar
  16. 16.
    Yosinori Watanabe. Logic Optimization of Interacting Components in Synchonous Digital System. PhD thesis, University of California, Berkeley, 1994. UCB/ERL Mem. No. M94/32.Google Scholar
  17. 17.
    H. Wong-Toi and D.L. Dill. Synthesizing processes and schedulers from temporal specifications. In Edmund M. Clarke and Robert P. Kurshan, editors, Proceedings of the Workshop on Computer-Aided Verification, volume 531 of LNCS, pages 272–281. Springer-Verlag, June 1990.Google Scholar
  18. 18.
    W. Wonham and P. Ramadge. On the supremal controllable sublanguage of a given language. SIAM Journal of Control and Optimization, 25(3):637–659, May 1987.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • A. Aziz
    • 1
  • F. Balarin
    • 2
  • R. K. Brayton
    • 1
  • M. D. DiBenedetto
    • 3
  • A. Saldanha
    • 2
  • A. L. Sangiovanni-Vincentelli
    • 1
  1. 1.Dept. of EECSUniversity of CaliforniaBerkeleyUSA
  2. 2.Cadence Berkeley LaboratoriesBerkeleyUSA
  3. 3.Dpt. di Informatica e SistemisticaUniversitá di Roma “La Sapienza”RomeItaly

Personalised recommendations