Time-Bounded Verification of CTMCs against Real-Time Specifications

DOI10.1007/978-3-642-24310-3_4MaRDI QIDQ3172840zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Efficient CTMC Model Checking of Linear Real-Time Objectives
• scientific article; zbMATH DE number 49713
• 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

Cites work

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

Cited in

(13)

• Smoothed model checking for uncertain continuous-time Markov chains
• Verification of linear duration properties over continuous-time Markov chains
• 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
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
• 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
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach
• 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)