Observing continuous-time MDPs by 1-clock timed automata

DOI10.1007/978-3-642-24288-5_2zbMATH Open1348.68127OpenAlexW9281975WikidataQ57801283 ScholiaQ57801283MaRDI QIDQ3172860FDOQ3172860

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

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

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

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)

Cited In (4)

• Monitoring CTMCs by multi-clock timed automata
• Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
• Fluid Model Checking of Timed Properties
• A probabilistic logic for verifying continuous-time Markov chains

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)