Efficient CTMC Model Checking of Linear Real-Time Objectives
From MaRDI portal
Publication:3000642
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
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, Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties, 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
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