Faster and symbolic CTMC model checking

DOI10.1007/3-540-44804-7_2MaRDI QIDQ4798030zbMATH OpenFDO

Authors Joost-Pieter Katoen, Marta Kwiatkowska, Gethin Norman, David Parker

Publication date 18 March 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2165/21650023.htm, https://ris.utwente.nl/ws/files/5292500/86_fastctmc.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Approximate symbolic model checking of continuous-time Markov chains
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• Probabilistic symbolic model checking with PRISM: A hybrid approach
• Model checking continuous-time Markov chains by transient analysis
• Model-checking continuous-time Markov chains

Cited in

(23)

• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Model-checking large structured Markov chains.
• Hypergraph-based parallel computation of passage time densities in large semi-Markov models
• A formal approach to adaptive software: continuous assurance of non-functional requirements
• HyperPCTL model checking by probabilistic decomposition
• Comparative branching-time semantics for Markov chains
• Model checking expected time and expected reward formulae with random time bounds
• Statistical probabilistic model checking with a focus on time-bounded properties
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• Model checking continuous-time Markov chains by transient analysis
• Compositional model checking of product-form CTMCs
• Automata-based CSL model checking
• Faster SPDL Model Checking Through Property-Driven State Space Generation
• Approximate symbolic model checking of continuous-time Markov chains
• Probabilistic symbolic model checking with PRISM: A hybrid approach
• Faster model checking for open systems
• Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation
• Model checking CSL until formulae with random time bounds
• scientific article; zbMATH DE number 1423228 (Why is no real title available?)
• CCMC: a conditional CSL model checker for continuous-time Markov chains
• Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic
• An MM algorithm to estimate parameters in continuous-time Markov chains
• Compositional analysis of probabilistic timed graph transformation systems

Describes a project that uses

Uses Software

• CUDD

This page was built for publication: Faster and symbolic CTMC model checking

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