{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:08:41Z","timestamp":1742382521409,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_11","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"110-124","source":"Crossref","is-referenced-by-count":14,"title":["On the Construction of Fine Automata for Safety Properties"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robby","family":"Lampert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11940197_11","volume-title":"Formal Approaches to Software Testing and Runtime Verification","author":"R. Armoni","year":"2006","unstructured":"Armoni, R., Korchemny, D., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: Deterministic dynamic monitors for linear-Time assertions. In: Havelund, K., N\u00fa\u00f1ez, M., Ro\u015fu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol.\u00a04262, Springer, Heidelberg (2006)"},{"issue":"2","key":"11_CR2","first-page":"142","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. I& C\u00a098(2), 142\u2013170 (1992)","journal-title":"I& C"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Moore, J.S.: Proof-checking, theorem-proving and program verification. Technical Report\u00a035, Institute for Computing Science and Computer Applications, University of Texas at Austin (January 1983)","DOI":"10.1090\/conm\/029\/07"},{"issue":"1","key":"11_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Bierea, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., 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":"11_CR6","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1109\/ASE.2001.989841","volume-title":"Proc. 16th International Conference on Automated Software Engineering","author":"D. Giannakopoulou","year":"2001","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proc. 16th International Conference on Automated Software Engineering, pp. 412\u2013416. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"11_CR7","first-page":"3","volume-title":"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: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman and Hall, Boca Raton (1995)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-55179-4_32","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1992","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 332\u2013342. Springer, Heidelberg (1992)"},{"key":"11_CR9","volume-title":"The Spin Model Checker: primer and reference manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: primer and reference manual. Addison-Wesley, Reading (2004)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1997","unstructured":"Hardin, R.H., Kurshan, R.P., Shukla, S.K., Vardi, M.Y.: A new heuristic for bad cycle detection using BDDs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 268\u2013278. Springer, Heidelberg (1997)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Iwashita, H., Nakata, T.: Forward model checking techniques oriented to buggy designs. In: Proc. ICCAD, pp. 400\u2013404 (1997)","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-540-30476-0_27","volume-title":"Automated Technology for Verification and Analysis","author":"O. Kupferman","year":"2004","unstructured":"Kupferman, O., Morgenstern, G., Murano, A.: Typeness for \u03c9-regular automata. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 324\u2013338. Springer, Heidelberg (2004)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-58325-4_202","volume-title":"Algorithms and Computation","author":"S.C. Krishnan","year":"1994","unstructured":"Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \u03c9-automata vis-a-vis deterministic B\u00fcchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol.\u00a0834, pp. 378\u2013386. Springer, Heidelberg (1994)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Safra, S., Vardi, M.Y.: Relating word and tree automata. In: Proc. 11th LICS, DIMACS, pp. 322\u2013333 (June 1996)","DOI":"10.1109\/LICS.1996.561360"},{"issue":"3","key":"11_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"},{"key":"11_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45653-8_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: On bounded specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 24\u201338. Springer, Heidelberg (2001)"},{"issue":"2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/1055686.1055689","volume":"6","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM Trans. on Computational Logic\u00a06(2), 273\u2013294 (2005)","journal-title":"ACM Trans. on Computational Logic"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, Pittsburgh, pp. 531\u2013540 (October 2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/BF01691063","volume":"3","author":"L.H. Landweber","year":"1969","unstructured":"Landweber, L.H.: Decision problems for \u03c9\u2013automata. Mathematical Systems Theory\u00a03, 376\u2013384 (1969)","journal-title":"Mathematical Systems Theory"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-44829-2_5","volume-title":"Model Checking Software","author":"T. Latvala","year":"2003","unstructured":"Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 74\u201388. Springer, Heidelberg (2003)"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Anuchitanukul, A., Bjorner, N., Browne, A., Chang, E., Colon, M., De Alfaro, L., Devarajan, H., Sipma, H., Uribe, T.: STeP: The Stanford Temporal Prover. TR STAN-CS-TR-94-1518, Dept. of Computer Science, Stanford University (1994)","DOI":"10.21236\/ADA324036"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 164\u2013174. Springer, Heidelberg (1993)"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Fischer, M.J.: Economy of description by automata, grammars, and formal systems. In: Proc. 12th IEEE Symp. on Switching and Automata Theory, pp. 188\u2013191 (1971)","DOI":"10.1109\/SWAT.1971.11"},{"key":"11_CR24","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theoretical Computer Science\u00a032, 321\u2013330 (1984)","journal-title":"Theoretical Computer Science"},{"key":"11_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)"},{"key":"11_CR26","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, New York (1995)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","first-page":"364","volume-title":"Computer Aided Verification","author":"S. Melzer","year":"1997","unstructured":"Melzer, S., Roemer, S.: Deadlock checking using net unfoldings. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 364\u2013375. Springer, Heidelberg (1997)"},{"key":"11_CR28","unstructured":"Owre, S., Shankar, R.E., Rushby, J.M.: User guide for the PVS specification and verification system. CSL (1995)"},{"key":"11_CR29","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"11_CR30","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal ACM\u00a032, 733\u2013749 (1985)","journal-title":"Journal ACM"},{"key":"11_CR31","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, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Sakoda, W., Sipser, M.: Non-determinism and the size of two-way automata. In: Proc. 10th STOC, pp. 275\u2013286 (1978)","DOI":"10.1145\/800133.804357"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Valmari","year":"1993","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, Springer, Heidelberg (1993)"},{"key":"11_CR34","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st LICS, Cambridge, pp. 332\u2013344 (June 1986)"},{"issue":"1","key":"11_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T09:47:56Z","timestamp":1736588876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/11901914_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}