Advertisement

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.

Keywords

Regular Language Label Transition System Reachability Analysis Reachability Problem Message Sequence Chart 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 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. 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)CrossRefGoogle Scholar
  5. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 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)CrossRefGoogle Scholar
  8. 8.
    Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)Google Scholar
  9. 9.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007)zbMATHMathSciNetGoogle Scholar
  12. 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. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 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. 16.
    Kuske, D.: Regular sets of infinite message sequence charts. Information and Computation 187, 80–109 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 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)CrossRefGoogle Scholar
  18. 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. 19.
    Mayr, R.: Undecidable problems in unreliable computations. Theor. Comp. Science 297(1-3), 337–354 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus (1977)Google Scholar
  21. 21.
    Post, E.: Formal reductions of the combinatorial decision problem. American Journal of Mathematics 65(2), 197–215 (1943)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251–261 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Zielonka, W.: Asynchronous automata. In: Rozenberg, G., Diekert, V. (eds.) Book of Traces, pp. 175–217. World Scientific, Singapore (1995)Google Scholar
  24. 24.
    Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications 21, 99–135 (1987)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Anca Muscholl
    • 1
  1. 1.LaBRIUniversity BordeauxFrance

Personalised recommendations