Model-checking large structured Markov chains.

DOI10.1016/S1567-8326(02)00067-XzbMath1048.68053WikidataQ57802004 ScholiaQ57802004MaRDI QIDQ1400291

Carsten Tepper, Peter Kemper, Peter Buchholz, Joost-Pieter Katoen

Publication date: 13 August 2003

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

zbMATH Keywords

Markov chainsModel checkingKronecker algebraStochastic bisimulationStructured analysis

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Computing bottom SCCs symbolically using transition guided reduction, Out of control: reducing probabilistic models by control-state elimination, CSL model checking algorithms for QBDs, Statistical probabilistic model checking with a focus on time-bounded properties, Compositional Model Checking of product-form CTMCs, Assisting the design of a groupware system - Model checking usability aspects of thinkteam, Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

Uses Software

• PRISM
• APNN-Toolbox

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Specification techniques for Markov reward models
• A logic for reasoning about time and reliability
• Efficient computation and representation of large reachability sets for composed automata
• Structured analysis approaches for large Markov chains
• Randomization Procedures in the Computation of Cumulative-Time Distributions over Discrete State Markov Processes
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Superposed stochastic automata: a class of stochastic Petri nets with parallel solution and distributed state space
• Complexity of Memory-Efficient Kronecker Operations with Applications to the Solution of Markov Models
• Integrating synchronization with priority into a Kronecker representation
• Reachability analysis based on structured representations
• Depth-First Search and Linear Graph Algorithms
• Model-checking continuous-time Markov chains
• Process algebra for performance evaluation