Observing continuous-time MDPs by 1-clock timed automata

DOI10.1007/978-3-642-24288-5_2MaRDI QIDQ3172860zbMATHOpenAlexWikidataFDO

Authors Taolue Chen, Tingting Han, Alexandru Mereacre, Joost-Pieter Katoen

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-24288-5_2

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

• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• On-the-fly verification and optimization of DTA-properties for large Markov chains
• Monitoring CTMCs by multi-clock timed automata
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(7)

• Monitoring CTMCs by multi-clock timed automata
• Fluid model checking of timed properties
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• A probabilistic logic for verifying continuous-time Markov chains
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Measuring performance of continuous-time stochastic processes using timed automata

Describes a project that uses

Uses Software

• MRMC
• LiQuor

This page was built for publication: Observing continuous-time MDPs by 1-clock timed automata

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