{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:10:21Z","timestamp":1725491421279},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372134"},{"type":"electronic","value":"9783540372141"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11812128_20","type":"book-chapter","created":{"date-parts":[[2006,8,9]],"date-time":"2006-08-09T09:32:31Z","timestamp":1155115951000},"page":"208-218","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Implementation of Alternating Automata"],"prefix":"10.1007","author":[{"given":"R.","family":"Bloem","sequence":"first","affiliation":[]},{"given":"A.","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"I.","family":"Pill","sequence":"additional","affiliation":[]},{"given":"M.","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"S.","family":"Semprini","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"IEEE-Commission: IEEE standard for Property Specification Language (PSL) (2005) IEEE Std (1850-2005)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","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.) TACAS 2002. LNCS, vol.\u00a02280, pp. 296\u2013311. Springer, Heidelberg (2002)"},{"key":"20_CR3","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. Logic in Computer Science, pp. 322\u2013331 (1986)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"1","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design\u00a01, 47\u201371 (1997)","journal-title":"Formal Methods in System Design"},{"key":"20_CR7","unstructured":"Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL, Prosyd\u00a0D\u00a03.2\/4 (2005), \n                    \n                      https:\/\/2.zoppoz.workers.dev:443\/http\/www.prosyd.org"},{"key":"20_CR8","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"},{"key":"20_CR9","unstructured":"Leucker, M.: Logics for mazurkiewicz traces. Technical Report AIB-2002-10, RWTH, Aachen, Germany (2002)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Jehle, M., Johannsen, J., Lange, M., Rachinsky, N.: Bounded model checking for all regular properties. In: 3rd Workshop on Bounded Model Checking (BMC 2005). Electronic Notes in Theoretical Computer Science, vol.\u00a0144.1, pp. 3\u201318 (2005)","DOI":"10.1016\/j.entcs.2005.07.016"},{"key":"20_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems, Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, New York (1992)"},{"issue":"3","key":"20_CR12","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"20_CR15","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSAT (2005), \n                    \n                      https:\/\/2.zoppoz.workers.dev:443\/http\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/Main.html"},{"key":"20_CR16","unstructured":"David, S.B., Orni, A.: Property-by-Example guide: a handbook of PSL\/Sugar examples - PROSYD deliverable d1.1\/3 (2005), \n                    \n                      https:\/\/2.zoppoz.workers.dev:443\/http\/www.prosyd.org"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-45089-0_5","volume-title":"Implementation and Application of Automata","author":"C. Fritz","year":"2003","unstructured":"Fritz, C.: Constructing b\u00fcchi automata from linear temporal logic using simulation relations for alternating b\u00fcchi automata. In: Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 35\u201348. Springer, Heidelberg (2003)"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/j.tcs.2005.01.016","volume":"338","author":"C. Fritz","year":"2005","unstructured":"Fritz, C., Wilke, T.: Simulation relations for alternating B\u00fcchi automata. Theoretical Computer Science\u00a0338, 275\u2013314 (2005)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/11812128_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:26:56Z","timestamp":1619508416000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/link.springer.com\/10.1007\/11812128_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372134","9783540372141"],"references-count":18,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/11812128_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}