Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains

DOI10.1007/978-3-540-85778-5_15MaRDI QIDQ3543299zbMATH OpenOpenAlexWikidataFDO

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

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 193017 (Why is no real title available?)
• scientific article; zbMATH DE number 3511563 (Why is no real title available?)
• scientific article; zbMATH DE number 1538068 (Why is no real title available?)
• scientific article; zbMATH DE number 3413713 (Why is no real title available?)
• A theory of timed automata
• Algebraic laws for nondeterminism and concurrency
• Bisimulation through probabilistic testing
• Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Exact and ordinary lumpability in finite Markov chains
• Interactive Markov chains. And the quest for quantified quality
• Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
• Model-checking continuous-time Markov chains

Cited in

(5)

• 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
• Compositional Modeling and Minimization of Time-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: 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)