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]](https://bibbase.org/img/filetypes/link.svg "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
{"_id":"rx8xHnThvAttRkbb8","bibbaseid":"hansson-jonsson-alogicforreasoningabouttimeandreliability-1994","downloads":0,"creationDate":"2016-07-28T14:19:17.028Z","title":"A logic for reasoning about time and reliability","author_short":["Hansson, H.","Jonsson, B."],"year":1994,"bibtype":"article","biburl":"https://bibbase.org/zotero/tillhofmann","bibdata":{"bibtype":"article","type":"article","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":[{"propositions":[],"lastnames":["Hansson"],"firstnames":["Hans"],"suffixes":[]},{"propositions":[],"lastnames":["Jonsson"],"firstnames":["Bengt"],"suffixes":[]}],"month":"September","year":"1994","keywords":"Automatic verification, CTL, Markov chains, Modal logic, Model checking, Probability, Real time, Soft deadlines","pages":"512–535","bibtex":"@article{hansson_logic_1994,\n\ttitle = {A logic for reasoning about time and reliability},\n\tvolume = {6},\n\tissn = {1433-299X},\n\turl = {https://doi.org/10.1007/BF01211866},\n\tdoi = {10.1007/BF01211866},\n\tabstract = {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.},\n\tlanguage = {en},\n\tnumber = {5},\n\turldate = {2018-10-24},\n\tjournal = {Formal Aspects of Computing},\n\tauthor = {Hansson, Hans and Jonsson, Bengt},\n\tmonth = sep,\n\tyear = {1994},\n\tkeywords = {Automatic verification, CTL, Markov chains, Modal logic, Model checking, Probability, Real time, Soft deadlines},\n\tpages = {512--535}\n}\n\n","author_short":["Hansson, H.","Jonsson, B."],"key":"hansson_logic_1994","id":"hansson_logic_1994","bibbaseid":"hansson-jonsson-alogicforreasoningabouttimeandreliability-1994","role":"author","urls":{"Paper":"https://doi.org/10.1007/BF01211866"},"keyword":["Automatic verification","CTL","Markov chains","Modal logic","Model checking","Probability","Real time","Soft deadlines"],"downloads":0},"search_terms":["logic","reasoning","time","reliability","hansson","jonsson"],"keywords":["markov chains; modal logic; ctl; real time; probability; soft deadlines; automatic verification; model checking","automatic verification","ctl","markov chains","modal logic","model checking","probability","real time","soft deadlines"],"authorIDs":[],"dataSources":["9pYjFWPBodPyDyb7N"]}