English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We study the verification of a finite continuous-time Markov chain (CTMC) Cagainst a linear real-time specification given as a deterministic timedautomaton (DTA) A with finite or Muller acceptance conditions. The centralquestion that we address is: what is the probability of the set of paths of Cthat are accepted by A, i.e., the likelihood that C satisfies A? It is shownthat under finite acceptance criteria this equals the reachability probabilityin a finite piecewise deterministic Markov process (PDP), whereas for Mulleracceptance criteria it coincides with the reachability probability of terminalstrongly connected components in such a PDP. Qualitative verification is shownto amount to a graph analysis of the PDP. Reachability probabilities in ourPDPs are then characterized as the least solution of a system of Volterraintegral equations of the second type and are shown to be approximated by thesolution of a system of partial differential equations. For single-clock DTA,this integral equation system can be transformed into a system of linearequations where the coefficients are solutions of ordinary differentialequations. As the coefficients are in fact transient probabilities in CTMCs,this result implies that standard algorithms for CTMC analysis suffice toverify single-clock DTA specifications.

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications