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

https://hal.inria.fr/hal-00772771
Contributor : Benedikt Bollig <>
Submitted on : Friday, January 11, 2013 - 10:25:14 AM
Last modification on : Monday, February 15, 2021 - 10:41:15 AM
Long-term archiving on: : Friday, April 12, 2013 - 11:20:44 AM

File

BGH-fossacs09.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

421

Files downloads

677