# Boundedness, empty channel detection and synchronization for communicating finite state machines

## 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.

## Preview

Unable to display preview. Download preview PDF.

## 5. References

- [1]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.Google Scholar - [2]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.Google Scholar - [3]Bochmann, G., Finite State Description of Communication Protocols,
*Computer Networks*, Vol. 2, 1978, pp.361–371.Google Scholar - [4]Brand, D. and Zafiropulo, P., On Communicating Finite-State Machines,
*J. ACM*, Vol. 30, No. 2, April 1983, pp. 323–342.Google Scholar - [5]Cook, S., Characterizations of Pushdown Machines in Terms of Time Bounded Computers,
*J. ACM*, Vol. 18, 1971, pp. 4–18.Google Scholar - [6]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.Google Scholar - [7]Gouda, M. and Rosier, L., Priority Networks of Communicating Finite State Machines, accepted for publication in the
*SIAM Journal on Computing*.Google Scholar - [8]Hack, M., Decidability Questions for Petri Nets, Ph.D. dissertation, Department of Electrical Engineering, MIT, 1975.Google Scholar
- [9]Hopcroft, J. and Pansiot, J. On the Reachability Problem for 5-Dimensional Vector Addition Systems,
*Theor. Computer Science*, Vol. 8, 1979, pp. 135–159.Google Scholar - [10]Hopcroft, J. and Ullman, J., "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, Reading, Mass., 1979.Google Scholar
- [11]Jones, N., Lien, Y. and Laaser, W., New Problems Complete for Nondeterministic Logspace,
*Math. Systems Theory*, Vol. 10, 1976, pp. 1–17.Google Scholar - [12]Karp, R. and Miller, R., Parallel Program Schemata,
*J. of Computer and System Sciences*, Vol. 3, No.2, 1969, pp.147–195.Google Scholar - [13]Kosaraju, S., Limitations of Dijkstra's Semaphore Primitives and Petri Nets,
*Operating Systems Review*, Vol. 7, No. 4, Oct. 1973, pp. 122–126.Google Scholar - [14]Minsky, M., "Computation: Finite and Infinite Machines", Prentice Hall, Englewood Cliffs, NJ, 1967.Google Scholar
- [15]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.Google Scholar - [16]Patil, S., Limitations and Capabilities of Dijkstra's Semaphore Primitives for Coordination Among Processes, Group Memo 57, Project MAC, MIT, February 1971, 18 pages.Google Scholar
- [17]Peterson, J., "Petri Net Theory and the Modeling of Systems", Prentice Hall, Englewood Cliffs, NJ, 1981.Google Scholar
- [18]Rackoff, C., The Covering and Boundedness Problems for Vector Addition Systems,
*Theor. Comput. Sci.*, Vol. 6, 1978, pp. 223–231.Google Scholar - [19]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.Google Scholar - [20]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.Google Scholar
- [21]Savitch, W., Relationships between Nondeterministic and Deterministic Tape Complexities,
*J. of Computer and System Sciences*, Vol. 4, No. 2, 1970, pp. 177–192.Google Scholar - [22]Sudborough, I., On Tape-Bounded Complexity Classes and Multihead Finite Automata,
*J. Computer and Systems Sciences*, Vol. 10, No. 1, 1975, pp. 62–76.Google Scholar - [23]Sunshine, C., Formal Modeling of Communication Protocols, USC/Inform. Sc. Institute, Research Report 81–89, March 1981.Google Scholar
- [24]Tannenbaum, A., "Computer Networks", Prentice Hall, Englewood Cliffs, NJ, 1981.Google Scholar
- [25]Valiant, L. and Paterson, M., Deterministic One-Counter Automata,
*J. of Computer and System Sciences*, Vol. 10, 1975, pp. 340–350.Google Scholar - [26]Yu. Y. and Gouda, M., Unboundedness Detection for a Class of Communicating Finite State Machines,
*Information Processing Letters*, 17, December 1983, pp. 235–240.Google Scholar - [27]Zafiropulo, P., et. al., Towards Analyzing and Synthesizing Protocols,
*IEEE Trans. on Comm.*, Vol. COM-28, No. 4, April 1980, pp. 651–661.Google Scholar