{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:26:47Z","timestamp":1725496007403},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540770497"},{"type":"electronic","value":"9783540770503"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-77050-3_44","type":"book-chapter","created":{"date-parts":[[2007,11,26]],"date-time":"2007-11-26T08:39:22Z","timestamp":1196066362000},"page":"532-543","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Schmalz","sequence":"first","affiliation":[]},{"given":"Hagen","family":"V\u00f6lzer","sequence":"additional","affiliation":[]},{"given":"Daniele","family":"Varacca","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"44_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-60045-0_49","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1995","unstructured":"Alur, R., Henzinger, T.A.: Local liveness for compositional modeling of fair reactive systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 166\u2013179. Springer, Heidelberg (1995)"},{"key":"44_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-39813-4_16","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Berwanger","year":"2003","unstructured":"Berwanger, D., Gr\u00e4del, E., Kreutzer, S.: Once upon a time in the west - determinacy, definability, and complexity of path games. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 229\u2013243. Springer, Heidelberg (2003)"},{"issue":"4","key":"44_CR3","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"issue":"16","key":"44_CR4","first-page":"995","volume":"B","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. Handbook of Theoretical Computer Science\u00a0B(16), 995\u20131072 (1990)","journal-title":"Handbook of Theoretical Computer Science"},{"issue":"3","key":"44_CR5","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program.\u00a08(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"44_CR6","first-page":"97","volume-title":"POPL","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97\u2013107. ACM Press, New York (1985)"},{"key":"44_CR7","unstructured":"Schmalz, M.: Extensions of an algorithm for generalised fair model checking. Diploma Thesis, Technical Report B 07-01, University of L\u00fcbeck, Germany (2007), \n                    \n                      http:\/\/www.tcs.uni-luebeck.de\/Forschung\/B0701.pdf"},{"key":"44_CR8","doi-asserted-by":"crossref","unstructured":"Schmalz, M., V\u00f6lzer, H., Varacca, D.: Model checking almost all paths can be less expensive than checking all paths. Technical Report 573, ETH Z\u00fcrich, Switzerland (2007), \n                    \n                      http:\/\/www.inf.ethz.ch\/research\/disstechreps\/techreports","DOI":"10.1007\/978-3-540-77050-3_44"},{"key":"44_CR9","unstructured":"Schnoebelen, P.: The complexity of temporal logic model checking. In: AiML, pp. 393\u2013436. King\u2019s College Publications (2002)"},{"issue":"3","key":"44_CR10","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"44_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/BFb0015772","volume-title":"Automata, Languages and Programming","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. In: Brauer, W. (ed.) Automata, Languages and Programming. LNCS, vol.\u00a0194, pp. 465\u2013474. Springer, Heidelberg (1985)"},{"key":"44_CR12","first-page":"389","volume-title":"LICS","author":"D. Varacca","year":"2006","unstructured":"Varacca, D., V\u00f6lzer, H.: Temporal logics and model checking for fairly correct systems. In: LICS, pp. 389\u2013398. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"44_CR13","first-page":"327","volume-title":"FOCS","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338. IEEE Computer Society Press, Los Alamitos (1985)"},{"key":"44_CR14","first-page":"332","volume-title":"LICS","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332\u2013344. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"44_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1007\/11539452_35","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"H. V\u00f6lzer","year":"2005","unstructured":"V\u00f6lzer, H., Varacca, D., Kindler, E.: Defining fairness. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 458\u2013472. Springer, Heidelberg (2005)"},{"key":"44_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-47813-2_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L.D. Zuck","year":"2002","unstructured":"Zuck, L.D., Pnueli, A., Kesten, Y.: Automatic verification of probabilistic free choice. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 208\u2013224. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77050-3_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:12:24Z","timestamp":1558278744000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77050-3_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540770497","9783540770503"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77050-3_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}