{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T03:28:05Z","timestamp":1792726085529,"version":"4.5.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1994,9,1]],"date-time":"1994-09-01T00:00:00Z","timestamp":778377600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1994,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present a logic for stating properties such as, \u201cafter a request for service there is at least a 98% probability that the service will be carried out within 2 seconds\u201d. 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.<\/jats:p>","DOI":"10.1007\/bf01211866","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T08:30:42Z","timestamp":1109320242000},"page":"512-535","source":"Crossref","is-referenced-by-count":1037,"title":["A logic for reasoning about time and reliability"],"prefix":"10.1145","volume":"6","author":[{"given":"Hans","family":"Hansson","sequence":"first","affiliation":[{"name":"Department of Computer Systems, Uppsala University, Box 325, S-751 05, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[{"name":"Department of Computer Systems, Uppsala University, Box 325, S-751 05, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Ajmone Marsan M. Balbo G. and Conte G.: Performance Models of Multiprocessor Systems . MIT Press 1986.","DOI":"10.1007\/978-94-009-5408-3_2"},{"key":"e_1_2_1_2_2_2","unstructured":"Abrahamson K.: Decidability and Expressiveness of Logics of Processes . PhD thesis Univ. of Washington 1980."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Alur R. Courcoubetis C. and Dill D.: Model-checking for real-time systems. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science pages 414\u2013425 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Alur R. Courcoubetis C. and Dill D.: Model-checking for probabilistic real-time systems. In Proc. 18 th Int. Coll. on Automata Languages and Programming (ICALP) volume 510 of Lecture Notes in Computer Science pages 115\u2013126. Springer Verlag 1991.","DOI":"10.1007\/3-540-54233-7_128"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Alur R. Courcoubetis C. and Dill D.: Verifying Automata Specifications of Probabilistic Real-Time Systems. In J. de Bakker C. Huizing W.-P. de Roever and G. Rozenberg editors Real-Time: Theory in Practice volume 600 of Lecture Notes in Computer Science pages 28\u201344. Springer Verlag 1992.","DOI":"10.1007\/BFb0031986"},{"key":"e_1_2_1_2_6_2","unstructured":"Alur R. and Dill D.: Automata for modeling real-time systems. In Proc. 17 th Int. Coll. on Automata Languages and Programming (ICALP) volume 443 of Lecture Notes in Computer Science Springer Verlag 1990."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Alur R. and Henzinger T.: A really temporal logic. In Proc. 30 th IEEE Annual Symp. Foundations of Computer Science pages 164\u2013169 1989.","DOI":"10.1109\/SFCS.1989.63473"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Alur R. and Henzinger T.: Logics and Models of Real Time: A Survey. In J. de Bakker C. Huizing W.-P. de Roever and G. Rozenberg editors Real-Time: Theory in Practice volume 600 of Lecture Notes in Computer Science pages 28\u201344. Springer Verlag 1992.","DOI":"10.1007\/BFb0031988"},{"key":"e_1_2_1_2_9_2","unstructured":"Aho A.V. Hopcroft J.E. and Ullman J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley Publishing Company 1974."},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bernstein A. and Harter P.K.: Proving real-time properties of programs with temporal logic. In Proc. 8 th ACM Symp. on Operating System Principles pages 1\u201311 Pacific Grove California 1981.","DOI":"10.1145\/1067627.806585"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/362946.362970"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Christoff L. and Christoff I: Reasoning about safety and liveness properties for probabilistic processes. In R. Shyamasundar editor Proc. 12 th Conf. on Foundations of Software Technology and Theoretical Computer Science volume 652 of Lecture Notes in Computer Science pages 342\u2013355. Springer-Verlag 1992.","DOI":"10.1007\/3-540-56287-7_117"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_2_14_2","unstructured":"Chiola G.: A software package for the analysis of generalized stochastic Petri net models. In Proc. Int. Workshop on Time Petri Nets pages 136\u2013143 July 1985."},{"key":"e_1_2_1_2_15_2","volume-title":"Spnp: Stochastic petri net package","author":"Ciardo G.","year":"1989"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Courcoubetis C. Vardi M. and Wolper P.: Reasoning about fair concurrent programs. In Proc. 18 th ACM Symp. on Theory of Computing pages 283\u2013294 1986.","DOI":"10.1145\/12130.12159"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Courcoubetis C. and Yannakakis C.: The complexity of probabilistic verification. In Proc. 29 th IEEE Annual Symp. Foundations of Computer Science pages 338\u2013345 1988.","DOI":"10.1109\/SFCS.1988.21950"},{"key":"e_1_2_1_2_18_2","unstructured":"Courcoubetis C. and Yannakakis C.: The complexity of probabilistic verification. Bell labs Murry Hill 1989."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"de Bakker J. Huizing C. de Roever W-.P. and Rozenberg G.: editors. Real-Time: Theory in Practice volume 600 of Lecture Notes in Computer Science . Springer Verlag 1992.","DOI":"10.1007\/BFb0031984"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Emerson A.: Real-Time and the Mu-Calculus. In J. de Bakker C. Huizing W-.P. de Roever and G. Rozenberg editors Real-Time: Theory in Practice volume 600 of Lecture Notes in Computer Science pages 176\u2013194. Springer Verlag 1992.","DOI":"10.1007\/BFb0031992"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00355298"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Feldman Y.A.: A decidable propositional probabilistic dynamic logic. In Proc. 15 th ACM Symp. on Theory of Computing pages 298\u2013309 Boston 1983.","DOI":"10.1145\/800061.808759"},{"key":"e_1_2_1_2_24_2","unstructured":"Gibbons A.: Algorithmic Graph Theory . Cambridge University Press 1985."},{"key":"e_1_2_1_2_25_2","unstructured":"Hansson H.: Time and Probabilities in Formal Design of Distributed Systems . PhD thesis Department of Computer Systems Uppsala University 1991. Available as report DoCS 91\/27 Department of Computer Systems Uppsala University Sweden and as report 05 in SICS dissertation series SICS Kista Sweden. A revised version of the thesis will appear in the Elsevier book series Real-Time Safety Critical Systems."},{"key":"e_1_2_1_2_26_2","first-page":"278","volume-title":"A calculus for communicating systems with time and probabilities","author":"Hansson H.","year":"1990"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hooman J.: Specification and Compositional Verification of Real-Time Systems volume 558 of Lecture Notes in Computer Science . North-Holland 1991.","DOI":"10.1007\/3-540-54947-1"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Hart S. and Sharir M.: Probabilistic temporal logics for finite and bounded models. In Proc. 16 th ACM Symp. on Theory of Computing pages 1\u201313 1984.","DOI":"10.1145\/800057.808660"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357214"},{"key":"e_1_2_1_2_30_2","unstructured":"Holliday M.A. and Vernon M.K.: The GTPN Analyzer: numerical methods and user interface. Technical Report 639 Dept. of Computer Science Univ. of Wisconsin \u2014 Madison Apr. 1986."},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.5009450"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Holliday M.A. and Vernon M.K.: A generalized timed Petri net model for performance analysis. IEEE Trans. on Software Engineering SE-13(12) 1987.","DOI":"10.1109\/TSE.1987.233141"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/12868.12870"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.5009519"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Joseph M.: editor. Formal Techniques in Real-Time and Fault-Tolerant Systems volume 331 of Lecture Notes in Computer Science . Springer Verlag 1988.","DOI":"10.1007\/3-540-50302-1"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Koymans R. Vytopil J. and de Roever W.P.: Real-time programming and asynchronous message passing. In Proc. 2 nd ACM Symp. on Principles of Distributed Computing pages 187\u2013197 Montr\u00e9al Canada 1983.","DOI":"10.1145\/800221.806721"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91022-1"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Larsen K.G. and Skou A.: Bisimulation through probabilistic testing. In Proc. 16 th ACM Symp. on Principles of Programming Languages pages 344\u2013352 1989.","DOI":"10.1145\/75277.75307"},{"key":"e_1_2_1_2_39_2","unstructured":"Milner R.: Communication and Concurrency . Prentice-Hall 1989."},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676110"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Ostroff J.: Automatic verification of timed transition models. In Sifakis editor Workshop on automatic verification methods for finite state systems volume 407 of Lecture Notes in Computer Science pages 247\u2013256. Springer Verlag 1989.","DOI":"10.1007\/3-540-52148-8_20"},{"key":"e_1_2_1_2_43_2","unstructured":"Ostroff J. and Wonham W.: Modelling specifying and verifying real-time embedded computer systems. In Proc. IEEE Real-time Systems Symp. pages 124\u2013132 Dec. 1987."},{"key":"e_1_2_1_2_44_2","volume-title":"PhD thesis","author":"Parrow J.","year":"1985"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Pnueli A. and Harel E.: Applications of temporal logic to the specification of real-time systems. In M. Joseph editor Proc. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems volume 331 of Lecture Notes in Computer Science pages 84\u201398. Springer Verlag 1988.","DOI":"10.1007\/3-540-50302-1_4"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01843570"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Razouk R.R.: The derivation of performance expressions for communication protocols from timed Petri net models. In Proc. ACM SIGCOMM '84 pages 210\u2013217 Montr\u00e9al Qu\u00e9bec 1984.","DOI":"10.1145\/800056.802080"},{"key":"e_1_2_1_2_49_2","unstructured":"Razouk R.R. and Phelps C.V.: Performance analysis of timed Petri net models. In Proc. IFIP WG 6.2 Symp. on Protocol Specification Testing and Verification IV pages 126\u2013129. North-Holland June 1984."},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01667079"},{"key":"e_1_2_1_2_51_2","unstructured":"Sanders W.H. and Meyer J.F.: Metasan: a performability evaluation tool based on stochastic activity networks. In Proc of the ACM-IEEE Comp. Soc. Fall Joint Conf. IEEE Computer Society Press November 1986."},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Vardi M: Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26 th IEEE Annual Symp. Foundations of Computer Science pages 327\u2013337 1985.","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Vernon M.K. and Holliday M.A.: Performance analysis of multiprocessor cache consistency protocols using generalized timed Petri nets. In Proc. of Performance 86 and ACM SIGMETRICS 1986 Joint conf. on Computer Performance Modelling Measurement and Evaluation pages 9\u201317. ACM press May 1986.","DOI":"10.1145\/317499.317534"},{"key":"e_1_2_1_2_54_2","unstructured":"Vardi M.Y. and Wolper P.: An automata-theoretic approach to automatic program verification. In Proc. IEEE Symp. on Logic in Computer Science pages 332\u2013344 June 1986."},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Vytopil P.: editor. Formal Techniques in Real-Time and Fault-Tolerant Systems volume 571 of Lecture Notes in Computer Science. Springer Verlag 1991.","DOI":"10.1007\/3-540-55092-5"},{"key":"e_1_2_1_2_56_2","first-page":"272","volume-title":"Performance evaluation using extended timed Petri nets","author":"Zuberek W.","year":"1985"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211866.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211866\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211866","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,23]],"date-time":"2024-12-23T17:30:26Z","timestamp":1734975026000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211866"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,9]]},"references-count":56,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1994,9]]}},"alternative-id":["10.1007\/BF01211866"],"URL":"https:\/\/doi.org\/10.1007\/bf01211866","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,9]]}}}