BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-96-1571
       ENTRY:: June 10, 1996
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Formal Verification of Performance and Reliability of
               Real-Time Systems
        TYPE:: Technical Report
      AUTHOR:: DeAlfaro, Luca
        DATE:: June 1996
       PAGES:: 24
    ABSTRACT:: In this paper we propose a methodology for the specification
               and verification of performance and reliability properties of
               real-time systems within the framework of temporal logic. The
               methodology is based on the system model of stochastic
               real-time systems (SRTSs), and on branching-time temporal
               logics that are extensions of the probabilistic logics pCTL
               and pCTL*. SRTSs are discrete-time transition systems that
               can model both probabilistic and nondeterministic behavior.
               The specification language extends the branching-time logics
               pCTL and pCTL* by introducing an operator to express bounds
               on the average time between events. We present model-checking
               algorithms for the algorithmic verification of system
               specifications, and we discuss their complexity.
       NOTES:: [Adminitrivia V1/Prg/19960610]
         END:: STAN//CS-TR-96-1571