Skip to Main content Skip to Navigation
Conference papers

Realizability of Concurrent Recursive Programs

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Benedikt Bollig Connect in order to contact the contributor
Submitted on : Friday, January 11, 2013 - 10:25:14 AM
Last modification on : Thursday, January 20, 2022 - 5:28:37 PM
Long-term archiving on: : Friday, April 12, 2013 - 11:20:44 AM


Files produced by the author(s)



Benedikt Bollig, Manuela-Lidia Grindei, Peter Habermehl. Realizability of Concurrent Recursive Programs. Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'09), 2009, York, UK, United Kingdom. pp.410-424, ⟨10.1007/978-3-642-00596-1_29⟩. ⟨hal-00772771⟩



Record views


Files downloads