Analysis of probabilistic basic parallel processes

DOI10.1007/978-3-642-54830-7_3MaRDI QIDQ5410663zbMATH OpenOpenAlexFDO

Authors Rémi Bonnet, Stefan Kiefer, Anthony Widjaja Lin

Publication date 16 April 2014

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

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

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Basic Parallel Processes (BPPs) are a well-known subclass of Petri Nets. They are the simplest common model of concurrent programs that allows unbounded spawning of processes. In the probabilistic version of BPPs, every process generates other processes according to a probability distribution. We study the decidability and complexity of fundamental qualitative problems over probabilistic BPPs -- in particular reachability with probability 1 of different classes of target sets (e.g. upward-closed sets). Our results concern both the Markov-chain model, where processes are scheduled randomly, and the MDP model, where processes are picked by a scheduler.

Recommendations

• On reachability equivalence for BPP-nets
• Publication:4490743
• On probabilistic parallel programs with process creation and synchronisation
• Decidability of performance equivalence for basic parallel processes
• Undecidable equivalences for basic parallel processes

Cited in

(5)

• Fair termination for parameterized probabilistic concurrent systems
• Probabilistic Analysis of Binary Sessions
• scientific article; zbMATH DE number 7561608 (Why is no real title available?)
• On probabilistic parallel programs with process creation and synchronisation
• Bounded model checking liveness on basic parallel processes

This page was built for publication: Analysis of probabilistic basic parallel processes

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