Time-Bounded Verification of CTMCs against Real-Time Specifications

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

Mathematics Subject Classification ID

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