Efficient CTMC Model Checking of Linear Real-Time Objectives

DOI10.1007/978-3-642-19835-9_12zbMath1315.68174OpenAlexW2103836778WikidataQ57801239 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

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (10)

Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ 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 ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ On-the-fly verification and optimization of DTA-properties for large Markov chains ⋮ Unnamed Item ⋮ The quest for minimal quotients for probabilistic and Markov automata ⋮ The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism ⋮ Fixed-Delay Events in Generalized Semi-Markov Processes Revisited

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

This page was built for publication: Efficient CTMC Model Checking of Linear Real-Time Objectives