In a dynamic parametric process every sub-process 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.
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|Reachability for dynamic parametric processes|
|Synthesizing Non-Vacuous Systems|
Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , ma e , Ofer Strichman TechnionFile Attached
|Solving Nonlinear Integer Arithmetic with MCSat|
Dejan Jovanović SRI International