A linear process-algebraic format with data for probabilistic automata
type: Item
instance of: scholarly article
title: A linear process-algebraic format with data for probabilistic automata
zbMATH Open document ID: 1283.68246
author: Joost-Pieter Katoen
author: Jaco van de Pol
author: Mark Timmer
author: Mariëlle I. A. Stoelinga
published in: Theoretical Computer Science
publication date: 2012-03-13T00:00:00Z
review text: A novel linear process-algebraic format for probabilistic automata is presented. The key ingredient is a symbolic transformation of probabilistic process algebra terms (terms of prCRL which is restricted \(\mu \text{CRL}\) with a probabilistic choice operator) that incorporate data into this linear format while preserving strong probabilistic bisimulation. This generalizes similar techniques for traditional process algebras with data, and treats data and data-dependent probabilistic choice in a fully symbolic manner, leading to the symbolic analysis of parameterized probabilistic systems. Several reduction techniques that can be easily applied to the presented models are discussed. A validation of the presented approach is presented on a benchmark case study, namely leader election protocols. It shows significant reductions of states, transitions as well as running time.
reviewed by: Damas Gruska
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68Q87
zbMATH DE Number: 6014287
zbMATH Keywords: probabilistic process algebra
zbMATH Keywords: linearization
zbMATH Keywords: data-dependent probabilistic choice
zbMATH Keywords: symbolic transformation
zbMATH Keywords: state space reduction
zbMATH Keywords: \(\mu \text{CRL}\)
describes a project that uses: PRISM
describes a project that uses: MoDeST
describes a project that uses: CADP
describes a project that uses: CEGAR
describes a project that uses: E-LOTOS
MaRDI profile type: Publication
full work available at URL: j.tcs.2011.07.021
OpenAlex ID: W2018187447
Wikidata QID: Q57801041
cites work: Q4798031
cites work: Magnifying-Lens Abstraction for Markov Decision Processes
cites work: Sliding Window Abstraction for Infinite Markov Chains
cites work: Three-Valued Abstraction for Continuous-Time Markov Chains
cites work: A game-based abstraction-refinement framework for Markov decision processes
cites work: Probabilistic CEGAR
cites work: Abstraction Refinement for Probabilistic Software
cites work: Bisimulation through probabilistic testing
cites work: Linearization of hybrid processes
cites work: Focus points and convergent process operators: A proof strategy for protocol verification
cites work: Cones and foci: A mechanical framework for protocol verification
cites work: State Space Reduction of Linear Processes Using Control Flow Reconstruction
cites work: An abstract interpretation toolkit for \(\mu\)CRL
cites work: A Database Approach to Distributed State-Space Generation
cites work: Symbolic Reachability for Process Algebras with Recursive Data Types
cites work: Q4250361
cites work: Model-checking processes with data
cites work: Q4806211
cites work: Q3992568
cites work: A logic for reasoning about time and reliability
cites work: Confluence Reduction for Probabilistic Systems
cites work: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
cites work: Symmetry breaking in distributed networks
cites work: Simplifying Itai-Rodeh leader election for anonymous rings
DOI: 10.1016/J.TCS.2011.07.021
description: scientific article; zbMATH DE number 6014287