{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:03:16Z","timestamp":1725501796035},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540779643"},{"type":"electronic","value":"9783540779667"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77966-7_6","type":"book-chapter","created":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T08:59:24Z","timestamp":1201856364000},"page":"19-33","source":"Crossref","is-referenced-by-count":2,"title":["On the Characterization of Until as a Fixed Point Under Clocked Semantics"],"prefix":"10.1007","author":[{"given":"Dana","family":"Fisman","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, Springer, Heidelberg (2002)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"E. Clarke","year":"1980","unstructured":"Clarke, E., Emerson, E.: Characterizing correctness properties of parallel programs as fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol.\u00a085, Springer, Heidelberg (1980)"},{"key":"6_CR3","unstructured":"Dam, M.: Temporal logic, automata and classical theories - an introduction. Lecture Notes for the 6th European Summer School on Logic, Language and Information\u00a0 (1994)"},{"key":"6_CR4","unstructured":"Eisner, C., Fisman, D.: Sugar 2.0 proposal presented to the Accellera Formal Verification Technical Committee (March 2002), http:\/\/www.haifa.il.ibm.com\/projects\/verification\/sugar\/Sugar_2.0_Accellera.ps"},{"key":"6_CR5","volume-title":"A practical introduction to PSL","author":"C. Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A practical introduction to PSL. Springer, Heidelberg (2006)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_67","volume-title":"Automata, Languages and Programming","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.) ICALP 2003. LNCS, vol.\u00a02719, Springer, Heidelberg (2003)"},{"key":"6_CR7","series-title":"DIMACS Series in Discrete Mathematics","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1090\/dimacs\/031\/06","volume-title":"Descriptive Complexity and Finite Models","author":"E.A. Emerson","year":"1997","unstructured":"Emerson, E.A.: Model checking and the Mu-calculus. In: Descriptive Complexity and Finite Models. DIMACS Series in Discrete Mathematics, vol.\u00a031, pp. 185\u2013214. American Mathematical Society, Providence, RI (1997)"},{"key":"6_CR8","unstructured":"Havlicek, J., Fisman, D., Eisner, C.: Basic results on the semantics of Accellera PSL 1.1 foundation language. Technical Report\u00a02004.02 Accellera, (May 2004)"},{"key":"6_CR9","unstructured":"Havlicek, J., Levi, N., Miller, H., Shultz, K.: Extended CBV statement semantics, partial proposal presented to the Accellera Formal Verification Technical Committee (April 2002), http:\/\/www.eda.org\/vfv\/hm\/att-0772\/01-ecbv_statement_semantics.ps.gz"},{"key":"6_CR10","unstructured":"Annex E of IEEE Standard for SystemVerilog Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800 TM (2005)"},{"key":"6_CR11","unstructured":"IEEE Standard for Property Specification Language (PSL). IEEE Std 1850 TM (2005)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Kaivola, R.: A simple decision method for the linear-time mu-calculus (1995)","DOI":"10.1007\/978-1-4471-3078-9_13"},{"issue":"3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science\u00a027(3), 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"6_CR14","volume-title":"Temporal Verification of Reactive Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Specification. Springer, New York (1992)"},{"issue":"1","key":"6_CR15","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst.\u00a06(1), 68\u201393 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18 th Annual IEEE Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR17","series-title":"NATO Advanced Summer Isntitutes","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems","author":"A. Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K. (ed.) Logics and Models of Concurrent Systems. NATO Advanced Summer Institute, vol.\u00a0F-13, pp. 123\u2013144. Springer, Heidelberg (1985)"},{"key":"6_CR18","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math.\u00a05, 285\u2013309 (1955)","journal-title":"Pacific J. Math."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Banff Higher Order Workshop, pp. 238\u2013266 (1995)","DOI":"10.1007\/3-540-60915-6_6"}],"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-77966-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:57:28Z","timestamp":1619521048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77966-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540779643","9783540779667"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77966-7_6","relation":{},"subject":[]}}