Efficient CTMC Model Checking of Linear Real-Time Objectives
DOI10.1007/978-3-642-19835-9_12zbMATH Open1315.68174OpenAlexW2103836778WikidataQ57801239 ScholiaQ57801239MaRDI QIDQ3000642FDOQ3000642
Authors: Benoît Barbot, Taolue Chen, Tingting Han, Alexandru Mereacre, 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
Recommendations
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- Correctness of efficient real-time model checking
- Model-checking in dense real-time
- Approximate model checking of real-time systems for linear duration invariants
- Practical Efficient Modular Linear-Time Model-Checking
- On Expressiveness and Complexity in Real-Time Model Checking
- Exact acceleration of real-time model checking
- Timed CTL model checking in Real-Time Maude
- Efficient timed model checking for discrete-time systems
Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- A theory of timed automata
- Title not available (Why is that?)
- Stochastic Real-Time Games with Qualitative Timed Automata Objectives
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Optimal state-space lumping in Markov chains
- Simple \(O(m \log n)\) time Markov chain lumping
- Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking
Cited In (13)
- Monitoring CTMCs by multi-clock timed automata
- Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems
- 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
- Fixed-delay events in generalized semi-Markov processes revisited
- The quest for minimal quotients for probabilistic and Markov automata
- The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
- Fluid Model Checking of Timed Properties
- Title not available (Why is that?)
- Title not available (Why is that?)
- A probabilistic logic for verifying continuous-time Markov chains
Uses Software
This page was built for publication: Efficient CTMC Model Checking of Linear Real-Time Objectives
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000642)
