Confluence Reduction for Probabilistic Systems

DOI10.1007/978-3-642-19835-9_29MaRDI QIDQ3000663zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Mark Timmer, Mariëlle I. A. Stoelinga, Jaco van de Pol

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.

Recommendations

• Confluence and convergence in probabilistically terminating reduction systems
• Confluence in probabilistic rewriting
• Taming confusion for modeling and implementing probabilistic concurrent systems
• Confluence and convergence modulo equivalence in probabilistically terminating reduction systems
• Introduction to Probabilistic Concurrent Systems
• Confluence reduction for Markov automata
• Confluence reduction for Markov automata
• Concurrency and probability: removing confusion, compositionally
• scientific article; zbMATH DE number 7147446

Cites work

• Branching time and abstraction in bisimulation semantics
• Computer Aided Verification
• Confluence for process verification
• Confluence Reduction for Probabilistic Systems
• scientific article; zbMATH DE number 1905121 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers
• Simplifying Itai-Rodeh leader election for anonymous rings
• State space reduction of linear processes using control flow reconstruction

Cited in

(11)

• Confluence and convergence in probabilistically terminating reduction systems
• Confluence and convergence modulo equivalence in probabilistically terminating reduction systems
• Layered reasoning for randomized distributed algorithms
• Confluence in probabilistic rewriting
• A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time
• Confluence reduction for Markov automata
• A coalgebraic representation of reduction by cone of influence
• Confluence Reduction for Probabilistic Systems
• scientific article; zbMATH DE number 1759425 (Why is no real title available?)
• Confluence reduction for Markov automata
• A linear process-algebraic format with data for probabilistic automata

This page was built for publication: Confluence Reduction for Probabilistic Systems

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