Time-Bounded Verification of CTMCs against Real-Time Specifications

DOI10.1007/978-3-642-24310-3_4zbMATH Open1348.68126OpenAlexW77257248MaRDI QIDQ3172840FDOQ3172840

Authors: Taolue Chen, Marco Diciolla, Marta Kwiatkowska, Alexandru Mereacre 

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

Recommendations

• Efficient CTMC Model Checking of Linear Real-Time Objectives
• scientific article
• Specification and compositional verification of real-time systems
• Complexity bounds for the verification of real-time software
• Verifying continuous-time duration calculus against real-time automaton
• Compositional verification of real-time systems with explicit clock temporal logic
• Timed CTL model checking in Real-Time Maude
• Verifying complex continuous real-time systems with coinductive CLP(R)
• Formal Modeling and Analysis of Timed Systems

Mathematics Subject Classification ID

Applications of continuous-time Markov processes on discrete state spaces (60J28) 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
• COMPLEXITY AND REAL COMPUTATION: A MANIFESTO
• The complexity of probabilistic verification
• On the expressiveness of TPTL and MTL
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• From \textsc{mtl} to deterministic timed automata
• A really temporal logic
• The benefits of relaxing punctuality
• Real-time logics: Complexity and expressiveness
• On the decidability and complexity of Metric Temporal Logic over finite words
• A Laplace transform algorithm for the volume of a convex polytope
• Weighted Lumpability on Markov Chains
• Convexity recognition of the union of polyhedra
• Time-bounded model checking of infinite-state continuous-time Markov chains
• Time-Bounded Verification
• The deconvolution operation in convex analysis: an introduction
• Towards a theory of time-bounded verification
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Efficient CTMC Model Checking of Linear Real-Time Objectives

Cited In (10)

• Smoothed model checking for uncertain continuous-time Markov chains
• On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets
• When are stochastic transition systems tameable?
• Model checking single agent behaviours by fluid approximation
• System design of stochastic models using robustness of temporal properties
• The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• A probabilistic logic for verifying continuous-time Markov chains

This page was built for publication: Time-Bounded Verification of CTMCs against Real-Time Specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172840)