Reachability for dynamic parametric processes

DOI10.1007/978-3-319-52234-0_23MaRDI QIDQ2961580zbMATH OpenOpenAlexFDO

Authors Anca Muscholl, Helmut Seidl, Igor Walukiewicz

Publication date 21 February 2017

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

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

Mathematics Subject Classification ID

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

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.

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

Cites work

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

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

Describes a project that uses

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)