Time-Bounded Verification of CTMCs against Real-Time Specifications
From MaRDI portal
Publication:3172840
DOI10.1007/978-3-642-24310-3_4zbMath1348.68126OpenAlexW77257248MaRDI QIDQ3172840
Marta Kwiatkowska, Taolue Chen, Alexandru Mereacre, Marco Diciolla
Publication date: 7 October 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-24310-3_4
Specification and verification (program logics, model checking, etc.) (68Q60) Applications of continuous-time Markov processes on discrete state spaces (60J28) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (7)
Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ When are stochastic transition systems tameable? ⋮ On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets ⋮ The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism ⋮ Model checking single agent behaviours by fluid approximation ⋮ System design of stochastic models using robustness of temporal properties ⋮ Smoothed model checking for uncertain continuous-time Markov chains
Cites Work
- Real-time logics: Complexity and expressiveness
- A theory of timed automata
- The deconvolution operation in convex analysis: an introduction
- On the expressiveness of TPTL and MTL
- Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
- Efficient CTMC Model Checking of Linear Real-Time Objectives
- Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- Time-Bounded Verification
- A Laplace transform algorithm for the volume of a convex polytope
- Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
- Weighted Lumpability on Markov Chains
- Towards a Theory of Time-Bounded Verification
- From Mtl to Deterministic Timed Automata
- A really temporal logic
- COMPLEXITY AND REAL COMPUTATION: A MANIFESTO
- The complexity of probabilistic verification
- The benefits of relaxing punctuality
- On the decidability and complexity of Metric Temporal Logic over finite words
- Convexity recognition of the union of polyhedra
This page was built for publication: Time-Bounded Verification of CTMCs against Real-Time Specifications
