Realizability of concurrent recursive programs
DOI10.1007/s10703-017-0282-yzbMath1425.68062OpenAlexW2738591572MaRDI QIDQ1620953
Manuela-Lidia Grindei, Peter Habermehl, Benedikt Bollig
Publication date: 15 November 2018
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-017-0282-y
monadic second-order logicrealizabilityasynchronous automataconcurrent recursive programsMazurkiewicz tracesnested-word automataZielonka's theorem
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Temporal logics for concurrent recursive programs: satisfiability and model checking
- Weighted asynchronous cellular automata
- An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
- Bounded MSC communication
- Regular sets of infinite message sequence charts
- A Kleene theorem and model checking algorithms for existentially bounded communicating automata
- A theory of regular MSC languages
- MSO Decidability of Multi-Pushdown Systems via Split-Width
- A Unifying Approach for Multistack Pushdown Automata
- Model Checking Concurrent Recursive Programs Using Temporal Logics
- Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width
- Reachability of Multistack Pushdown Systems with Scope-Bounded Matching Relations
- Controllers for the Verification of Communicating Multi-pushdown Systems
- Adding nesting structure to words
- Verifying Communicating Multi-pushdown Systems via Split-Width
- Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
- An Infinite Automaton Characterization of Double Exponential Time
- Optimal Zielonka-Type Construction of Deterministic Asynchronous Automata
- Constructing Exponential-Size Deterministic Zielonka Automata
- Realizability of Concurrent Recursive Programs
- On the Expressive Power of 2-Stack Visibly Pushdown Automata
- Notes on finite asynchronous automata
- Model-Checking Bounded Multi-Pushdown Systems
- On Visibly Pushdown Trace Languages
- The Complexity of Model Checking Multi-stack Systems
- The tree width of auxiliary storage
- Interprocedural Analysis of Concurrent Programs Under a Context Bound
- Context-Bounded Analysis of Concurrent Queue Systems
- Synthesis of Safe Message-Passing Systems
- MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
- Tools and Algorithms for the Construction and Analysis of Systems
- Scope-Bounded Pushdown Languages
- Reachability Analysis of Communicating Pushdown Systems
- CONCUR 2003 - Concurrency Theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
