{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:16Z","timestamp":1725489316491},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442400"},{"type":"electronic","value":"9783540457930"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45793-3_21","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:03:26Z","timestamp":1187251406000},"page":"306-321","source":"Crossref","is-referenced-by-count":9,"title":["A Logic of Probability with Decidable Model-Checking"],"prefix":"10.1007","author":[{"given":"Dani\u00e8le","family":"Beauquier","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Rabinovich","sequence":"additional","affiliation":[]},{"given":"Anatol","family":"Slissenko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1049","volume":"112","author":"M. Abadi","year":"1994","unstructured":"M. Abadi and J. Halpern. Decidability and expressiveness for first-order logic of probability. Information and Computation, 112(1):1\u201336, 1994.","journal-title":"Information and Computation"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In Computer Aided Verification. Proceeding of CAV\u201995, pages 155\u2013165. Springer Verlag, 1995. Lect. Notes in Comput. Sci., vol. 939.","DOI":"10.1007\/3-540-60045-0_48"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"J. R. B\u00fcchi. Weak second-order arithmetic and finite automata. Z. Math. Logik u. Grundlag. Math., (6):66\u201392, 1960.","DOI":"10.1002\/malq.19600060105"},{"key":"21_CR4","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. Journal of the ACM, 42:857\u2013907, 1995.","journal-title":"Journal of the ACM"},{"issue":"2","key":"21_CR5","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1145\/174652.174658","volume":"41","author":"R. Fagin","year":"1994","unstructured":"R. Fagin and J. Halpern. Reasoning about knowledge and probability. J. of the Assoc. Comput. Mach., 41(2):340\u2013367, 1994.","journal-title":"J. of the Assoc. Comput. Mach."},{"issue":"1","key":"21_CR6","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/0890-5401(90)90060-U","volume":"87","author":"R. Fagin","year":"1990","unstructured":"R. Fagin, J.Y. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Information and Computation, 87:1,2:78\u2013128, 1990.","journal-title":"Information and Computation"},{"key":"21_CR7","volume-title":"The Theory of Matrices","author":"F. R. F. R. Gantmakher","year":"1977","unstructured":"F. R. (Feliks Ruvimovich) Gantmakher. The Theory of Matrices. Chelsea Pub. Co., New York, 1977."},{"key":"21_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013976","volume-title":"Temporal Logic","author":"D. Gabbay","year":"1994","unstructured":"D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic. Clarendon Press, Oxford, 1994."},{"key":"21_CR9","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0004-3702(90)90019-V","volume":"46","author":"J. Halpern","year":"1990","unstructured":"J. Halpern. An analysis of first-order logics of probability. Artificial Intelligence, 46:311\u2013350, 1990.","journal-title":"Artificial Intelligence"},{"key":"21_CR10","unstructured":"H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994. Series: \u201cReal Time Safety Critical System\u201d, vol. 1."},{"issue":"5","key":"21_CR11","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. A. Hansson","year":"1994","unstructured":"H. A. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"21_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"W. A. Hodges","year":"1993","unstructured":"W. A. Hodges. Model Theory. Cambridge University Press, Cambridge, 1993."},{"key":"21_CR13","volume-title":"Finite Markov Chains","author":"J. G. Kemeny","year":"1960","unstructured":"J. G. Kemeny and J. L. Snell. Finite Markov Chains. D Van Nostad Co., Inc., Princeton, N.J., 1960."},{"key":"21_CR14","volume-title":"Denumerable Markov Chains","author":"J. G. Kemeny","year":"1966","unstructured":"J. G. Kemeny, J. L. Snell, and A.W. Knapp. Denumerable Markov Chains. D Van Nostad Co., Inc., Princeton, N. J., 1966."},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"H. J. Keisler. Probability quantifiers. In J. Barwise and S. S.Feferman, editors, Model Theoretic Logics, pages 509\u2013556. Springer, 1985.","DOI":"10.1017\/9781316717158.021"},{"issue":"3","key":"21_CR16","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D. Lehmann","year":"1982","unstructured":"D. Lehmann and S. Shelah. Reasoning about time and chance. Information and Control, 53(3):165\u2013198, 1982.","journal-title":"Information and Control"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 131\u2013191. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45793-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T00:33:56Z","timestamp":1556757236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45793-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442400","9783540457930"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45793-3_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}