A logic for reasoning about time and reliability. Hansson, H. & Jonsson, B. Formal Aspects of Computing, 6(5):512–535, September, 1994.
A logic for reasoning about time and reliability [link]Paper  doi  abstract   bibtex   
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.
@article{hansson_logic_1994,
	title = {A logic for reasoning about time and reliability},
	volume = {6},
	issn = {1433-299X},
	url = {https://doi.org/10.1007/BF01211866},
	doi = {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.},
	language = {en},
	number = {5},
	urldate = {2018-10-24},
	journal = {Formal Aspects of Computing},
	author = {Hansson, Hans and Jonsson, Bengt},
	month = sep,
	year = {1994},
	keywords = {Automatic verification, CTL, Markov chains, Modal logic, Model checking, Probability, Real time, Soft deadlines},
	pages = {512--535}
}

Downloads: 0