LTL model checking of time-inhomogeneous Markov chains

DOI10.1007/978-3-642-04761-9_10MaRDI QIDQ3648693zbMATH OpenOpenAlexWikidataFDO

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

Publication date 1 December 2009

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Recommendations

• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• scientific article; zbMATH DE number 1670788
• Model-checking continuous-time Markov chains
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• A logic for reasoning about time and reliability
• An optimal automata approach to LTL model checking of probabilistic systems
• Complementation, Disambiguation, and Determinization of Büchi Automata Unified
• scientific article; zbMATH DE number 52120 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 956802 (Why is no real title available?)
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• Model-checking continuous-time Markov chains
• Rational \(\omega\)-languages are non-ambiguous
• The complexity of probabilistic verification
• Unambiguous Büchi automata.

Cited in

(5)

• Model checking single agent behaviours by fluid approximation
• Analysis of timed and long-run objectives for Markov automata
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• Checking individual agent behaviours in Markov population models by fluid approximation

Describes a project that uses

Uses Software

• MRMC

This page was built for publication: LTL model checking of time-inhomogeneous Markov chains

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