Search

• < Previous
• 1
• Next >

---

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

Taolue Chen ; Tingting Han ; Joost-Pieter Katoen ; Alexandru Mereacre.

We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C&nbsp;[&hellip;]

---

On the Axiomatizability of Impossible Futures

Taolue Chen ; Wan Fokkink ; Rob van Glabbeek.

A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as&nbsp;[&hellip;]

---