{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T18:24:51Z","timestamp":1729621491033,"version":"3.28.0"},"reference-count":31,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006,11]]},"DOI":"10.1109\/fmcad.2006.19","type":"proceedings-article","created":{"date-parts":[[2006,12,14]],"date-time":"2006-12-14T17:06:56Z","timestamp":1166116016000},"page":"125-133","source":"Crossref","is-referenced-by-count":17,"title":["From PSL to NBA: a Modular Symbolic Encoding"],"prefix":"10.1109","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"Simone","family":"Semprini","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/ISTCS.1997.595167"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_6"},{"key":"18","first-page":"196","article-title":"The Glory of the Past","author":"lichtenstein","year":"1985","journal-title":"J Logic Program"},{"key":"15","first-page":"573","article-title":"PSL Model Checking and Run-time Verification via Testers","volume":"4085","author":"pnueli","year":"2006","journal-title":"ser LNCS"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.19"},{"key":"13","first-page":"495","article-title":"NuSMV: A new Symbolic Model Verifier","volume":"1633","author":"cimatti","year":"1999","journal-title":"ser LNCS"},{"article-title":"Property-by-Example guide: A handbook of PSL\/Sugar examples","year":"2005","author":"david","key":"14"},{"key":"11","first-page":"247","article-title":"Efficient Bu?chi Automata from LTL Formulae","volume":"1855","author":"somenzi","year":"2000","journal-title":"ser LNCS"},{"key":"12","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/11513988_35","article-title":"Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking","author":"sebastiani","year":"2005","journal-title":"Proc of the 16th International Conference on Computer-Aided Verification (CAV'05)"},{"journal-title":"Introduction to Automata Theory Languages and Computation","year":"1979","author":"hopcroft","key":"21"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44612-5_65"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45687-2_37"},{"key":"24","first-page":"238","article-title":"An Automata-Theoretic Approach to Linear Temporal Logic","author":"vardi","year":"1995","journal-title":"Proc Banff Higher Order Workshop"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008615614281"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"26"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"28","first-page":"267","article-title":"Efficient Model Checking in Fragments of the Prepositional ?-Calculus","author":"emerson","year":"1986","journal-title":"Proc Symp Logic Comput Sci"},{"key":"29","first-page":"98","article-title":"Incremental and complete bounded model checking for full PLTL","volume":"3576","author":"heljanko","year":"2005","journal-title":"ser LNCS"},{"key":"3","first-page":"191","article-title":"Regular Vacuity","author":"bustan","year":"2005","journal-title":"CHARME"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90076-R"},{"key":"1","first-page":"1850","article-title":"IEEE standard for Property Specification Language (PSL)","year":"2005","journal-title":"IEEE Std"},{"journal-title":"MiniSat","year":"2005","author":"ee?n","key":"30"},{"key":"7","first-page":"95","article-title":"Bounded Model Checking for Weak Alternating Bu?chi Automata","volume":"4144","author":"heljanko","year":"2006","journal-title":"ser LNCS"},{"article-title":"Automata Construction Algorithms Optimized for PSL","year":"2005","author":"ben-david","key":"6"},{"key":"5","first-page":"35","article-title":"Constructing Bu?chi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Bu?chi Automata","volume":"2759","author":"fritz","year":"2003","journal-title":"ser LNCS"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0121-x"},{"key":"4","first-page":"53","article-title":"Fast 111 to bu?chi automata translation","volume":"2102","author":"gastin","year":"2001","journal-title":"ser LNCS"},{"year":"0","key":"9"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"}],"event":{"name":"2006 Formal Methods in Computer-Aided Design","start":{"date-parts":[[2006,11,12]]},"location":"San Jose, CA","end":{"date-parts":[[2006,11,16]]}},"container-title":["2006 Formal Methods in Computer Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx5\/4020992\/4020993\/04021018.pdf?arnumber=4021018","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,6]],"date-time":"2021-08-06T01:49:53Z","timestamp":1628214593000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/ieeexplore.ieee.org\/document\/4021018\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":31,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/fmcad.2006.19","relation":{},"subject":[],"published":{"date-parts":[[2006,11]]}}}