{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:57:42Z","timestamp":1725512262683},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540708889"},{"type":"electronic","value":"9783540708896"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70889-6_1","type":"book-chapter","created":{"date-parts":[[2007,5,10]],"date-time":"2007-05-10T14:04:16Z","timestamp":1178805856000},"page":"1-15","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking PSL Using HOL and SMV"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Tuerk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Accellera. Property specification language reference manual, version 1.1 (June 2004), \n                    \n                      http:\/\/www.eda.org"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., et al.: 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":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., et al.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 363\u2013367. Springer, Heidelberg (2001)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/3-540-63166-6_53","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1997","unstructured":"Beer, I., et al.: RuleBase: Model checking at IBM. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 480\u2013483. Springer, Heidelberg (1997)"},{"key":"1_CR5","first-page":"1","volume-title":"Symposium on Logic in Computer Science (LICS)","author":"J. Burch","year":"1990","unstructured":"Burch, J., et al.: Symbolic model checking: 1020 states and beyond. In: Symposium on Logic in Computer Science (LICS), Washington, D.C., June 1990, pp. 1\u201333. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"1_CR6","unstructured":"Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05- 04, The Weizmann Institute of Science, Israel (2005)"},{"key":"1_CR7","first-page":"1","volume-title":"International Congress on Logic, Methodology and Philosophy of Science","author":"J. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.: On a decision method in restricted second order arithmetic. In: Nagel, E. (ed.) International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201312. Stanford University Press, Stanford (1960)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"1_CR10","unstructured":"DeepChip survey on assertions (June 2004), \n                    \n                      http:\/\/www.deepchip.com\/items\/dvcon04-06.html"},{"issue":"3","key":"1_CR11","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. Emerson","year":"1982","unstructured":"Emerson, E., Clarke, E.: Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"1_CR13","volume-title":"Symposium on Protocol Specification, Testing, and Verification (PSTV)","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., et al.: Simple on-the-fly automatic verification of linear temporal logic. In: Symposium on Protocol Specification, Testing, and Verification (PSTV), Warsaw, June 1995, North-Holland, Amsterdam (1995)"},{"key":"1_CR14","unstructured":"Gordon, M.: HOL: A machine oriented formulation of higher order logic. Tech. Rep.\u00a068, Computer Laboratory, University of Cambridge (May 1985)"},{"key":"1_CR15","unstructured":"Gordon, M.: PSL semantics in higher order logic. In: Workshop on Designing Correct Circuits (DCC), Barcelona, Spain (2004)"},{"key":"1_CR16","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"1_CR17","unstructured":"Havlicek, J., Fisman, D., Eisner, C.: Basic results on the semantics of Accellera PSL 1.1 foundation language. Technical Report 2004.02, Accellera (2004)"},{"key":"1_CR18","first-page":"3","volume-title":"Automata Studies","author":"S. Kleene","year":"1956","unstructured":"Kleene, S.: Representation of events in nerve nets and finite automata. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 3\u201341. Princeton University Press, Princeton (1956)"},{"key":"1_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer, Norwell (1993)"},{"key":"1_CR20","first-page":"46","volume-title":"Symposium on Foundations of Computer Science (FOCS), vol. 18","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Symposium on Foundations of Computer Science (FOCS), vol. 18, New York, vol.\u00a018, pp. 46\u201357. IEEE Computer Society Press, Los Alamitos (1977)"},{"key":"1_CR21","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":"1_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving automata generation for linear temporal logic by considering the automata hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 39\u201354. Springer, Heidelberg (2001)"},{"key":"1_CR23","series-title":"EATCS Series","volume-title":"Texts in Theoretical Computer Science","author":"K. Schneider","year":"2003","unstructured":"Schneider, K.: Verification of Reactive Systems \u2013 Formal Methods and Algorithms. In: Texts in Theoretical Computer Science. EATCS Series, Springer, Heidelberg (2003)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-48256-3_17","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Schneider","year":"1999","unstructured":"Schneider, K., Hoffmann, D.: A HOL conversion for translating linear time temporal logic to omega-automata. In: Bertot, Y., et al. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 255\u2013272. Springer, Heidelberg (1999)"},{"key":"1_CR25","unstructured":"Tuerk, T.: A hierarchy for Accellera\u2019s property specification language. Master\u2019s thesis, University of Kaiserslautern, Department of Computer Science (2005)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/11541868_22","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Tuerk","year":"2005","unstructured":"Tuerk, T., Schneider, K.: From PSL to LTL: A formal validation in HOL. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 342\u2013357. Springer, Heidelberg (2005)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vardi","year":"2001","unstructured":"Vardi, M.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 1\u201322. Springer, Heidelberg (2001)"},{"key":"1_CR28","first-page":"340","volume-title":"Symposium on Foundations of Computer Science (FOCS)","author":"P. Wolper","year":"1981","unstructured":"Wolper, P.: Temporal logic can be more expressive. In: Symposium on Foundations of Computer Science (FOCS), New York, pp. 340\u2013348. IEEE Computer Society Press, Los Alamitos (1981)"},{"issue":"1-2","key":"1_CR29","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"},{"key":"1_CR30","first-page":"185","volume-title":"Symposium on Foundations of Computer Science (FOCS)","author":"P. Wolper","year":"1983","unstructured":"Wolper, P., Vardi, M., Sistla, A.: Reasoning about infinite computations paths. In: Symposium on Foundations of Computer Science (FOCS), New York, pp. 185\u2013194. IEEE Computer Society Press, Los Alamitos (1983)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software, Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70889-6_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:11:09Z","timestamp":1605762669000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70889-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540708889","9783540708896"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70889-6_1","relation":{},"subject":[]}}