Change search
CiteExportLink to record
Permanent link

Direct link
A logic for reasoning about time and reliability
Number of Authors: 2
1990 (English)Report (Refereed)
Abstract [en]

We present a logic for stating properties such as, "after a request for service there is at least a 98\045 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 satis- fies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and\003This research report is a revised and extended version of a paper that has appeared under the title "A Framework for Reasoning about Time and Reliability" in the Proceeding of the 10thIEEE Real-time Systems Symposium, Santa Monica CA, December 1989. This work was partially supported by the Swedish Board for Technical Development (STU) as part of Esprit BRA Project SPEC, and by the Swedish Telecommunication Administration.1the Markov chain. A simple example is included to illustrate the algorithms.

Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1990, 1. , 35 p.
SICS Research Report, ISSN 0283-3638 ; R90:13
Keyword [en]
Branching time temporal logic, Markov chains, Model checking, Real-time, Reliability
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-21343OAI: diva2:1041377
Original report number R90013.Available from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(296 kB)16 downloads
File information
File name FULLTEXT01.pdfFile size 296 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 16 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

CiteExportLink to record
Permanent link

Direct link