Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata

DOI10.1145/2461328.2461376MaRDI QIDQ2986937zbMATH OpenOpenAlexFDO

Authors Hongfei Fu

Publication date 16 May 2017

Published in Proceedings of the 16th international conference on Hybrid systems: computation and control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.4787

zbMATH Keywords

continuous-time Markov chainsdeterministic timed automatamodel checking

Mathematics Subject Classification ID

Applications of continuous-time Markov processes on discrete state spaces (60J28) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We consider the problem of approximating the probability mass of the set of timed paths under a continuous-time Markov chain (CTMC) that are accepted by a deterministic timed automaton (DTA). As opposed to several existing works on this topic, we consider DTA with multiple clocks. Our key contribution is an algorithm to approximate these probabilities using finite difference methods. An error bound is provided which indicates the approximation error. The stepping stones towards this result include rigorous proofs for the measurability of the set of accepted paths and the integral-equation system characterizing the acceptance probability, and a differential characterization for the acceptance probability.

Recommendations

• Monitoring CTMCs by multi-clock timed automata
• Time-Bounded Verification of CTMCs against Real-Time Specifications
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Observing continuous-time MDPs by 1-clock timed automata

Cites work

• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A note on two problems in connexion with graphs
• Controlling a Class of Nonlinear Systems on Rectangles
• Diagnostic Information for Realizability
• Enhancing model checking in verification by AI techniques
• scientific article; zbMATH DE number 5595151 (Why is no real title available?)
• scientific article; zbMATH DE number 2080065 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Markov decision processes and regular events
• Model repair for probabilistic systems
• Receding horizon control for temporal logic specifications

Cited in

(4)

• On-the-fly verification and optimization of DTA-properties for large Markov chains
• Fluid model checking of timed properties
• Monitoring CTMCs by multi-clock timed automata
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

This page was built for publication: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata

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