{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T04:35:40Z","timestamp":1771043740549,"version":"3.50.1"},"publisher-location":"Cham","reference-count":74,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_24","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"795-829","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Functional Specification of Hardware via Temporal Logic"],"prefix":"10.1007","author":[{"given":"Cindy","family":"Eisner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dana","family":"Fisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"24_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1007\/10722167_40","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"Y. Abarbanel","year":"2000","unstructured":"Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0538\u2013542. Springer, Heidelberg (2000)"},{"issue":"4","key":"24_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"24_CR4","series-title":"LNCS","first-page":"65","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Bustan, D., Kupferman, O., Vardi, M.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02619, pp.\u00a065\u201380. Springer, Heidelberg (2003)"},{"key":"24_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39799-8_13","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Armoni","year":"2013","unstructured":"Armoni, R., Fisman, D., Jin, N.: SVA and PSL local variables\u2014a\u00a0practical approach. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a08044, pp.\u00a0197\u2013212. Springer, Heidelberg (2013)"},{"key":"24_CR6","series-title":"LNCS","first-page":"296","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","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., Zbar, Y.: The ForSpec temporal logic: a\u00a0new temporal property-specification language. In: Katoen, J., Stevens, P. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02280, pp.\u00a0296\u2013311. Springer, Heidelberg (2002)"},{"key":"24_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","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.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a0363\u2013367. Springer, Heidelberg (2001)"},{"key":"24_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Hu, A.J., Vardi, M.Y. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01427, pp.\u00a0184\u2013194. Springer, Heidelberg (1998)"},{"key":"24_CR9","unstructured":"Ben-David, S., Bloem, R., Fisman, D., Griesmayer, A., Pill, I., Ruah, S.: Automata construction algorithms optimized for PSL (Deliverable 3.2\/4). Tech. rep., PROSYD (2005)"},{"key":"24_CR10","series-title":"LNCS","first-page":"14","volume-title":"Intl. Haifa Verification Conference (HVC)","author":"S. Ben-David","year":"2005","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: The safety simple subset. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol.\u00a03875, pp.\u00a014\u201329. Springer, Heidelberg (2005)"},{"issue":"3","key":"24_CR11","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/j.tcs.2008.03.011","volume":"404","author":"S. Ben-David","year":"2008","unstructured":"Ben-David, S., Fisman, D., Ruah, S.: Embedding finite automata within regular expressions. Theor. Comput. Sci. 404(3), 202\u2013218 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0222\u2013235. Springer, Heidelberg (1999)"},{"key":"24_CR13","unstructured":"Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Tech. Rep. MCS05-04, The Weizmann Institute of Science (2005)"},{"key":"24_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","author":"D. Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.: Regular vacuity. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a03725, pp.\u00a0191\u2013206. Springer, Heidelberg (2005)"},{"key":"24_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/11817963_21","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Bustan","year":"2006","unstructured":"Bustan, D., Havlicek, J.: Some complexity results for SystemVerilog assertions. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0205\u2013218. Springer, Heidelberg (2006)"},{"key":"24_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-6600-1","volume-title":"The Power of Assertions in SystemVerilog","author":"E. Cerny","year":"2010","unstructured":"Cerny, E., Dudani, S., Havlicek, J., Korchemny, D.: The Power of Assertions in SystemVerilog. Springer, Heidelberg (2010)"},{"key":"24_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logic of Programs","author":"E. Clarke","year":"1981","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Workshop on Logic of Programs. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1981)"},{"key":"24_CR18","unstructured":"Eisner, C., Fisman, D.: Sugar 2.0 proposal presented to the Accellera Formal Verification Technical Committee (2002). At http:\/\/www.haifa.il.ibm.com\/projects\/verification\/sugar\/Sugar_2.0_Accellera.ps"},{"key":"24_CR19","volume-title":"A Practical Introduction to PSL","author":"C. Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, New York (2006)"},{"key":"24_CR20","first-page":"1","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"C. Eisner","year":"2008","unstructured":"Eisner, C., Fisman, D.: Augmenting a regular expression-based temporal logic with local variables. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a01\u20138. IEEE, Piscataway (2008)"},{"key":"24_CR21","series-title":"LNCS","first-page":"164","volume-title":"Intl. Haifa Verification Conference (HVC)","author":"C. Eisner","year":"2008","unstructured":"Eisner, C., Fisman, D.: Structural contradictions. In: Chockler, H., Hu, A.J. (eds.) Intl. Haifa Verification Conference (HVC). LNCS, vol.\u00a05394, pp.\u00a0164\u2013178. Springer, Heidelberg (2008)"},{"key":"24_CR22","first-page":"1","volume-title":"Symp. on Principles of Distributed Computing (PODC)","author":"C. Eisner","year":"2005","unstructured":"Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: Aguilera, M.K., Aspnes, J. (eds.) Symp. on Principles of Distributed Computing (PODC), pp.\u00a01\u20138. ACM, New York (2005)"},{"issue":"2","key":"24_CR23","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/2532440","volume":"15","author":"C. Eisner","year":"2014","unstructured":"Eisner, C., Fisman, D., Havlicek, J.: Safety and liveness, weakness and strength, and the underlying topological relations. ACM Trans. Comput. Log. 15(2), 13:1\u201313:44 (2014)","journal-title":"ACM Trans. Comput. Log."},{"key":"24_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02725, pp.\u00a027\u201339. Springer, Heidelberg (2003)"},{"key":"24_CR25","unstructured":"Eisner, C., Fisman, D., Havlicek, J., M\u00e5rtensson, J.: The \u22a4,\u22a5$\\top, \\bot$ approach for truncated semantics. Tech. Rep. 2006.01, Accellera (2006)"},{"key":"24_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1007\/3-540-45061-0_67","volume-title":"Intl. Coll. on Automata, Languages and Programming (ICALP)","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., McIsaac, A., Van Campenhout, D.: The definition of a temporal clock operator. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Intl. Coll. on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a02719, pp.\u00a0857\u2013870. Springer, Heidelberg (2003)"},{"key":"24_CR27","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B","author":"E. Emerson","year":"1990","unstructured":"Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B, pp.\u00a0995\u20131072. Elsevier\/MIT Press, Amsterdam\/Cambridge (1990). Chap.\u00a016"},{"key":"24_CR28","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. Fischer","year":"1979","unstructured":"Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J.\u00a0Comput. Syst. Sci. 18, 194\u2013211 (1979)","journal-title":"J.\u00a0Comput. Syst. Sci."},{"key":"24_CR29","series-title":"LNCS","first-page":"19","volume-title":"Intl. Haifa Verification Conference (HVC)","author":"D. Fisman","year":"2007","unstructured":"Fisman, D.: On the characterization of until as a fixed point under clocked semantics. In: Yorav, K. (ed.) Intl. Haifa Verification Conference (HVC). LNCS, vol.\u00a04899, pp.\u00a019\u201333. Springer, Heidelberg (2007)"},{"key":"24_CR30","first-page":"127","volume-title":"Advances in Modal Logic","author":"T. French","year":"2002","unstructured":"French, T., Reynolds, M.: A sound and complete proof system for QPTL. In: Balbiani, P., Suzuki, N., Wolter, F., Zakharyaschev, M. (eds.) Advances in Modal Logic, pp.\u00a0127\u2013148. King\u2019s College Publications, London (2002)"},{"key":"24_CR31","first-page":"163","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"D. Gabbay","year":"1980","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Abrahams, P.W., Lipton, R.J., Bourne, S.R. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0163\u2013173. ACM, New York (1980)"},{"key":"24_CR32","series-title":"LNCS","volume-title":"Intl. Symp. on Mathematical Foundations of Computer Science (MFCS)","author":"W. Gelade","year":"2008","unstructured":"Gelade, W.: Succinctness of regular expressions with interleaving, intersection and counting. In: Ochmanski, E., Tyszkiewicz, J. (eds.) Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol.\u00a05162. Springer, Heidelberg (2008)"},{"key":"24_CR33","series-title":"Leibniz International Proceedings in Informatics","first-page":"325","volume-title":"Annual Symp. on Theoretical Aspects of Computer Science (STACS)","author":"W. Gelade","year":"2008","unstructured":"Gelade, W., Neven, F.: Succinctness of the complement and intersection of regular expressions. In: Annual Symp. on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics, vol.\u00a01, pp.\u00a0325\u2013336. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl (2008)"},{"issue":"4","key":"24_CR34","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/s00165-003-0014-5","volume":"15","author":"M. Gordon","year":"2003","unstructured":"Gordon, M.: Validating the PSL\/Sugar semantics using automated reasoning. Form. Asp. Comput. 15(4), 406\u2013421 (2003)","journal-title":"Form. Asp. Comput."},{"key":"24_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-18088-5_22","volume-title":"Intl. Coll. on Automata, Languages and Programming (ICALP)","author":"T. Hafer","year":"1987","unstructured":"Hafer, T., Thomas, W.: Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) Intl. Coll. on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0267, pp.\u00a0269\u2013279. Springer, Heidelberg (1987)"},{"key":"24_CR36","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"Intl. Coll. on Automata, Languages and Programming (ICALP)","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.) Intl. Coll. on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0154, pp.\u00a0278\u2013291. Springer, Heidelberg (1983)"},{"issue":"2","key":"24_CR37","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0022-0000(82)90003-4","volume":"25","author":"D. Harel","year":"1982","unstructured":"Harel, D., Kozen, D., Parikh, R.: Process logic: expressiveness, decidability, completeness. J.\u00a0Comput. Syst. Sci. 25(2), 144\u2013170 (1982)","journal-title":"J.\u00a0Comput. Syst. Sci."},{"key":"24_CR38","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"24_CR39","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0304-3975(85)90225-7","volume":"38","author":"D. Harel","year":"1985","unstructured":"Harel, D., Peleg, D.: Process logic with regular formulas. Theor. Comput. Sci. 38, 307\u2013322 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"24_CR40","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. Tech. Rep. 2004.01, Accellera (2004)"},{"key":"24_CR41","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-31623-4_13","volume-title":"Workshop on Descriptional Complexity of Formal Systems (DCFS)","author":"M. Holzer","year":"2012","unstructured":"Holzer, M., Jakobi, S.: State complexity of chop operations on unary and finite languages. In: Kutrib, M., Moreira, N., Reis, R. (eds.) Workshop on Descriptional Complexity of Formal Systems (DCFS). LNCS, vol.\u00a07386, pp.\u00a0169\u2013182. Springer, Heidelberg (2012)"},{"key":"24_CR42","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)"},{"key":"24_CR43","unstructured":"IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850\u2122-2005"},{"key":"24_CR44","unstructured":"IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850\u2122-2010"},{"key":"24_CR45","unstructured":"IEEE Standard for SystemVerilog\u2014Unified Hardware Design, Specification, and Verification Language, Annex E. IEEE Std 1800\u2122-2005"},{"key":"24_CR46","unstructured":"IEEE Standard for SystemVerilog\u2014Unified Hardware Design, Specification, and Verification Language, Annex F. IEEE Std 1800\u2122-2009"},{"key":"24_CR47","unstructured":"Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, Univ. of California, Los Angeles (1968)"},{"key":"24_CR48","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/LICS.1995.523239","volume-title":"Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science","author":"Y. Kesten","year":"1995","unstructured":"Kesten, Y., Pnueli, A.: A complete proof system for QPTL. In: Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pp.\u00a02\u201312. IEEE, Piscataway (1995)"},{"key":"24_CR49","first-page":"163","volume-title":"Symp. on Programming Languages and Software Tools (SPLST)","author":"P. Kilpel\u00e4inen","year":"2003","unstructured":"Kilpel\u00e4inen, P., Tuhkanen, R.: Regular expressions with numerical occurrence indicators\u2014preliminary results. In: Kilpel\u00e4inen, P., P\u00e4ivinen, N. (eds.) Symp. on Programming Languages and Software Tools (SPLST), pp.\u00a0163\u2013173 (2003). University of Kuopio, Department of Computer Science"},{"key":"24_CR50","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0172\u2013183. Springer, Heidelberg (1999)"},{"key":"24_CR51","series-title":"LNCS","first-page":"90","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"M. Lange","year":"2007","unstructured":"Lange, M.: Linear time logics around PSL: complexity, expressiveness, and a little bit of succinctness. In: Caires, L., Vasconcelos, V.T. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a04703, pp.\u00a090\u2013104. Springer, Heidelberg (2007)"},{"key":"24_CR52","first-page":"383","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"F. Laroussinie","year":"2002","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Kohlenbach, U., Abramsky, S. (eds.) Symp. on Logic in Computer Science (LICS), pp.\u00a0383\u2013392. IEEE, Piscataway (2002)"},{"key":"24_CR53","first-page":"97","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Deusen, M.S.V., Galil, Z., Reid, B.K. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a097\u2013107. ACM, New York (1985)"},{"key":"24_CR54","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logic of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs. LNCS, vol.\u00a0193, pp.\u00a0196\u2013218. Springer, Heidelberg (1985)"},{"key":"24_CR55","first-page":"648","volume-title":"Asia and South Pacific Design Automation Conf. (ASPDAC)","author":"J. Long","year":"2009","unstructured":"Long, J., Seawright, A., Kavalipati, P.: Multi-clock SVA synthesis without re-writing. In: Wakabayashi, K. (ed.) Asia and South Pacific Design Automation Conf. (ASPDAC), pp.\u00a0648\u2013653. IEEE, Piscataway (2009)"},{"key":"24_CR56","first-page":"643","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"M. Maidl","year":"2000","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0643\u2013652. IEEE, Piscataway (2000)"},{"key":"24_CR57","doi-asserted-by":"publisher","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 Academic, Norwell (1993)"},{"key":"24_CR58","volume-title":"Counter-Free Automata (MIT Research Monograph No.\u00a065)","author":"R. McNaughton","year":"1971","unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT Research Monograph No.\u00a065). MIT Press, Cambridge (1971)"},{"key":"24_CR59","series-title":"Formal Methods in Computation","volume-title":"Proc. Banff Higher Order Workshop","author":"M. Morley","year":"1999","unstructured":"Morley, M.: Semantics of temporal e. In: Melham, T.F., Moller, F.G. (eds.) Proc. Banff Higher Order Workshop. Formal Methods in Computation (1999). Univ. of Glasgow, Dept. of Computing Science. Technical Report"},{"key":"24_CR60","first-page":"422","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"D.E. Muller","year":"1988","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0422\u2013427. IEEE, Piscataway (1988)"},{"key":"24_CR61","first-page":"129","volume-title":"Design Automation Conf. (DAC)","author":"M.T. Oliveira","year":"2002","unstructured":"Oliveira, M.T., Hu, A.J.: High-level specification and automatic generation of IP interface monitors. In: Design Automation Conf. (DAC), pp.\u00a0129\u2013134. ACM, New York (2002)"},{"key":"24_CR62","first-page":"46","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a046\u201357. IEEE, Piscataway (1977)"},{"key":"24_CR63","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. Tech. rep., Massachusetts Inst. of Technology (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"24_CR64","first-page":"424","volume-title":"Design Automation Conf. (DAC)","author":"A. Seawright","year":"1993","unstructured":"Seawright, A., Brewer, F.: High-level symbolic construction technique for high performance sequential synthesis. In: Dunlop, A.E. (ed.) Design Automation Conf. (DAC), pp.\u00a0424\u2013428. IEEE, Piscataway (1993)"},{"key":"24_CR65","unstructured":"Sistla, A.P.: Theoretical issues in the design and verification of distributed systems. Ph.D. thesis, Harvard Univ. (1983)"},{"issue":"3","key":"24_CR66","first-page":"733","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J.\u00a0ACM 32(3), 733\u2013749 (1985)","journal-title":"J.\u00a0ACM"},{"key":"24_CR67","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.L.: The complementation problem for B\u00fcchi automata, with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"24_CR68","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/S0019-9958(79)90629-6","volume":"42","author":"W. Thomas","year":"1979","unstructured":"Thomas, W.: Star-free regular sets of \u03c9$\\omega$-sequences. Inf. Control 42(2), 148\u2013156 (1979)","journal-title":"Inf. Control"},{"key":"24_CR69","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Vardi","year":"2001","unstructured":"Vardi, M.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02031, pp.\u00a01\u201322. Springer, Heidelberg (2001)"},{"key":"24_CR70","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-69850-0_10","volume-title":"25 Years of Model Checking","author":"M.Y. Vardi","year":"2008","unstructured":"Vardi, M.Y.: From Church and Prior to PSL. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp.\u00a0150\u2013171. Springer, Heidelberg (2008)"},{"key":"24_CR71","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/3-540-12896-4_383","volume-title":"Workshop on Logic of Programs","author":"M.Y. Vardi","year":"1983","unstructured":"Vardi, M.Y., Wolper, P.: Yet another process logic (preliminary version). In: Clarke, E.M., Kozen, D. (eds.) Workshop on Logic of Programs. LNCS, vol.\u00a0164, pp.\u00a0501\u2013512. Springer, Heidelberg (1983)"},{"key":"24_CR72","first-page":"332","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Symp. on Logic in Computer Science (LICS), pp.\u00a0332\u2013344. IEEE, Piscataway (1986)"},{"key":"24_CR73","first-page":"162","volume-title":"Design, Automation & Test in Europe (DATE)","author":"K. Winkelmann","year":"2004","unstructured":"Winkelmann, K., Trylus, H., Stoffel, D., Fey, G.: Cost-efficient block verification for a UMTS up-link chip-rate coprocessor. In: Design, Automation & Test in Europe (DATE), pp.\u00a0162\u2013167. IEEE, Piscataway (2004)"},{"issue":"1\/2","key":"24_CR74","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. Inf. Control 56(1\/2), 72\u201399 (1983)","journal-title":"Inf. Control"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T05:45:12Z","timestamp":1571377512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_24","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}