{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:17:27Z","timestamp":1740097047137,"version":"3.37.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319049205"},{"type":"electronic","value":"9783319049212"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-04921-2_29","type":"book-chapter","created":{"date-parts":[[2014,2,5]],"date-time":"2014-02-05T08:52:25Z","timestamp":1391590345000},"page":"360-371","source":"Crossref","is-referenced-by-count":7,"title":["Counting Models of Linear-Time Temporal Logic"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hazem","family":"Torfah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Bayardo, R.J., Schrag, R.: Using csp look-back techniques to solve real-world sat instances. In: AAAI\/IAAI, pp. 203\u2013208 (1997)","DOI":"10.1007\/3-540-61551-2_65"},{"key":"29_CR2","unstructured":"Biere, A.: Bounded model checking. In: Handbook of Satisfiability, pp. 457\u2013481. IOS Press (2009)"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R.P., Gamauf, H.-J., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems with RATSY. In: Association, O.P. (ed.) Proceedings First Workshop on Synthesis (SYNT 2012), vol.\u00a084, pp. 47\u201353. Electronic Proceedings in Theoretical Computer Science (2012)","DOI":"10.4204\/EPTCS.84.4"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A. Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 652\u2013657. Springer, Heidelberg (2012)"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond (1992)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"29_CR6","unstructured":"Darwiche, A.: New advances in compiling cnf into decomposable negation normal form. In: ECAI, pp. 328\u2013332 (2004)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: Symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 272\u2013275. Springer, Heidelberg (2011)"},{"issue":"5-6","key":"29_CR8","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B. Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. International Journal on Software Tools for Technology Transfer\u00a015(5-6), 519\u2013539 (2013)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"29_CR9","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 633\u2013654. IOS Press, Amsterdam (2009), \n                    \n                      http:\/\/dblp.uni-trier.de\/db\/series\/faia\/faia185.html#GomesSS09"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-02930-1_20","volume-title":"Automata, Languages and Programming","author":"L. Kuhtz","year":"2009","unstructured":"Kuhtz, L., Finkbeiner, B.: LTL path checking is efficiently parallelizable. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol.\u00a05556, pp. 235\u2013246. Springer, Heidelberg (2009)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-23217-6_28","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"L. Kuhtz","year":"2011","unstructured":"Kuhtz, L., Finkbeiner, B.: Weak kripke structures and LTL. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 419\u2013433. Springer, Heidelberg (2011)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11901914_11","volume-title":"Automated Technology for Verification and Analysis","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Lampert, R.: On the construction of fine automata for safety properties. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 110\u2013124. Springer, Heidelberg (2006)"},{"key":"29_CR13","first-page":"2001","volume":"27","author":"M.L. Littman","year":"2000","unstructured":"Littman, M.L., Majercik, S.M., Pitassi, T.: Stochastic boolean satisfiability. Journal of Automated Reasoning\u00a027, 2001 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"29_CR14","unstructured":"Morwood, D., Bryce, D.: Evaluating temporal plans in incomplete domains. In: AAAI (2012)"},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46\u201357. IEEE Computer Society, Washington, DC (1977), \n                    \n                      http:\/\/dx.doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-04921-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T01:52:47Z","timestamp":1558835567000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-04921-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049205","9783319049212"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04921-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}