Model-checking continuous-time Markov chains
From MaRDI portal
Publication:5738903
DOI10.1145/343369.343402zbMath1365.68313OpenAlexW2041226400MaRDI QIDQ5738903
Vigyan Singhal, Adnan Aziz, Kumud Sanwal, Robert K. Brayton
Publication date: 13 June 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/343369.343402
Specification and verification (program logics, model checking, etc.) (68Q60) Continuous-time Markov processes on discrete state spaces (60J27)
Related Items (53)
Measuring the constrained reachability in quantum Markov chains ⋮ Model Checking of Biological Systems ⋮ Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation ⋮ Least upper bounds for probability measures and their applications to abstractions ⋮ Comparative branching-time semantics for Markov chains ⋮ Precisely deciding CSL formulas through approximate model checking for CTMCs ⋮ Computing Behavioral Relations for Probabilistic Concurrent Systems ⋮ Precise parameter synthesis for stochastic biochemical systems ⋮ Efficient trace generation for rare-event analysis in chemical reaction networks ⋮ Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference ⋮ Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach ⋮ Model-checking large structured Markov chains. ⋮ Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking ⋮ The computability of LQR and LQG control ⋮ Markov Set-Chains as Abstractions of Stochastic Hybrid Systems ⋮ Approximating Markov processes through filtration ⋮ Three-valued abstraction for probabilistic systems ⋮ Comparative Analysis of Statistical Model Checking Tools ⋮ Computing branching distances with quantitative games ⋮ Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains ⋮ State-Aware Performance Analysis with eXtended Stochastic Probes ⋮ Sampling-Based Verification of CTMCs with Uncertain Rates ⋮ How Might Petri Nets Enhance Your Systems Biology Toolkit ⋮ Automata-Based CSL Model Checking ⋮ Probabilistic Model Checking of the PDGF Signaling Pathway ⋮ Guarded autonomous transitions increase conciseness and expressiveness of timed automata ⋮ Performability assessment by model checking of Markov reward models ⋮ Model checking expected time and expected reward formulae with random time bounds ⋮ Model checking Markov population models by stochastic approximations ⋮ CSL model checking algorithms for QBDs ⋮ Model checking mobile stochastic logic ⋮ Statistical probabilistic model checking with a focus on time-bounded properties ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Survey on Directed Model Checking ⋮ Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing ⋮ Compositional Model Checking of product-form CTMCs ⋮ Assisting the design of a groupware system - Model checking usability aspects of thinkteam ⋮ Symbolic computation of differential equivalences ⋮ Extended Stochastic Petri Nets for Model-Based Design of Wetlab Experiments ⋮ LTL Model Checking of Time-Inhomogeneous Markov Chains ⋮ Statistical Model Checking Using Perfect Simulation ⋮ Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games ⋮ A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models ⋮ Logical characterization of fluid equivalences ⋮ Model checking for performability ⋮ Compositional construction of control barrier functions for continuous-time stochastic hybrid systems ⋮ Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes ⋮ Stochastic Model Checking of the Stochastic Quality Calculus ⋮ Model checking single agent behaviours by fluid approximation ⋮ Some decidable results on reachability of solvable systems ⋮ Computing Cumulative Rewards Using Fast Adaptive Uniformization
This page was built for publication: Model-checking continuous-time Markov chains
