Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains

DOI10.1007/978-3-540-85778-5_15zbMATH Open1171.68550OpenAlexW128642691WikidataQ57801664 ScholiaQ57801664MaRDI QIDQ3543299FDOQ3543299

Authors: 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

Recommendations

• Model-checking continuous-time Markov chains
• Model checking finite-horizon Markov chains with probabilistic inference
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking for Hidden Markov Models
• scientific article; zbMATH DE number 7760477
• Tools and Algorithms for the Construction and Analysis of Systems
• Accelerated model checking of parametric Markov chains
• LTL model checking of time-inhomogeneous Markov chains
• Model checking of open interval Markov chains

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

• LTL model checking of time-inhomogeneous Markov chains
• Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains
• Model checking single agent behaviours by fluid approximation
• Checking individual agent behaviours in Markov population models by fluid approximation
• Performability assessment by model checking of Markov reward models

Uses Software

• MRMC

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

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