{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:46:28Z","timestamp":1764402388583,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540401179"},{"type":"electronic","value":"9783540448297"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44829-2_5","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"74-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":55,"title":["Efficient Model Checking of Safety Properties"],"prefix":"10.1007","author":[{"given":"Timo","family":"Latvala","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design 19 (2001) 291\u2013314","journal-title":"Formal Methods in System Design"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker Spin. IEEE Transactions on Software Engineering 23 (1997) 279\u2013295","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Kurshan, R.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeon University Press (1994)","DOI":"10.1515\/9781400864041"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"Vardi, M. Y., Wolper, P.: Automata-theoretic techniques for modal logic of programs. Journal of Computer and System Sciences 32 (1986) 183\u2013221","journal-title":"Journal of Computer and System Sciences"},{"key":"5_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M. Vardi","year":"1996","unstructured":"Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure versus Automata. Volume 1043 of LNCS. Springer (1996) 238\u2013266"},{"key":"5_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume-title":"Computer Aided Verification (CAV\u201997)","author":"R. Hardin","year":"1997","unstructured":"Hardin, R., Kurshan, R., Shukla, S., Vardi, M.: A new heuristic for bad cycle detection using BDDs. In: Computer Aided Verification (CAV\u201997). Volume 1254 of LNCS., Springer (1997) 268\u2013278"},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/3-540-45139-0_4","volume-title":"SPIN 2001","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: SPIN 2001. Volume 2057 of LNCS., Springer (2001) 37\u201356"},{"key":"5_CR8","unstructured":"Heljanko, K.: Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets. PhD thesis, Helsinki University of Technology, Department of Computer Science and Engineering (2002)"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A. Sistla","year":"1994","unstructured":"Sistla, A.: Safety, liveness, and fairness in temporal logic. Formal Aspects in Computing 6 (1994) 495\u2013511","journal-title":"Formal Aspects in Computing"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Geilen, M.: On the construction of monitors for temporal logic properties. In: RV\u201901 \u2014 First Workshop on Runtime Verification. Volume 55 of Electronic Notes in Theoretical Computer Science., Elsevier Science Publishers (2001)","DOI":"10.1016\/S1571-0661(04)00252-X"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verication. Model-Checking Techniques and Tools. Springer (2001)","DOI":"10.1007\/978-3-662-04558-9"},{"key":"5_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Tools and Algorithms for the Construction and Analysis of Systems. Volume 2280 of LNCS., Springer (2002) 342\u2013356"},{"key":"5_CR13","unstructured":"Helovuo, J., Lepp\u00e4nen, S.: Exploration testing. In: Application of Concurrency in System Design (ACSD\u20192001), IEEE (2001) 201\u2013210"},{"key":"5_CR14","unstructured":"Latvala, T.: On model checking safety properties. Technical Report HUT-TCS-A76, Helsinki University of Technology (2002) Available from http:\/\/www.tcs.hut.fi\/Publications"},{"key":"5_CR15","unstructured":"Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science (1989)"},{"key":"5_CR16","unstructured":"Vardi, M.: Automata-theoretic approach to design verification. Webpage (1999) http:\/\/www.wisdom.weizmann.ac.il\/~vardi\/av\/notes\/lec2.ps"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Property specification patterns for finite-state verification. In: Workshop on Formal Methods in Software Practice, ACM Press (1998) 7\u201315","DOI":"10.1145\/298595.298598"},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification (CAV\u20192001)","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Computer Aided Verification (CAV\u20192001). Volume 2102 of LNCS., Springer (2001) 53\u201365"},{"key":"5_CR19","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, Warsaw, Chapman & Hall (1995) 3\u201318"},{"key":"5_CR20","unstructured":"M\u00e4kel\u00e4, M., Tauriainen, H., R\u00f6nkk\u00f6, M.: lbt: LTL to B\u00fcchi conversion (2001) http:\/\/www.tcs.hut.fi\/Software\/maria\/tools\/lbt\/"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. STTT \u2014 International Journal on Software Tools for Technology Transfer 4 (2002) 57\u201370","journal-title":"STTT \u2014 International Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T01:58:23Z","timestamp":1676685503000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}