Reachability for dynamic parametric processes

TL;DR

This paper proves the decidability of reachability in dynamic parametric processes with arbitrarily many subprocesses, especially when modeled by pushdown or higher-order pushdown systems, and provides complexity results for subclasses.

Contribution

It establishes decidability of reachability for dynamic parametric processes under mild assumptions and offers algorithms with varying complexity for specific subclasses.

Findings

Reachability is decidable under mild assumptions.

Algorithms with complexity from NP to DEXPTIME for subclasses.

Applicable to processes modeled by pushdown and higher-order pushdown systems.

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.