Approximating Acceptance Probabilities of CTMC-Paths on Multi-Clock Deterministic Timed Automata

TL;DR

This paper presents an algorithm to approximate the probability of CTMC paths accepted by multi-clock deterministic timed automata, extending previous work to more complex automata with multiple clocks.

Contribution

The paper introduces a novel finite difference method-based algorithm with error bounds for approximating acceptance probabilities in multi-clock DTA.

Findings

Algorithm provides accurate probability approximations

Error bounds ensure reliability of the approximation

Extends previous single-clock approaches to multi-clock automata

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.