Reachability for dynamic parametric processes

DOI10.1007/978-3-319-52234-0_23zbMATH Open1484.68143arXiv1609.05385OpenAlexW2522644249MaRDI QIDQ2961580FDOQ2961580

Authors: Anca Muscholl, Helmut Seidl, Igor Walukiewicz 

Publication date: 21 February 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent. We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.

Full work available at URL: https://arxiv.org/abs/1609.05385

Recommendations

• Reachability analysis of communicating pushdown systems
• Parameterised pushdown systems with non-atomic writes
• Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
• Advances in Parametric Real-Time Reasoning
• Constrained dynamic tree networks

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
• Computer Aided Verification
• CONCUR 2005 – Concurrency Theory
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Collapsible pushdown automata and recursion schemes
• Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
• Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
• Parameterised pushdown systems with non-atomic writes
• Reachability under contextual locking

Cited In (4)

• Fully Dynamic Single-Source Reachability in Practice: An Experimental Study
• Replication, refinement \& reachability: complexity in dynamic condition-response graphs
• Parameterized verification under TSO with data types
• Parameterised pushdown systems with non-atomic writes

Uses Software

• Program-Conflict-Analysis

This page was built for publication: Reachability for dynamic parametric processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2961580)