Time-Bounded Verification of CTMCs against Real-Time Specifications
From MaRDI portal
Publication:3172840
DOI10.1007/978-3-642-24310-3_4zbMath1348.68126MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
60J28: Applications of continuous-time Markov processes on discrete state spaces
68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Related Items
The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism, Smoothed model checking for uncertain continuous-time Markov chains, When are stochastic transition systems tameable?, Model checking single agent behaviours by fluid approximation, System design of stochastic models using robustness of temporal properties, On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets, Time-Bounded Verification of CTMCs against Real-Time Specifications
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
