Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
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...
Glavni autori: | , , , |
---|---|
Format: | Članak |
Jezik: | English |
Izdano: |
Logical Methods in Computer Science e.V.
2011-03-01
|
Serija: | Logical Methods in Computer Science |
Teme: | |
Online pristup: | https://lmcs.episciences.org/697/pdf |