{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:48:42Z","timestamp":1725558522035},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540406716"},{"type":"electronic","value":"9783540451389"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45138-9_26","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T18:41:48Z","timestamp":1277232108000},"page":"318-327","source":"Crossref","is-referenced-by-count":30,"title":["Relating Hierarchy of Temporal Properties to Model Checking"],"prefix":"10.1007","author":[{"given":"Ivana","family":"\u010cern\u00e1","sequence":"first","affiliation":[]},{"given":"Radek","family":"Pel\u00e1nek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Computer Aided Verification","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.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 222\u2013235. Springer, Heidelberg (1999)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-44829-2_4","volume-title":"Model Checking Software","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of linear temporal properties to model checking. Technical Report FIMU-RS-2003-03, Faculty of Informatics, Masaryk University (2003), http:\/\/www.fi.muni.cz\/informatics\/reports\/","key":"26_CR3","DOI":"10.1007\/978-3-540-45138-9_26"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/3-540-55719-9_97","volume-title":"Automata, Languages and Programming","author":"E.Y. Chang","year":"1992","unstructured":"Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 474\u2013486. Springer, Heidelberg (1992)"},{"key":"26_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design\u00a01, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/298595.298598","volume-title":"Proc. Workshop on Formal Methods in Software Practice","author":"M.B. Dwyer","year":"1998","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. Workshop on Formal Methods in Software Practice, pp. 7\u201315. ACM Press, New York (1998)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 57\u201379. Springer, Heidelberg (2001)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1109\/LICS.1996.561310","volume-title":"Proc. IEEE Symposium on Logic in Computer Science","author":"K. Etessami","year":"1996","unstructured":"Etessami, K., Wilke, T.: An Until hierarchy for temporal logic. In: Proc. IEEE Symposium on Logic in Computer Science, pp. 108\u2013117. Computer Society Press, Los Alamitos (1996)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., Fraer, R., Vardi, G.K.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"key":"26_CR12","first-page":"3","volume-title":"Proc. Protocol Specification Testing and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. Protocol Specification Testing and Verification, pp. 3\u201318. Chapman & Hall, Boca Raton (1995)"},{"key":"26_CR13","first-page":"23","volume-title":"Proc. SPIN Workshop","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. SPIN Workshop, pp. 23\u201332. American Mathematical Society, Providence (1996)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-45793-3_19","volume-title":"Computer Science Logic","author":"A. Ku\u010dera","year":"2002","unstructured":"Ku\u010dera, A., Strej\u010dek, J.: The stuttering principle revisited: On the expressiveness of nested X and U operators in the logic LTL. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 276\u2013291. Springer, Heidelberg (2002)"},{"issue":"3","key":"26_CR15","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"unstructured":"L\u00f6ding, C.: Methods for the transformation of omega-automata: Complexity and connection to second order logic. Master\u2019s thesis, Christian-Albrechts-University of Kiel (1998)","key":"26_CR16"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-44929-9_36","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"C. L\u00f6ding","year":"2000","unstructured":"L\u00f6ding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 521\u2013535. Springer, Heidelberg (2000)"},{"key":"26_CR18","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"Proc. ACM Symposium on Principles of Distributed Computing","author":"Z. Manna","year":"1990","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proc. ACM Symposium on Principles of Distributed Computing, pp. 377\u2013410. ACM Press, New York (1990)"},{"key":"26_CR19","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 automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 39\u201354. Springer, Heidelberg (2001)"},{"issue":"5","key":"26_CR20","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A.P. Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, liveness, and fairness in temporal logic. Formal Aspects of Computing\u00a06(5), 495\u2013512 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-45841-7_37","volume-title":"STACS 2002","author":"D. Therien","year":"2002","unstructured":"Therien, D., Wilke, T.: Nesting Until and Since in linear temporal logic. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol.\u00a02285, pp. 455\u2013464. Springer, Heidelberg (2002)"},{"key":"26_CR23","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of Formal Languages","author":"W. Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata and logic. In: Handbook of Formal Languages, vol.\u00a03, pp. 389\u2013455. Springer, Heidelberg (1997)"},{"doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about inifinite computation paths. In: Proc. Symp. on Foundations of Computer Science, Tuscon, pp. 185\u2013194 (1983)","key":"26_CR24","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45138-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T05:53:56Z","timestamp":1559195636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45138-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406716","9783540451389"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45138-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}