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.

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Benedikt Bollig, Manuela-Lidia Grindei, Peter Habermehl
• Keywords: Applied Computing, Concurrent Recursive Processes, Concurrent Recursive Programs, FOSSACS 2009, Zielonka’s Asynchronous Automata