A linear process-algebraic format with data for probabilistic automata

DOI10.1016/J.TCS.2011.07.021MaRDI QIDQ764285zbMATH OpenOpenAlexWikidataFDO

Authors Joost-Pieter Katoen, Jaco van de Pol, Mark Timmer, Mariëlle I. A. Stoelinga

Publication date 13 March 2012

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2011.07.021

zbMATH Keywords

linearizationstate space reductionprobabilistic process algebra\(\mu \text{CRL}\)data-dependent probabilistic choicesymbolic transformation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 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)

Recommendations

• Abstract probabilistic automata
• Abstract probabilistic automata
• Compositional abstraction techniques for probabilistic automata
• Bisimulations meet PCTL equivalences for probabilistic automata
• Probabilistic communicating processes

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1303726 (Why is no real title available?)
• scientific article; zbMATH DE number 1884411 (Why is no real title available?)
• scientific article; zbMATH DE number 1905121 (Why is no real title available?)
• A database approach to distributed state-space generation
• A game-based abstraction-refinement framework for Markov decision processes
• A linear process-algebraic format with data for probabilistic automata
• A logic for reasoning about time and reliability
• Abstraction Refinement for Probabilistic Software
• An abstract interpretation toolkit for \(\mu\)CRL
• Bisimulation through probabilistic testing
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Cones and foci: A mechanical framework for protocol verification
• Confluence Reduction for Probabilistic Systems
• Focus points and convergent process operators: A proof strategy for protocol verification
• Linearization of hybrid processes
• Magnifying-Lens Abstraction for Markov Decision Processes
• Model-checking processes with data
• Probabilistic CEGAR
• Simplifying Itai-Rodeh leader election for anonymous rings
• Sliding Window Abstraction for Infinite Markov Chains
• State space reduction of linear processes using control flow reconstruction
• Symbolic Reachability for Process Algebras with Recursive Data Types
• Symmetry breaking in distributed networks
• Three-Valued Abstraction for Continuous-Time Markov Chains

Cited in

(3)

• A linear process-algebraic format with data for probabilistic automata
• Layered reasoning for randomized distributed algorithms
• Counterexample generation for discrete-time Markov models: an introductory survey

Describes a project that uses

Uses Software

• PRISM
• MoDeST
• E-LOTOS
• CEGAR
• CADP

This page was built for publication: A linear process-algebraic format with data for probabilistic automata

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