In this paper we present a methodology for the verification of performance and reliability properties of discrete real-time systems. The methodology relies on a temporal logic that can express bounds on the probability of events and on the average time between them. The semantics both probabilistic and nondeterministic behavior. We present model-checking algorithms for the algorithmic verification of the specifications, and we discuss their complexity.
展开▼
