Efficient CTMC Model Checking of Linear Real-Time Objectives

DOI10.1007/978-3-642-19835-9_12zbMath1315.68174WikidataQ57801239 ScholiaQ57801239MaRDI QIDQ3000642

Benoît Barbot, Alexandru Mereacre, Taolue Chen, Tingting Han, Joost-Pieter Katoen

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_12

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

Unnamed Item, The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism, The quest for minimal quotients for probabilistic and Markov automata, On-the-fly verification and optimization of DTA-properties for large Markov chains, On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets, Fluid Model Checking of Timed Properties, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, Fixed-Delay Events in Generalized Semi-Markov Processes Revisited, Time-Bounded Verification of CTMCs against Real-Time Specifications

Uses Software

• PRISM
• MRMC

Cites Work

• Unnamed Item
• Optimal state-space lumping in Markov chains
• A theory of timed automata
• Simple O(m logn) Time Markov Chain Lumping
• Stochastic Real-Time Games with Qualitative Timed Automata Objectives
• Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking