{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:26:21Z","timestamp":1740108381451,"version":"3.37.3"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T00:00:00Z","timestamp":1479340800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Deutsche Forschungsgemeinschaft (DE)","award":["SFB\/TR 14","ZI 1516\/1-1"],"award-info":[{"award-number":["SFB\/TR 14","ZI 1516\/1-1"]}]},{"DOI":"10.13039\/501100002990","name":"Deutsche Telekom Stiftung","doi-asserted-by":"publisher","award":["T-13-11"],"award-info":[{"award-number":["T-13-11"]}],"id":[{"id":"10.13039\/501100002990","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,5]]},"DOI":"10.1007\/s00236-016-0284-z","type":"journal-article","created":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T06:09:40Z","timestamp":1479362980000},"page":"191-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The complexity of counting models of linear-time temporal logic"],"prefix":"10.1007","volume":"55","author":[{"given":"Hazem","family":"Torfah","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,17]]},"reference":[{"key":"284_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804090","volume-title":"Computational Complexity: A Modern Approach","author":"S Arora","year":"2009","unstructured":"Arora, S., Barak, B.: Computational Complexity: A Modern Approach, 1st edn. Cambridge University Press, New York (2009)","edition":"1"},{"key":"284_CR2","doi-asserted-by":"crossref","unstructured":"Bertoni, A. Mauri, G., Sabadini, N.: A characterization of the class of functions computable in polynomial time on random access machines. In: STOC 1981, pp 168\u2013176. ACM (1981)","DOI":"10.1145\/800076.802470"},{"key":"284_CR3","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, pp. 457\u2013481. IOS Press (2009)"},{"key":"284_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gamauf, H.-J., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems with RATSY. In: Peled, D., Schewe, S. (eds.) SYNT 2012, Volume\u00a084 of EPTCS, pp. 47\u201353. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.84.4"},{"key":"284_CR5","first-page":"652","volume-title":"CAV 2012, Volume 7358 of LNCS","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, Volume 7358 of LNCS, pp. 652\u2013657. Springer, New York (2012)"},{"issue":"2","key":"284_CR6","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"284_CR7","first-page":"272","volume-title":"TACAS 2011, Volume 6605 of LNCS","author":"R Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Rustan, K., Leino, M. (eds.) TACAS 2011, Volume 6605 of LNCS, pp. 272\u2013275. Springer, New York (2011)"},{"issue":"5\u20136","key":"284_CR8","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"284_CR9","first-page":"360","volume-title":"LATA 2014, Volume 8370 of LNCS","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Torfah, H.: Counting models of linear-time temporal logic. In: Dediu, A.H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.L., Truthe, B. (eds.) LATA 2014, Volume 8370 of LNCS, pp. 360\u2013371. Springer, New York (2014)"},{"issue":"1","key":"284_CR10","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/203610.203611","volume":"26","author":"LA Hemaspaandra","year":"1995","unstructured":"Hemaspaandra, L.A., Vollmer, H.: The satanic notations: counting classes beyond #P and other definitional adventures. SIGACT News 26(1), 2\u201313 (1995)","journal-title":"SIGACT News"},{"key":"284_CR11","first-page":"235","volume-title":"ICALP 2009, Volume 5556 of LNCS","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, Volume 5556 of LNCS, pp. 235\u2013246. Springer, New York (2009)"},{"issue":"6","key":"284_CR12","doi-asserted-by":"crossref","first-page":"1087","DOI":"10.1137\/0218073","volume":"18","author":"RE Ladner","year":"1989","unstructured":"Ladner, R.E.: Polynomial space counting problems. SIAM J. Comput. 18(6), 1087\u20131097 (1989)","journal-title":"SIAM J. Comput."},{"issue":"304","key":"284_CR13","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0304-3975(03)00080-X","volume":"1\u20133","author":"M Li\u015bkiewicz","year":"2003","unstructured":"Li\u015bkiewicz, M., Ogihara, M., Toda, S.: The complexity of counting self-avoiding walks in subgraphs of two-dimensional grids and hypercubes. Theor. Comput. Sci. 1\u20133(304), 129\u2013156 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"284_CR14","first-page":"2001","volume":"27","author":"ML Littman","year":"2000","unstructured":"Littman, M.L., Majercik, S.M., Pitassi, T.: Stochastic boolean satisfiability. J. Autom. Reason. 27, 2001 (2000)","journal-title":"J. Autom. Reason."},{"key":"284_CR15","first-page":"245","volume-title":"CSR 2014, Volume 8476 of LNCS","author":"M Lohrey","year":"2014","unstructured":"Lohrey, M., Schmidt-Schau\u00df, M.: Processing succinct matrices and vectors. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.-\u00c9., Vereshchagin, N.K. (eds.) CSR 2014, Volume 8476 of LNCS, pp. 245\u2013258. New York, Springer (2014)"},{"key":"284_CR16","volume-title":"AAAI 2012","author":"D Morwood","year":"2012","unstructured":"Morwood, D., Bryce, D.: Evaluating temporal plans in incomplete domains. In: Hoffmann, J., Selman, B. (eds.) AAAI 2012. AAAI Press, Menlo Park (2012)"},{"key":"284_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"284_CR18","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A Prasad Sistla","year":"1985","unstructured":"Prasad Sistla, A., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"5","key":"284_CR19","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A Prasad Sistla","year":"1994","unstructured":"Prasad Sistla, A.: Safety, liveness and fairness in temporal logic. Form. Asp. Comput. 6(5), 495\u2013511 (1994)","journal-title":"Form. Asp. Comput."},{"key":"284_CR20","first-page":"241","volume-title":"FSTTCS 2014, Volume 29 of LIPIcs","author":"H Torfah","year":"2014","unstructured":"Torfah, H., Zimmermann, M.: The complexity of counting models of linear-time temporal logic. In: Raman, V., Suresh, S.P. (eds.) FSTTCS 2014, Volume 29 of LIPIcs, pp. 241\u2013252. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Wadern (2014)"},{"key":"284_CR21","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0304-3975(79)90044-6","volume":"8","author":"LG Valiant","year":"1979","unstructured":"Valiant, L.G.: The complexity of computing the permanent. Theor. Comput. Sci. 8, 189\u2013201 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"284_CR22","unstructured":"Williams, R.: A counting class based on PSPACE. http:\/\/web.stanford.edu\/~rrwill\/sharp-p-pspace.pdf (1999)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0284-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0284-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0284-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T14:01:53Z","timestamp":1568556113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0284-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,17]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,5]]}},"alternative-id":["284"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0284-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2016,11,17]]}}}