Skip to main content
SpringerLink
Log in

Deciding boundedness for systems of two linear communicating finite state machines

  • Foundations of CAST: Theory and Methodology
  • Conference paper
  • First Online:
Computer Aided Systems Theory — CAST '94

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1105))

  • 179 Accesses

Abstract

Since 1981, we know that the unboundedness is an undecidable problem for systems of finite state machines that communicate exclusively by exchanging messages over unidirectional, FIFO channels. This led some authors to reduce the general model in order to find restricted classes in where the problem becomes decidable. In this paper, we present a new class of systems constituted of two linear Communicating finite state machines. A linear machine is a directed graph where each strongly connected component is reduced to an elementary circuit. We show for this class that the boundedness problem is decidable. Consequently, the decision procedures can be automatized and integrated into the frame of Computer-Aided Systems Technology. Examples will be used to illustrate our purpose.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Benslimane “Contribution à la Validation des Protocoles: réduction de l'espace d'états et décidabilité du caractère borné” Ph.D thesis of Franche-Comté University, (1993).

    Google Scholar 

  2. A.Benslimane “Deciding Boundedness for systems of two communicating finite state machines” HPDC-3 Third IEEE International symposium on High Performance of Distributed Computing, San Francisco California, IEEE Computer Society Press, (2–5 August 1994), pp. 262–269.

    Google Scholar 

  3. G.V. Bochmann “Finite State Description of Communication Protocols” Computer Networks, N∘2, (1978), pp. 361–372.

    Google Scholar 

  4. D. Brand and P. Zafiropulo “On Communicating Finite-State Machines” Tech. Rep. RZ 1053. IBM Zurich Research Lab., Ruschlikon, Switzerland, (January 1981).

    Google Scholar 

  5. A. Choquet and A. Finkel “ Simulation of Linear Fifo Nets by Petri Nets having a Structured Set of Terminal Markings” Proc. of the 8th European Workshop on Applications and Theory of Petri Nets, Zaragoza, Spain, (June 1987).

    Google Scholar 

  6. A.S. Danthine “Protocol Representation with Finite State Models”, IEEE Trans. on Commun., Vol. COM-28, N∘ 4, (April 1980), pp. 632–642.

    Google Scholar 

  7. A. Finkel “Structuration des Systèmes de Transitions: Applications au Contrôle de Parallélisme par Files Fifo” Thèse d'état L.R.I. Orsay, (Juin 1986).

    Google Scholar 

  8. A. Finkel “A new Class of Analysable CFSMS with Unbounded Fifo Channels” Protocol Specification, Testing, and Verification, VIII, S. Aggarwal and K. Sabnani (ed.) North-Holland Publishing Compagny IFIP, (1988), pp. 283–294.

    Google Scholar 

  9. M.G. Gouda and Y.T. Yu “Synthesis of Communicating Finite State Machines with Guaranteed Progress” IEEE Trans. on Commun., Vol. COM-32, N∘ 7, (July 1984), pp. 779–787.

    Google Scholar 

  10. M.G. Gouda, E.M. Gurari, T.H. Lai and L.E. Rosier “On Deadlock Detection in Systems of Communicating Finite State Machines” Computer and Artificial Intelligence, Vol. 6, N∘ 3, (1987), pp. 209–228.

    Google Scholar 

  11. T. Jéron “Contribution à la Validation des Protocoles: test d' infinitude et vérification à la vollé” Ph.D thesis of Rennes University, (1991).

    Google Scholar 

  12. J. Pachl “Protocol description and analysis based on a state transition model with channel expression” Protocol Specification, Testing, and Verification, VI, B. Sarikaya and G.V. Bochmann (ed.), North-Holland Publishing Compagny IFIP, (1987), pp. 243–254.

    Google Scholar 

  13. W. Peng and S. Purushothaman “A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State Machines” Workshop on Computer Aided Verification DIMACS 90, (June 1990), pp. 242–252.

    Google Scholar 

  14. R. Razouk and G. Estrin “modeling and Verification of Communication Protocols in SARA: The X.21 Interface” IEEE Trans. on Comp. C-29, 12, (Dec. 1980), pp. 1052–1083.

    Google Scholar 

  15. L.E. Rosier and M. Gouda “On deciding progress for a class of communicatng protocols” Proc. of the 8th Ann. Conf. on Inf. Sci. and Syst., Princeton Univ., (1984), pp. 663–667.

    Google Scholar 

  16. C.A. Sunshine “Formal Modeling of Communication Protocols” Computer Networks and Simulation II, S. Schoemaker (ed.), North-Holland Publishing Compagny, (1982), pp. 53–75.

    Google Scholar 

  17. C.H. West “Application and Limitations of Automated Protocol Validation” Protocol Specification, Testing, and Verification, C.Sunshine (ed.) North-Holland Publishing Compagny IFIP, (1982), pp. 361–371.

    Google Scholar 

  18. Y.T. Yu and M.G. Gouda “Deadlock Detection for a Class of Communicating Finite State Machines” IEEE Trans. on Commun., Vol. COM-30, N∘ 12, (December 1982), pp. 2514–2518.

    Google Scholar 

  19. P. Zafiropulo, C.H. West, H.Rudin, D.D. Cowan and D.Brand “Towards Analyzing and Synthesizing Protocols” IEEE Trans. Commun., Vol. COM-28, N∘ 4, (April 1980), pp. 651–661.

    Google Scholar 

  20. J. Zhao and G.V. Bochmann “Reduced Reachability Analysis of Communication Protocols: A new approach” Protocol Specification, Testing, and Verification, VI, B. Sarikaya and G.V. Bochmann (ed.), North-Holland Publishing Compagny IFIP, (1987), pp. 243–254.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d'Informatique, Institut Polytechnique de Sévenans, 90010, Belfort cedex, France

    Abderrahim Benslimane

Authors
  1. Abderrahim Benslimane
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

George J. Klir Tuncer I. Ören

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benslimane, A. (1996). Deciding boundedness for systems of two linear communicating finite state machines. In: Klir, G.J., Ören, T.I. (eds) Computer Aided Systems Theory — CAST '94. Lecture Notes in Computer Science, vol 1105. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61478-8_71

Download citation

  • DOI: https://doi.org/10.1007/3-540-61478-8_71

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61478-4

  • Online ISBN: 978-3-540-68600-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation