Model checking infinite-state Markov chains

DOI10.1007/978-3-540-31980-1_16MaRDI QIDQ5703762zbMATH OpenOpenAlexFDO

Authors Anne Remke, B. R. Haverkort, Lucia Cloth

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

Logic in computer science (03B70) Continuous-time Markov processes on discrete state spaces (60J27) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• CSL model checking algorithms for QBDs
• CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
• Model-checking large structured Markov chains.
• Model-checking continuous-time Markov chains
• A Markov chain model checker

Cited in

(19)

• Model-checking large structured Markov chains.
• Performance analysis for (X,S)-bottleneck cell in large-scale wireless networks
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• Formal reasoning about finite-state discrete-time Markov chains in HOL
• Simulative model checking of steady state and time-unbounded temporal operators
• Carrying probabilities to the infinite world
• CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• Model Checking Interactive Markov Chains
• Sliding Window Abstraction for Infinite Markov Chains
• Model checking interactive Markov chains
• LTL model checking of time-inhomogeneous Markov chains
• A Markov chain model checker
• Beyond memoryless distributions: model checking semi-Markov chains
• Model checking CSL until formulae with random time bounds
• Distributed Markovian bisimulation reduction aimed at CSL model checking
• Performability assessment by model checking of Markov reward models
• An analytical model for end-to-end communication channel over PLCN based on QBDs
• CSL model checking algorithms for QBDs

This page was built for publication: Model checking infinite-state Markov chains

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