Time−Bounded Verification of CTMCs Against Real−Time Specifications
Abstract. In this paper we study time-bounded verification of a finite continuous-timeMarkov chain (CTMC) C against a real-time specification, provided either as a metric temporal logic (MTL) property 'φ', or as a timed automaton (TA) A. The key question is: what is the probability of the...
প্রধান লেখক: | Chen, T, Diciolla, M, Kwiatkowska, M, Mereacre, A |
---|---|
বিন্যাস: | Conference item |
প্রকাশিত: |
Springer
2011
|
অনুরূপ উপাদানগুলি
অনুরূপ উপাদানগুলি
-
Verification of Linear Duration Properties over Continuous−Time Markov Chains
অনুযায়ী: Chen, T, অন্যান্য
প্রকাশিত: (2012) -
Verification of Linear Duration Properties over Continuous Time Markov Chains
অনুযায়ী: Chen, T, অন্যান্য
প্রকাশিত: (2012) -
Quantitative Verification of Implantable Cardiac Pacemakers
অনুযায়ী: Chen, T, অন্যান্য
প্রকাশিত: (2015) -
A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers
অনুযায়ী: Chen, T, অন্যান্য
প্রকাশিত: (2013) -
Synthesising Optimal Timing Delays for Timed I/O Automata
অনুযায়ী: Diciolla, M, অন্যান্য
প্রকাশিত: (2014)