A logic for reasoning about time and reliability
- 1 September 1994
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 6 (5) , 512-535
- https://doi.org/10.1007/bf01211866
Abstract
We present a logic for stating properties such as, “after a request for service there is at least a 98% probability that the service will be carried out within 2 seconds”. The logic extends the temporal logic CTL by Emerson, Clarke and Sistla with time and probabilities. Formulas are interpreted over discrete time Markov chains. We give algorithms for checking that a given Markov chain satisfies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and the Markov chain. A simple example is included to illustrate the algorithms.Keywords
This publication has 43 references indexed in Scilit:
- Real-time and the Mu-Calculus (preliminary report)Published by Springer Nature ,1992
- Logics and models of real time: A surveyPublished by Springer Nature ,1992
- Verifying automata specifications of probabilistic real-time systemsPublished by Springer Nature ,1992
- Time-dependent distributed systems: proving safety, liveness and real-time propertiesDistributed Computing, 1987
- Verification of multiprocess probabilistic protocolsDistributed Computing, 1986
- Termination of Probabilistic Concurrent ProgramACM Transactions on Programming Languages and Systems, 1983
- Using branching time temporal logic to synthesize synchronization skeletonsScience of Computer Programming, 1982
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982
- Proving real-time properties of programs with temporal logicACM SIGOPS Operating Systems Review, 1981
- A note on reliable full-duplex transmission over half-duplex linksCommunications of the ACM, 1969