LTL Model Checking of Time-Inhomogeneous Markov Chains

DOI10.1007/978-3-642-04761-9_10zbMath1262.68108OpenAlexW2125571758WikidataQ57801547 ScholiaQ57801547MaRDI QIDQ3648693

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)

Related Items (2)

Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation ⋮ Model checking single agent behaviours by fluid approximation

Uses Software

• MRMC

Cites Work

• Rational \(\omega\)-languages are non-ambiguous
• A logic for reasoning about time and reliability
• Unambiguous Büchi automata.
• Complementation, Disambiguation, and Determinization of Büchi Automata Unified
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• The complexity of probabilistic verification
• Model-checking continuous-time Markov chains
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: LTL Model Checking of Time-Inhomogeneous Markov Chains