{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T16:06:15Z","timestamp":1732032375765},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_16","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"265-276","source":"Crossref","is-referenced-by-count":41,"title":["Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach"],"prefix":"10.1007","author":[{"given":"Moshe Y.","family":"Vardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"C. Baier and M.Z. Kwiatowska. Automatic verification of liveness properties of randomized systems. In ACMSymp. on Principles of Distributed Systems (PODC), 1997.","DOI":"10.1145\/259380.259527"},{"key":"16_CR2","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1\u201312, Stanford, 1962. Stanford University Press."},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Computer Aided Verification, Proc. 6th Int. Conference","author":"O. Bernholtz","year":"1994","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In D. L. Dill, editor, Computer Aided Verification, Proc. 6th Int. Conference, volume 818 of Lecture Notes in Computer Science, pages 142\u2013155, Stanford, June 1994. Springer-Verlag, Berlin."},{"key":"16_CR4","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Proc. Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52\u201371. Springer-Verlag, 1981."},{"issue":"2","key":"16_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model-checking algorithms. In Proc. 6th ACM Symposium on Principles of Distributed Computing, pages 294\u2013303, Vancouver, British Columbia, August 1987.","DOI":"10.1145\/41840.41865"},{"key":"16_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"Decade of Concurrency \u2014 Reflections and Perspectives (Proceedings of REX School)","author":"E.M. Clarke","year":"1993","unstructured":"E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Decade of Concurrency \u2014 Reflections and Perspectives (Proceedings of REX School), volume 803 of Lecture Notes in Computer Science, pages 124\u2013175. Springer-Verlag, 1993."},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Y. Choueka. Theories of automata on \u03c9-tapes: A simplified approach. Journal of Computer and System Sciences, 8:117\u2013141, 1974.","journal-title":"Journal of Computer and System Sciences"},{"key":"16_CR9","unstructured":"T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press, 1990."},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/BFb0032043","volume-title":"Proc. 17th Int. Coll. on Automata Languages and Programming","author":"C. Courcoubetis","year":"1990","unstructured":"C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events. In Proc. 17th Int. Coll. on Automata Languages and Programming, volume 443, pages 336\u2013349, Coventry, July 1990. Lecture Notes in Computer Science, Springer-Verlag."},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM, 42:857\u2013907, 1995.","journal-title":"J. ACM"},{"key":"16_CR13","volume-title":"Finite-State Markovian Decision Processes","author":"C. Derman","year":"1970","unstructured":"C. Derman. Finite-State Markovian Decision Processes. Academic Press, New York, 1970."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. Tree automata, Mu-calculus and determinacy. In Proc. 32nd IEEE Symposium on Foundations of Computer Science, pages 368\u2013377, San Juan, October 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"16_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-15648-8_7","volume-title":"Proc. Workshop on Logic of Programs","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson. Automata, tableaux, and temporal logics. In Proc. Workshop on Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79\u201387. Springer-Verlag, 1985."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"N. Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proc. 7th ACM Symposium on Principles of Programming Languages, pages 163\u2013173, January 1980.","DOI":"10.1145\/567446.567462"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6:512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"D. Harel and A. Pnueli. On the development of reactive systems. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 477\u2013498. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S. Hart","year":"1983","unstructured":"S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. ACM Trans. on Programming Languages, 5:356\u2013380, 1983.","journal-title":"ACM Trans. on Programming Languages"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"N. Klarlund. Progress measures for complementation of \u03c9-automata with applications to temporal logic. In Proc. 32nd IEEE Symposium on Foundations of Computer Science, pages 358\u2013367, San Juan, October 1991.","DOI":"10.1109\/SFCS.1991.185391"},{"key":"16_CR22","volume-title":"Finite Markov Chains","author":"J.G. Kemeny","year":"1960","unstructured":"J.G. Kemeny and J.L. Snell. Finite Markov Chains. Van Nostrad, Princeton, 1960."},{"key":"16_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J.G. Kemeny","year":"1976","unstructured":"J.G. Kemeny, J.L. Snell, and A.W. Knapp. Denumerable Markov Chains. Springer-Verlag, New York, 1976."},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"16_CR25","unstructured":"O. Kupferman and M.Y. Vardi. Synthesis with incomplete informatio. In 2nd International Conference on Temporal Logic, pages 91\u2013106, Manchester, July 1997. Kluwer Academic Publishers."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. In Proc. 5th Israeli Symposium on Theory of Computing and Systems, pages 147\u2013158. IEEE Computer Society Press, 1997.","DOI":"10.1109\/ISTCS.1997.595167"},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0065-2458(08)60533-1","volume":"29","author":"M.T. Liu","year":"1989","unstructured":"M.T. Liu. Protocol engineering. Advances in Computing, 29:79\u2013195, 1989.","journal-title":"Advances in Computing"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New Orleans, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"D. Lehman and M. O. Rabin. On the advantage of free choice: A fully symmetric and fully distributed solution to the dining philosophers problem. In Proc. 8th ACM Symposium on Principles of Programming Languages, pages 133\u2013138, 1981.","DOI":"10.1145\/567532.567547"},{"key":"16_CR30","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"R. McNaughton","year":"1966","unstructured":"R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521\u2013530, 1966.","journal-title":"Information and Control"},{"key":"16_CR31","volume-title":"Complementation is more difficult with automata on infinite words","author":"M. Michel","year":"1988","unstructured":"M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988."},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR33","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"16_CR34","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th International Symp. on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, volume 137, pages 337\u2013351. Springer-Verlag, Lecture Notes in Computer Science, 1981."},{"key":"16_CR35","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1146\/annurev.cs.02.060187.001451","volume":"2","author":"H. Rudin","year":"1987","unstructured":"H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291\u2013316, 1987.","journal-title":"Annual Review of Computer Science"},{"key":"16_CR36","volume-title":"Complexity of automata on infinite objects","author":"S. Safra","year":"1989","unstructured":"S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1989."},{"key":"16_CR37","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"S. Safra and M.Y. Vardi. On \u03c9-automata and temporal logic. In Proc. 21st ACM Symposium on Theory of Computing, pages 127\u2013137, Seattle, May 1989.","DOI":"10.1145\/73007.73019"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 165\u2013191, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26th IEEE Symp. on Foundations of Computer Science, pages 327\u2013338, Portland, October 1985.","DOI":"10.1109\/SFCS.1985.12"},{"key":"16_CR41","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today-Recent Trends and Developments","author":"M.Y. Vardi","year":"1995","unstructured":"M.Y. Vardi. Alternating automata and program verification. In Computer Science Today-Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 471\u2013485. Springer-Verlag, Berlin, 1995."},{"key":"16_CR42","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of Lecture Notes in Computer Science, pages 238\u2013266. Springer-Verlag, Berlin, 1996."},{"key":"16_CR43","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First Symposium on Logic in Computer Science, pages 322\u2013331, Cambridge, June 1986."},{"issue":"1","key":"16_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"issue":"1\u20132","key":"16_CR45","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal logic can be more expressive. Information and Control, 56(1\u20132):72\u201399, 1983.","journal-title":"Information and Control"},{"key":"16_CR46","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-51803-7_23","volume-title":"Proc. Temporal Logic in Specification","author":"P. Wolper","year":"1989","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75\u2013123. Lecture Notes in Computer Science, Springer-Verlag, 1989."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T16:34:53Z","timestamp":1556382893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}