Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains

DOI10.1007/978-3-540-85778-5_15zbMath1171.68550OpenAlexW128642691WikidataQ57801664 ScholiaQ57801664MaRDI QIDQ3543299

Alexandru Mereacre, Joost-Pieter Katoen

Publication date: 2 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-85778-5_15

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation ⋮ Performability assessment by model checking of Markov reward models ⋮ LTL Model Checking of Time-Inhomogeneous Markov Chains ⋮ Model checking single agent behaviours by fluid approximation

Uses Software

• MRMC

Cites Work

• Interactive Markov chains. And the quest for quantified quality
• Bisimulation through probabilistic testing
• A theory of timed automata
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains
• Algebraic laws for nondeterminism and concurrency
• Exact and ordinary lumpability in finite Markov chains
• Model-checking continuous-time Markov chains
• Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains