×

Compositionally progressive solutions of synchronous FSM equations. (English) Zbl 1161.93322

Summary: The paper addresses the problem of designing a component that combined with a known part of a system, called the context FSM, is a reduction of a given specification FSM. We study compositionally progressive solutions of synchronous FSM equations. Such solutions, when combined with the context, do not block any input that may occur in the specification, so they are of practical use. We show that, if a synchronous FSM equation has a compositionally progressive solution, then there is a largest regular compositionally progressive solution including all of them. We provide two different algorithms to compute a largest regular compositionally progressive solution: one deletes all compositionally non-progressive strings from a largest solution, the other splits states of a largest solution and then removes those inducing a non-progressive composition.

MSC:

93C65 Discrete event control/observation systems
93C83 Control/observation systems involving computers (process control, etc.)
93B50 Synthesis problems

Software:

UMDES
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barrett G, Lafortune S (1998) Bisimulation, the supervisory control problem and strong model matching for finite state machines. Discret Event Dyn Syst: Theory Appl 8(4):377–429 · Zbl 0919.93005 · doi:10.1023/A:1008301317459
[2] Bochmann GV (2002) Submodule construction and supervisory control: a generalization. In: Watson BW, Wood D (eds) Proceedings of the 6th International Conference on Implementation and Application of Automata (CIAA ’01), vol 2494 of Lecture Notes in Computer Science. Springer, pp 27–39 · Zbl 1015.68115
[3] Buffalov S, El-Fakih K, Yevtushenko N, Bochmann G v (2003) Progressive solutions to a parallel automata equation. In: Proceedings of the IFIP 23rd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2003), vol 2767 of LNCS. Springer, pp 367–382, September · Zbl 1279.68135
[4] Cassandras CC, Lafortune S (1999) Introduction to discrete event systems. Kluwer · Zbl 0934.93001
[5] El-Fakih K, Buffalov S, Yevtushenko N, Bochmann GV (2006) Progressive solutions to a parallel automata equation. Theor Comp Sci 362:17–32 · Zbl 1100.68047 · doi:10.1016/j.tcs.2006.05.034
[6] Holloway LE, Grogh BH, Giua, A (1997) A survey of Petri net methods for controlled discrete event systems. Discret Event Dyn Syst: Theory Appl 7(2):151–190 · Zbl 0968.93053 · doi:10.1023/A:1008271916548
[7] Hopcroft JE, Motwani R, Ullman JD (2001) Introduction to automata theory, languages, and computation. Addison-Wesley · Zbl 0980.68066
[8] Kumar R, Nelvagal S, Marcus SI (1997) A discrete event systems approach for protocol conversion. Discret Event Dyn Syst: Theory Appl 7(3):295–315 · Zbl 0960.93034 · doi:10.1023/A:1008258331497
[9] Mishchenko A, Brayton R, Jiang J-H, Villa T, Yevtushenko N (2005) Efficient solution of language equations using partitioned representations. In: The Proceedings of the Design, Automation and Test in Europe Conference, vol 01. pp 418–423, March
[10] Moisan S, Ressouche A, Rigault, J-P (2003) Behavioral substitutability in component frameworks: a formal approach. In: Specification and Verification of Component-Based Systems Workshop at ESEC/FSE 2003, September 1–2,2003. Technical Report #03-11, Department of Computer Science, Iowa State University, pp 22–28, September
[11] Ramadge P, Wonham W (1989) The control of discrete event systems. Proc IEEE 77(1):81–98 · doi:10.1109/5.21072
[12] Sewell P, Vitek J (2003) Secure composition of untrusted code: box {\(\pi\)}, wrappers, and causality types. J Comput Secur 11(2):135–187,
[13] Starke PH (1972) Abstract automata. North-Holland
[14] Vetrova M (2004) Designing and testing FSM compensators. PhD thesis, Tomsk State University, Russia (in Russian)
[15] Villa T, Yevtushenko N, Zharikova S (2003) Characterization of progressive solutions of a synchronous FSM equation. In: Vestnik, 278, series physics. pp 129–133, September (in Russian)
[16] Yevtushenko N, Villa T, Brayton R, Petrenko A, Sangiovanni-Vincentelli A (2000) Sequential synthesis by language equation solving. In: International Workshop on Logic Synthesis, June
[17] Yevtushenko N, Villa T, Brayton R, Petrenko A, Sangiovanni-Vincentelli A (2002) Solution of synchronous language equations for logic synthesis. In: The Biannual 4th Russian Conference with Foreign Participation on Computer-Aided Technologies in Applied Mathematics, September, http://www.parades.rm.cnr.it/villa/articoli/ps/tomsk2002.ps · Zbl 1161.93322
[18] Yevtushenko N, Villa T, Brayton R, Petrenko A, Sangiovanni-Vincentelli A (2003) Sequential synthesis by language equation solving. Technical report, Tech. Rep. No. UCB/ERL M03/9, Berkeley, CA, April, http://www.parades.rm.cnr.it/villa/articoli/ps/TR-UCB_ERL-M03_9.ps
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.