{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:49:26Z","timestamp":1725572966373},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_21","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"205-218","source":"Crossref","is-referenced-by-count":18,"title":["Some Complexity Results for SystemVerilog Assertions"],"prefix":"10.1007","author":[{"given":"Doron","family":"Bustan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Havlicek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Accellera. SystemVerilog 3.1a Language Reference Manual: Accellera\u2019s Extensions to Verilog (2004), http:\/\/www.eda.org\/sv\/SystemVerilog_3.1a.pdf"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.: Real-time logics: complexity and expressiveness. In: Proc. 5th Symp. on Logic in Computer Science, pp. 390\u2013401 (June 1990)","DOI":"10.21236\/ADA323441"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/3-540-36577-X_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 65\u201380. Springer, Heidelberg (2003)"},{"key":"21_CR4","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., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Tiemeyer, A., Singerman, E., 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, pp. 296\u2013311. Springer, Heidelberg (2002)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","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, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"21_CR6","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. In: Int\u2019l. Symp. on Leveraging Applications of Formal Methods (2004)"},{"key":"21_CR7","unstructured":"Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science (May 2005)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 191\u2013206. Springer, Heidelberg (2005)"},{"issue":"4","key":"21_CR9","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/s00165-003-0014-5","volume":"15","author":"M.J.C. Gordon","year":"2003","unstructured":"Gordon, M.J.C.: Validating the PSL\/Sugar semantics using automated reasoning. Formal Aspects of Computing\u00a015(4), 406\u2013421 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"21_CR10","unstructured":"Havlicek, J., Shultz, K., Armoni, R., Dudani, S., Cerny, E.: Notes on the semantics of local variables in Accellera SystemVerilog 3.1 concurrent assertions. Technical Report 2004.01, Accellera (May 2004), Available from: www.accellera.org"},{"key":"21_CR11","first-page":"35","volume":"19","author":"H.R. Lewis","year":"1978","unstructured":"Lewis, H.R.: Complexity of solvable cases of the decision problem for the predicate calculus. Foundations of Computer Science\u00a019, 35\u201347 (1978)","journal-title":"Foundations of Computer Science"},{"key":"21_CR12","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":"21_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development\u00a03, 115\u2013125 (1959)","journal-title":"IBM Journal of Research and Development"},{"key":"21_CR14","unstructured":"IEEE\u00a0Computer Society. 1800: IEEE Standard for SystemVerilog\u2013Unified Hardware Design, Specification, and Verification Language. IEEE (2005)"},{"key":"21_CR15","unstructured":"IEEE\u00a0Computer Society. 1850: IEEE Standard for Property Specification Language (PSL). IEEE (2005)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"van Emde Boas, P.: The convenience of tilings. In: Complexity, Logic and Recursion Theory. Lecture Notes in Pure and Applied Mathematics, vol.\u00a0187, pp. 331\u2013363 (1997)","DOI":"10.1201\/9780429187490-12"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"issue":"1","key":"21_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"21_CR19","unstructured":"Verification guild: A community of verification professionals, http:\/\/verificationguild.com"},{"key":"21_CR20","unstructured":"Wang, H.: Dominoes and the AEA case of the decision problem. In: Symposium on the Mathematical Theory of Automata, pp. 23\u201355 (1962)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:15:56Z","timestamp":1605644156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11817963_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}