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

  • Louis E. Rosier
  • Hsu-Chun Yen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 182)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

5. References

  1. [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. [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. [3]
    Bochmann, G., Finite State Description of Communication Protocols, Computer Networks, Vol. 2, 1978, pp.361–371.Google Scholar
  4. [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. [5]
    Cook, S., Characterizations of Pushdown Machines in Terms of Time Bounded Computers, J. ACM, Vol. 18, 1971, pp. 4–18.Google Scholar
  6. [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. [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. [8]
    Hack, M., Decidability Questions for Petri Nets, Ph.D. dissertation, Department of Electrical Engineering, MIT, 1975.Google Scholar
  9. [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. [10]
    Hopcroft, J. and Ullman, J., "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, Reading, Mass., 1979.Google Scholar
  11. [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. [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. [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. [14]
    Minsky, M., "Computation: Finite and Infinite Machines", Prentice Hall, Englewood Cliffs, NJ, 1967.Google Scholar
  15. [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. [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. [17]
    Peterson, J., "Petri Net Theory and the Modeling of Systems", Prentice Hall, Englewood Cliffs, NJ, 1981.Google Scholar
  18. [18]
    Rackoff, C., The Covering and Boundedness Problems for Vector Addition Systems, Theor. Comput. Sci., Vol. 6, 1978, pp. 223–231.Google Scholar
  19. [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. [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. [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. [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. [23]
    Sunshine, C., Formal Modeling of Communication Protocols, USC/Inform. Sc. Institute, Research Report 81–89, March 1981.Google Scholar
  24. [24]
    Tannenbaum, A., "Computer Networks", Prentice Hall, Englewood Cliffs, NJ, 1981.Google Scholar
  25. [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. [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. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Louis E. Rosier
    • 1
  • Hsu-Chun Yen
    • 1
  1. 1.Department of Computer SciencesUniversity of Texas at AustinAustin

Personalised recommendations