Confluence Reduction for Probabilistic Systems

DOI10.1007/978-3-642-19835-9_29zbMATH Open1316.68077DBLPconf/tacas/TimmerSP11arXiv1011.2314OpenAlexW2131603512WikidataQ62047461 ScholiaQ62047461MaRDI QIDQ3000663FDOQ3000663

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)

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Branching time and abstraction in bisimulation semantics
• Title not available (Why is that?)
• Computer Aided Verification
• Confluence for process verification
• Simplifying Itai-Rodeh leader election for anonymous rings
• Confluence Reduction for Probabilistic Systems
• State space reduction of linear processes using control flow reconstruction
• Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers

Cited In (7)

• Layered reasoning for randomized distributed algorithms
• Title not available (Why is that?)
• A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time
• Confluence Reduction for Probabilistic Systems
• Confluence in probabilistic rewriting
• A linear process-algebraic format with data for probabilistic automata
• Confluence reduction for Markov 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)