{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:57:09Z","timestamp":1725490629376},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"},{"type":"electronic","value":"9783540733683"}],"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-73368-3_53","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"532-546","source":"Crossref","is-referenced-by-count":27,"title":["Boolean Abstraction for Temporal Logic Satisfiability"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Schuppan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"53_CR1","unstructured":"Accellera. Property specification language reference manual, version 1.1"},{"key":"53_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, Springer, Heidelberg (2002)"},{"key":"53_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"53_CR4","unstructured":"Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata Construction Algorithms Optimized for PSL, 2005. In: PROSYD deliverable D\u00a03.2\/4 (2005)"},{"key":"53_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"53_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science\u00a02 (2006)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"53_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11812128_20","volume-title":"Implementation and Application of Automata","author":"R. Bloem","year":"2006","unstructured":"Bloem, R., Cimatti, A., Pill, I., Roveri, M., Semprini, S.: Symbolic Implementation of Alternating Automata. In: Ibarra, O.H., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol.\u00a04094, Springer, Heidelberg (2006)"},{"issue":"1\u20133","key":"53_CR8","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s10817-005-9004-z","volume":"35","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: Tight integration of SAT and mathematical decision procedures. Journal of Automated Reasoning\u00a035(1\u20133), 265\u2013293 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"53_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, Springer, Heidelberg (1999)"},{"key":"53_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From PSL to NBA: a modular symbolic encoding. In: FMCAD (2006)","DOI":"10.1109\/FMCAD.2006.19"},{"key":"53_CR11","unstructured":"Cimatti, A., Roveri, M., Tonetta, S.: Syntactic optimizations for PSL verification. In: TACAS (2007)"},{"issue":"1","key":"53_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E. Clarke","year":"1997","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design\u00a010(1), 47\u201371 (1997)","journal-title":"Formal Methods in System Design"},{"key":"53_CR13","unstructured":"Ben David, S., Orni, A.: Property-by-Example guide: a handbook of PSL\/Sugar examples. In: PROSYD deliverable D\u00a01.1\/3 (2005)"},{"key":"53_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"53_CR15","doi-asserted-by":"crossref","unstructured":"Emerson, A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of TCS, Volume B: Formal Models and Sematics, pp. 995\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1","key":"53_CR16","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M. Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Logic\u00a02(1), 12\u201356 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"53_CR17","doi-asserted-by":"crossref","unstructured":"Fuxman, A., Liu, L., Pistore, M., Roveri, M., Mylopoulos, J.: Specifying and analyzing early requirements in Tropos: Some experimental results. In: RE (2003)","DOI":"10.1007\/s00766-004-0191-7"},{"key":"53_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0036915","volume-title":"Automata, Languages and Programming","author":"J.Y. Halpern","year":"1983","unstructured":"Halpern, J.Y., Manna, Z., Moszkowski, B.C.: A hardware semantics based on temporal intervals. In: D\u00edaz, J. (ed.) Automata, Languages and Programming. LNCS, vol.\u00a0154, Springer, Heidelberg (1983)"},{"key":"53_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_12","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2006","unstructured":"Heljanko, K., Junttila, T., Kein\u00e4nen, M., Lange, M., Latvala, T.: Bounded model checking for weak alternating b\u00fcchi automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"53_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"issue":"3","key":"53_CR21","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"53_CR22","unstructured":"Lange, M., Stirling, C.: Focus Games for Satisfiability and Completeness of Temporal Logic. In: LICS (2001)"},{"key":"53_CR23","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional Temporal Logics: Decidability and Completeness. Logic Journal of the IGPL\u00a08(1) (2000)","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"53_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)"},{"key":"53_CR25","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theoretical Computer Science\u00a032, 321\u2013330 (1984)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"53_CR26","doi-asserted-by":"publisher","first-page":"55","DOI":"10.3166\/jancl.14.55-104","volume":"14","author":"B.C. Moszkowski","year":"2004","unstructured":"Moszkowski, B.C.: A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time. Journal of Applied Non-Classical Logics\u00a014(1-2), 55\u2013104 (2004)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"53_CR27","doi-asserted-by":"crossref","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC (2006)","DOI":"10.1145\/1146909.1147119"},{"key":"53_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"53_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/11813040_38","volume-title":"FM 2006: Formal Methods","author":"A. Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 573\u2013586. Springer, Heidelberg (2006)"},{"key":"53_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36618-0","volume-title":"Correct Hardware Design and Verification Methods","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: \u201cMore Deterministic\u201d vs. \u201cSmaller\u201d B\u00fcchi Automata for Efficient LTL Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, Springer, Heidelberg (2003)"},{"key":"53_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, Springer, Heidelberg (2000)"},{"issue":"3","key":"53_CR32","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. J. ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"53_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"},{"issue":"1\/2","key":"53_CR34","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal Logic Can Be More Expressive. Information and Control\u00a056(1\/2), 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T01:35:53Z","timestamp":1558488953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540733676","9783540733683"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}