Programs with quasi-stable channels are effectively recognizable

Extended Abstract
  • Gérard Cécé
  • Alain Finkel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


We consider the analysis of infinite half-duplex systems which consists of finite state machines that communicate over unbounded channels. The property half-duplex for two machines and two channels (one in each direction) says that each reachable state has at least one channel empty.

The contributions of this paper are (a) to give a finite description of the reachability set of such systems, which happens to be effectively recognizable; this description allows us to solve classical verification problems such as: whether a given state is reachable, whether there exist deadlock states, whether the reachability set is finite and whether a specified action is useless; (b) to propose an extension of these results for a new class, systems with quasi-stable channels, which includes systems with similar behavior but which implies more than two machines.


Turing Machine Finite State Machine Reachable State Reachability Graph Reachability Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    P. Abdulla and B. Jonsson. Verifying Programs with Unreliable Channels. In Proc. 8 th Annual IEEE Symposium of Logic in Computer Science, 1993.Google Scholar
  2. 2.
    P. Abdulla and B. Jonsson. Undecidable Verification Problems for Programs with Unreliable Channels, in Proc. of ICALP, vol. 820 of LNCS pp.316–1994.Google Scholar
  3. 3.
    J. Berstel. Transductions and Context-Free Languages. B.G. Teubner Stuttgart, 1979.Google Scholar
  4. 4.
    B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs. In Proc. of 8 th CAV (August), USA LNCS 1102, pp. 1–12, 1996.Google Scholar
  5. 5.
    Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. JACM, 30(2):323–342, 1983.Google Scholar
  6. 6.
    G. Cécé, A. Finkel and S. Purushothaman Iyer. Unreliable Channels Are Easier to Verify Than Perfect Channels. In Information and Computation, vol. 124, No 1, 20–31, 1996Google Scholar
  7. 7.
    G. Cécé and A. Finkel Programs with Quasi-Stable Channels are Effectively Recognizable. Technical Report, LSV, ENS de Cachan, 1997 (available via the authors) grenadeGoogle Scholar
  8. 8.
    A. Finkel. Reduction and covering of Infinite Reachability Trees. Information and Computation, vol. 89, nℴ 2, pp. 144–170, 1990.Google Scholar
  9. 9.
    A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7:129–135, 1994.Google Scholar
  10. 10.
    A. Finkel and P. McKenzie. Verifying identical communicating Processes is undecidable. to appear in TCS 1997Google Scholar
  11. 11.
    M. G. Gouda, E. G. Manning and Y. T. Yu. On the Progress of Communication between Two Finite State Machines. Information and Control, 63:217–225, 1984.Google Scholar
  12. 12.
    T. Jéron and C. Jard. Testing for unboundedness of fifo channels. Theoretical Computer Science 113, pp. 93–117, 1993.Google Scholar
  13. 13.
    J. K. Pachl. Reachability Problems for Communicating Finite State Machines Research Report CS-82-12, University of Waterloo, Dpt. of Computer Science, 1982.Google Scholar
  14. 14.
    J. K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Proc. of Protocol Specification, Testing and Verification, VII, May 1987.Google Scholar
  15. 15.
    Kenneth J. Turner. Using Formal Description Techniques; an introduction to Estelle, Lotos and SDL. ©John Wiley & Son Ltd., 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Gérard Cécé
    • 1
  • Alain Finkel
    • 2
  1. 1.LSVCNRS URA 2236Cachan CedexFrance
  2. 2.ENS de CachanCachan CedexFrance

Personalised recommendations