A linear process-algebraic format with data for probabilistic automata

DOI10.1016/j.tcs.2011.07.021zbMath1283.68246OpenAlexW2018187447WikidataQ57801041 ScholiaQ57801041MaRDI QIDQ764285

Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, 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) 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)

Related Items (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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A game-based abstraction-refinement framework for Markov decision processes
• A linear process-algebraic format with data for probabilistic automata
• Cones and foci: A mechanical framework for protocol verification
• An abstract interpretation toolkit for \(\mu\)CRL
• Symmetry breaking in distributed networks
• Bisimulation through probabilistic testing
• A logic for reasoning about time and reliability
• Focus points and convergent process operators: A proof strategy for protocol verification
• Linearization of hybrid processes
• Model-checking processes with data
• Confluence Reduction for Probabilistic Systems
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• A Database Approach to Distributed State-Space Generation
• Probabilistic CEGAR
• Abstraction Refinement for Probabilistic Software
• Sliding Window Abstraction for Infinite Markov Chains
• State Space Reduction of Linear Processes Using Control Flow Reconstruction
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Magnifying-Lens Abstraction for Markov Decision Processes
• Symbolic Reachability for Process Algebras with Recursive Data Types

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