Efficient CTMC Model Checking of Linear Real-Time Objectives

DOI10.1007/978-3-642-19835-9_12MaRDI QIDQ3000642zbMATH OpenOpenAlexWikidataFDO

Authors Benoît Barbot, Taolue Chen, Tingting Han, Alexandru Mereacre, Joost-Pieter Katoen

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19835-9_12

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Correctness of efficient real-time model checking
• Model-checking in dense real-time
• Approximate model checking of real-time systems for linear duration invariants
• Practical Efficient Modular Linear-Time Model-Checking
• On Expressiveness and Complexity in Real-Time Model Checking
• Exact acceleration of real-time model checking
• Timed CTL model checking in Real-Time Maude
• Efficient timed model checking for discrete-time systems

Cites work

• scientific article; zbMATH DE number 1337733 (Why is no real title available?)
• A theory of timed automata
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
• Distributed Markovian bisimulation reduction aimed at CSL model checking
• Optimal state-space lumping in Markov chains
• Simple \(O(m \log n)\) time Markov chain lumping
• Stochastic Real-Time Games with Qualitative Timed Automata Objectives

Cited in

(13)

• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
• Monitoring CTMCs by multi-clock timed automata
• 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
• Fixed-delay events in generalized semi-Markov processes revisited
• The quest for minimal quotients for probabilistic and Markov automata
• Fluid model checking of timed properties
• The linear time-branching time spectrum of equivalences for stochastic systems with non-determinism
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• scientific article; zbMATH DE number 1884410 (Why is no real title available?)
• A probabilistic logic for verifying continuous-time Markov chains

Describes a project that uses

Uses Software

• MRMC
• PRISM

This page was built for publication: Efficient CTMC Model Checking of Linear Real-Time Objectives

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