Approximate symbolic model checking of continuous-time Markov chains

DOI10.1007/3-540-48320-9_12MaRDI QIDQ4270055zbMATH OpenFDO

Authors Holger Hermanns, Christel Baier, Joost-Pieter Katoen

Publication date 25 April 2000

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

Full work available at URL https://ris.utwente.nl/ws/files/268935850/Baier1999approximative.pdf

zbMATH Keywords

continuous-time Markov chainsextension of continuous stochastic logic CSLsymbolic approximate methodsymbolic model checking algorithmsystem of linear equationstemporal logicVolterra integral equation system

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1884410
• Model checking conditional CSL for continuous-time Markov chains
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• Model-checking continuous-time Markov chains
• Automata-based CSL model checking

Cited in

(35)

• Approximating labelled Markov processes
• Model-checking large structured Markov chains.
• A uniformization-based algorithm for continuous-time stochastic games model checking
• Performance measure sensitive congruences for Markovian process algebras
• Twenty years of rewriting logic
• Model checking conditional CSL for continuous-time Markov chains
• Bio-PEPA: A framework for the modelling and analysis of biological systems
• Comparative branching-time semantics for Markov chains
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• Model checking open systems with alternating projection temporal logic
• Formal reasoning about finite-state discrete-time Markov chains in HOL
• Model checking expected time and expected reward formulae with random time bounds
• Statistical probabilistic model checking with a focus on time-bounded properties
• A theory of stochastic systems. I: Stochastic automata
• Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system
• Efficient decomposition algorithm for stationary analysis of complex stochastic Petri net models
• On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Automata-based CSL model checking
• Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata
• scientific article; zbMATH DE number 1884410 (Why is no real title available?)
• Central limit model checking
• Verification, Model Checking, and Abstract Interpretation
• Process algebra for performance evaluation
• Formal modelling and verification of probabilistic resource bounded agents
• Checking continuous stochastic logic against quantum continuous-time Markov chains
• Learning algorithms for verification of Markov decision processes
• A sample-driven solving procedure for the repeated reachability of quantum continuous-time Markov chains
• Quantitative analysis with the probabilistic model checker PRISM
• Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games
• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• Multiphase until formulas over Markov reward models: an algebraic approach
• Performability assessment by model checking of Markov reward models
• Mixing logics and rewards for the component-oriented specification of performance measures
• Model checking mobile stochastic logic

This page was built for publication: Approximate symbolic model checking of continuous-time Markov chains

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