A linear process-algebraic format with data for probabilistic automata

DOI10.1016/J.TCS.2011.07.021zbMATH Open1283.68246OpenAlexW2018187447WikidataQ57801041 ScholiaQ57801041MaRDI QIDQ764285FDOQ764285

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

Recommendations

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

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)

Cites Work

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

Cited In (3)

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

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)