Vi definierar och studerar en automatiserad modell av samtidiga rekursiva program. En automaton består av ett begränsat antal pushdown-system som körs parallellt och kommunicerar via delade åtgärder. Vi kombinerar faktiskt multi-stacken synbart pushdown automata och Zielonkas asynkrona automata mot en modell med ett obeslutsamt tomrumsproblem. Men en rimlig begränsning gör att vi kan lyfta Zielonkas teorem till denna rekursiva inställning och tillåter en logisk karakterisering i form av en lämplig monadisk andraordningslogik. Med utgångspunkt i resultaten från Mazurkiewicz spårteori och arbete av La Torre, Madhusudan och Parlato utvecklar vi därmed en ram för specifikation, syntes och verifiering av samtidiga rekursiva processer.
I REF utsträcks modellen till att användas som boplats för Mazurkiewicz-spår och Zielonkas konstruktion lyfts till denna miljö.
Realizability of Concurrent Recursive Programs
{'venue': 'Lecture Notes in Computer Science', 'journal': 'Lecture Notes in Computer Science', 'mag_field_of_study': ['Computer Science']}