Advertisement

Realizability of Concurrent Recursive Programs

  • Benedikt Bollig
  • Manuela-Lidia Grindei
  • Peter Habermehl
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)

Abstract

We define and study an automata model of concurrent recursive programs. An automaton consists of a finite number of pushdown systems running in parallel and communicating via shared actions. Actually, we combine multi-stack visibly pushdown automata and Zielonka’s asynchronous automata towards a model with an undecidable emptiness problem. However, a reasonable restriction allows us to lift Zielonka’s Theorem to this recursive setting and permits a logical characterization in terms of a suitable monadic second-order logic. Building on results from Mazurkiewicz trace theory and work by La Torre, Madhusudan, and Parlato, we thus develop a framework for the specification, synthesis, and verification of concurrent recursive processes.

Keywords

Model Check Context Switch Trace Theory Logical Characterization Recursive Setting 
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.

References

  1. 1.
    Alur, R., Arenas, M., Barceló, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Logical Methods in Computer Science 4(4:11), 1–44 (2008)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC 2004, pp. 202–211. ACM Press, New York (2004)Google Scholar
  3. 3.
    Alur, R., Madhusudan, P.: Adding nesting structure to words. In: H. Ibarra, O., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1–13. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Baudru, N., Morin, R.: Unfolding synthesis of asynchronous automata. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 46–57. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Bollig, B.: On the expressive power of 2-stack visibly pushdown automata. Logical Methods in Computer Science 4(4:16), 1–35 (2008)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. International Journal on Foundations of Computer Science 14(4), 551–582 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Castellani, I., Mukund, M., Thiagarajan, P.S.: Synthesizing distributed transition systems from global specifications. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 219–231. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Ştefănescu, A., Esparza, J., Muscholl, A.: Synthesis of distributed algorithms using asynchronous automata. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 27–41. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences 64(2), 396–418 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)Google Scholar
  11. 11.
    Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266 (1982)CrossRefzbMATHGoogle Scholar
  12. 12.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Genest, B., Muscholl, A.: Constructing Exponential-Size Deterministic Zielonka Automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 565–576. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Henriksen, J.G., Mukund, M., Narayan Kumar, K., Sohoni, M., Thiagarajan, P.S.: A theory of regular MSC languages. Information and Computation 202(1), 1–38 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Kuske, D.: Weighted asynchronous cellular automata. Theoretical Computer Science 374(1-3), 127–148 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007, pp. 161–170. IEEE Computer Society Press, Los Alamitos (2007)Google 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.
    Morin, R.: Decompositions of asynchronous systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 549–564. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  19. 19.
    Muscholl, A., Peled, D.: Message sequence graphs and decision problems on Mazurkiewicz traces. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 81–91. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  20. 20.
    Ochmański, E.: Regular behaviour of concurrent systems. Bulletin of the European Association for Theoretical Computer Science (EATCS) 27, 56–67 (1985)Google Scholar
  21. 21.
    Peled, D., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages. Theoretical Computer Science 195(2), 183–203 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Prog. Lang. Syst. 22(2), 416–430 (2000)CrossRefGoogle Scholar
  24. 24.
    Sakarovitch, J.: The ”last” decision problem for rational trace languages. In: Simon, I. (ed.) LATIN 1992. LNCS, vol. 583, pp. 460–473. Springer, Heidelberg (1992)Google Scholar
  25. 25.
    Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 300–314. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  26. 26.
    Thomas, W.: On logical definability of trace languages. In: Proceedings of Algebraic and Syntactic Methods in Computer Science (ASMICS), Report TUM-I9002, Technical University of Munich, pp. 172–182 (1990)Google Scholar
  27. 27.
    Zielonka, W.: Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications 21, 99–135 (1987)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Benedikt Bollig
    • 1
  • Manuela-Lidia Grindei
    • 1
  • Peter Habermehl
    • 1
    • 2
  1. 1.LSV, ENS Cachan, CNRS, INRIAFrance
  2. 2.LIAFA, CNRS and University Paris Diderot (Paris 7)France

Personalised recommendations