Skip to main content

Analysis of Communicating Automata

  • Conference paper
Language and Automata Theory and Applications (LATA 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6031))

Abstract

This extended abstract is a survey of some of the recent developments in the area of automated verification dedicated to the analysis of communicating automata.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite state systems. In: LICS’96, pp. 313–323 (1996)

    Google Scholar 

  2. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  3. Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 1–12. Springer, Heidelberg (1996)

    Google Scholar 

  4. Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 172–186. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  5. Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theor. Comp. Science 221(1-2), 211–250 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  6. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  7. Chambart, P., Schnoebelen, P.: Mixing lossy and perfect fifo channels. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 340–355. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)

    Google Scholar 

  9. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  10. Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Information and Computation 204(6), 920–956 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  11. Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007)

    MATH  MathSciNet  Google Scholar 

  12. Genest, B., Muscholl, A., Peled, D.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 537–558. Springer, Heidelberg (2004)

    Google Scholar 

  13. Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state high-level MSCs: Model-checking and realizability. J. Comput. Syst. Sci. 72(4), 617–647 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  14. Henriksen, J.G., Mukund, M., Kumar, K.N., Sohoni, M., Thiagarajan, P.: A theory of regular MSC languages. Information and Computation 202(1), 1–38 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  15. Heußner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 267–281. Springer, Heidelberg (2010)

    Google Scholar 

  16. Kuske, D.: Regular sets of infinite message sequence charts. Information and Computation 187, 80–109 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  17. La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 299–314. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Manna, Z., Pnueli, A.: Verification of the concurrent programs: the temporal framework. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Science, pp. 215–273. Academic Press, London (1981)

    Google Scholar 

  19. Mayr, R.: Undecidable problems in unreliable computations. Theor. Comp. Science 297(1-3), 337–354 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  20. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus (1977)

    Google Scholar 

  21. Post, E.: Formal reductions of the combinatorial decision problem. American Journal of Mathematics 65(2), 197–215 (1943)

    Article  MATH  MathSciNet  Google Scholar 

  22. Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251–261 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  23. Zielonka, W.: Asynchronous automata. In: Rozenberg, G., Diekert, V. (eds.) Book of Traces, pp. 175–217. World Scientific, Singapore (1995)

    Google Scholar 

  24. Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications 21, 99–135 (1987)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Muscholl, A. (2010). Analysis of Communicating Automata. In: Dediu, AH., Fernau, H., Martín-Vide, C. (eds) Language and Automata Theory and Applications. LATA 2010. Lecture Notes in Computer Science, vol 6031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13089-2_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13089-2_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13088-5

  • Online ISBN: 978-3-642-13089-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics