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