Abstract
In this paper, we consider networks of communicating finite state machines (CFSM's), that explicitly allow zero testing (i.e. empty channel detection). In our main result, we show that the boundedness problem is decidable for the class of FIFO networks consisting of two such CFSM's, where one of the two machines is allowed to send only a single type of message to the other. This result, we feel, is somewhat surprising since the zero testing capability is precisely the required extension needed in order to render the problem undecidable for the related class of vector addition systems with states (VASS's) of dimension two. Note that both have the ability to store two nonnegative integers which can be conditionally tested for zero. The reason for the disparity appears to be that such a class of extended VASS's would be capable of more synchronized behavior (since the actions of the two counters can be controlled by a single finite state control). The rest of the paper examines other classes of networks which allow empty channel detection. These results seem to indicate that our main result can not be extended.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
5. References
Agerwala, T. and Flynn, M., Comments on Capabilities, Limitations, and ‘Correctness’ of Petri Nets, Proceedings of the First Annual Symposium on Computer Architectures, New York: ACM, 1973, pp. 81–86.
Berthelot, G. and Terrat, R., Petri Net Theory for the Correctness of Protocols, IEEE Trans. on Comm., Vol. COM-30, No. 12, December 1982, pp. 2497–2505.
Bochmann, G., Finite State Description of Communication Protocols, Computer Networks, Vol. 2, 1978, pp.361–371.
Brand, D. and Zafiropulo, P., On Communicating Finite-State Machines, J. ACM, Vol. 30, No. 2, April 1983, pp. 323–342.
Cook, S., Characterizations of Pushdown Machines in Terms of Time Bounded Computers, J. ACM, Vol. 18, 1971, pp. 4–18.
Cunha, P. and Maibaum, T., A Synchronization Calculus for Message-Oriented Programming, Proc. 2nd International Conf. on Distributed Computing Systems, April 1981, pp. 433–445.
Gouda, M. and Rosier, L., Priority Networks of Communicating Finite State Machines, accepted for publication in the SIAM Journal on Computing.
Hack, M., Decidability Questions for Petri Nets, Ph.D. dissertation, Department of Electrical Engineering, MIT, 1975.
Hopcroft, J. and Pansiot, J. On the Reachability Problem for 5-Dimensional Vector Addition Systems, Theor. Computer Science, Vol. 8, 1979, pp. 135–159.
Hopcroft, J. and Ullman, J., "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, Reading, Mass., 1979.
Jones, N., Lien, Y. and Laaser, W., New Problems Complete for Nondeterministic Logspace, Math. Systems Theory, Vol. 10, 1976, pp. 1–17.
Karp, R. and Miller, R., Parallel Program Schemata, J. of Computer and System Sciences, Vol. 3, No.2, 1969, pp.147–195.
Kosaraju, S., Limitations of Dijkstra's Semaphore Primitives and Petri Nets, Operating Systems Review, Vol. 7, No. 4, Oct. 1973, pp. 122–126.
Minsky, M., "Computation: Finite and Infinite Machines", Prentice Hall, Englewood Cliffs, NJ, 1967.
Parnas, D., On a Solution to the Cigarette Smokers' Problem (Without Conditional Statements), Communications of the ACM, Vol. 18, No. 3, March 1975, pp. 181–183.
Patil, S., Limitations and Capabilities of Dijkstra's Semaphore Primitives for Coordination Among Processes, Group Memo 57, Project MAC, MIT, February 1971, 18 pages.
Peterson, J., "Petri Net Theory and the Modeling of Systems", Prentice Hall, Englewood Cliffs, NJ, 1981.
Rackoff, C., The Covering and Boundedness Problems for Vector Addition Systems, Theor. Comput. Sci., Vol. 6, 1978, pp. 223–231.
Rosier, L. and Gouda, M., On Deciding Progress for a Class of Communication Protocols, in the Proceedings of the Eighteen Annual Conference on Information Sciences and Systems, Princeton Univ., 1984.
Raeuchle, T. and Toueg, S., Exposure to Deadlock for Communicating Processes is Hard to Detect, Tech. Rep. No. 83-555, Cornell University, Department of Computer Science.
Savitch, W., Relationships between Nondeterministic and Deterministic Tape Complexities, J. of Computer and System Sciences, Vol. 4, No. 2, 1970, pp. 177–192.
Sudborough, I., On Tape-Bounded Complexity Classes and Multihead Finite Automata, J. Computer and Systems Sciences, Vol. 10, No. 1, 1975, pp. 62–76.
Sunshine, C., Formal Modeling of Communication Protocols, USC/Inform. Sc. Institute, Research Report 81–89, March 1981.
Tannenbaum, A., "Computer Networks", Prentice Hall, Englewood Cliffs, NJ, 1981.
Valiant, L. and Paterson, M., Deterministic One-Counter Automata, J. of Computer and System Sciences, Vol. 10, 1975, pp. 340–350.
Yu. Y. and Gouda, M., Unboundedness Detection for a Class of Communicating Finite State Machines, Information Processing Letters, 17, December 1983, pp. 235–240.
Zafiropulo, P., et. al., Towards Analyzing and Synthesizing Protocols, IEEE Trans. on Comm., Vol. COM-28, No. 4, April 1980, pp. 651–661.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rosier, L.E., Yen, HC. (1984). Boundedness, empty channel detection and synchronization for communicating finite state machines. In: Mehlhorn, K. (eds) STACS 85. STACS 1985. Lecture Notes in Computer Science, vol 182. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024017
Download citation
DOI: https://doi.org/10.1007/BFb0024017
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-13912-6
Online ISBN: 978-3-540-39136-4
eBook Packages: Springer Book Archive