Realizability of Concurrent Recursive Programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Realizability of Concurrent Recursive Programs

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
BGH-fossacs09.pdf (215.78 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00772771 , version 1 (11-01-2013)

Identifiants

Citer

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⟩
103 Consultations
105 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More