Static Partial Order Reduction for Probabilistic Concurrent Systems

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

Abstract

Sound criteria for partial order reduction for probabilistic concurrent systems have been presented in the literature. Their realization relies on a depth-first search-based approach for generating the reduced model. The drawback of this dynamic approach is that it can hardly be combined with other techniques to tackle the state explosion problem, e.g., symbolic probabilistic model checking with multi-terminal variants of binary decision diagrams. Following the approach presented by Kurshan et al. for non-probabilistic systems, we study partial order reduction techniques for probabilistic concurrent systems that can be realized by a static analysis. The idea is to inject the reduction criteria into the control flow graphs of the processes of the system to be analyzed. We provide the theoretical foundations of static partial order reduction for probabilistic concurrent systems and present algorithms to realize them. Finally, we report on some experimental results.

Details

Original languageEnglish
Title of host publication2012 Ninth International Conference on Quantitative Evaluation of Systems
PublisherIEEE, New York [u. a.]
Pages104-113
Number of pages10
ISBN (print)978-0-7695-4781-7
Publication statusPublished - 20 Sept 2012
Peer-reviewedYes

Conference

Title2012 Ninth International Conference on Quantitative Evaluation of Systems
Duration17 - 20 September 2012
LocationLondon, UK

External IDs

Scopus 84870766876
ORCID /0000-0002-5321-9343/work/142236771

Keywords

Keywords

  • Probabilistic logic, Explosions, Process control, Markov processes, Labeling, Computational modeling