On the use of MTBDDs for performability analysis and verification of stochastic systems.

DOI10.1016/S1567-8326(02)00066-8zbMath1054.68018MaRDI QIDQ1400289

D. Massart

Publication date: 13 August 2003

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

zbMATH Keywords

Markov chainMarkov decision processModel checkingBinary decision diagramsMulti-terminal binary decision diagramsPerformability analysis

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (5)

A General Framework for Probabilistic Characterizing Formulae ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Partially-shared zero-suppressed multi-terminal BDDs: Concept, algorithms and applications ⋮ Distributed disk-based algorithms for model checking very large Markov chains ⋮ Model checking for performability

Uses Software

• PRISM
• LOTOS
• CUDD

Cites Work

• Interactive Markov chains. And the quest for quantified quality
• Specification-oriented semantics for communicating processes
• A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time
• Bisimulation through probabilistic testing
• Transient solutions in Markovian queues. An algorithm for finding them and determining their waiting-time distributions
• A class of hierarchical queueing networks and their analysis
• Automated compositional Markov chain generation for a plain-old telephone system
• Generating BDDs for symbolic model checking in CCS
• Model checking of probabilistic and nondeterministic systems
• Fast randomized consensus using shared memory
• Graph-Based Algorithms for Boolean Function Manipulation
• The complexity of probabilistic verification
• Improving the variable ordering of OBDDs is NP-complete
• Termination of Probabilistic Concurrent Program
• Compositional performance modelling with the TIPPtool
• Process algebra for performance evaluation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the use of MTBDDs for performability analysis and verification of stochastic systems.