Abstract
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.
Supported by SRC under contract 95-DC-324A.
Chapter PDF
References
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.
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.
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.
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.
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.
M.D. DiBenedetto, A. Saldanha, and A. Sangiovanni-Vincentelli. Strong model matching for finite state machines. In Proc. of Euorpean Control Conference, September 1995.
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.
J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, languages and Computation. Addison Wesley, 1979.
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.
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.
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.
J. Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68, 1989.
Amir Pneuli and Roni Rosner. On the synthesis of a reactive module. In Proc. Principles of Programming Languages, 1989.
M.O. Rabin. Automata on infinite trees an Church's problem, volume 13 of Regional Conference Series in Mathematics. American Mathematical Society, 1972.
P. Ramadge and W. Wonham. The control of discrete event systems. Proceedings of the IEEE, 77(1):81–98, January 1989.
Yosinori Watanabe. Logic Optimization of Interacting Components in Synchonous Digital System. PhD thesis, University of California, Berkeley, 1994. UCB/ERL Mem. No. M94/32.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aziz, A., Balarin, F., Brayton, R.K., DiBenedetto, M.D., Saldanha, A., Sangiovanni-Vincentelli, A.L. (1995). Supervisory control of finite state machines. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_57
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_57
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive