{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:25Z","timestamp":1760202625069,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405245"},{"type":"electronic","value":"9783540450696"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45069-6_36","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T21:11:46Z","timestamp":1277241106000},"page":"381-393","source":"Crossref","is-referenced-by-count":12,"title":["Bridging the Gap between Fair Simulation and Trace Inclusion"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. TCS\u00a082 (1991)","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"36_CR2","first-page":"189","volume":"24","author":"B. Bloom","year":"1996","unstructured":"Bloom, B., Paige, R.: Transformational design and implementation of a new efficient solution to the ready simulation problem. SCP\u00a024, 189\u2013220 (1996)","journal-title":"SCP"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: A simplified approach. In: JCSS (1974)","DOI":"10.1016\/S0022-0000(74)80051-6"},{"key":"36_CR4","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: 16th LICS (2001)"},{"key":"36_CR5","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model-checking in fragments of the propositional modal \u03bc-calculus. In: 1st LICS, pp. 267\u2013278 (1986)"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Model checking and the \u03bc-calculus. In: Descriptive Complexity and Finite Models, pp. 185\u2013214. AMS (1997)","DOI":"10.1090\/dimacs\/031\/06"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Harrington, L.A.: Automata, trees and games. In: 14th STOC (1982)","DOI":"10.1145\/800070.802177"},{"issue":"3","key":"36_CR8","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. TOPLAS\u00a016(3), 843\u2013871 (1994)","journal-title":"TOPLAS"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: 36th FOCS, pp. 453\u2013462 (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"36_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63141-0_19","volume-title":"CONCUR\u201997: Concurrency Theory","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 273\u2013287. Springer, Heidelberg (1997)"},{"key":"36_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-46419-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Henzinger","year":"2000","unstructured":"Henzinger, T., Rajamani, S.: Fair bisimulation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 299. Springer, Heidelberg (2000)"},{"key":"36_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M. Jurdzinski","year":"2000","unstructured":"Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol.\u00a01770, pp. 290\u2013301. Springer, Heidelberg (2000)"},{"key":"36_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 \u03bc-calculus. TCS\u00a027, 333\u2013354 (1983)","journal-title":"TCS"},{"issue":"1","key":"36_CR14","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstractions: The cornerstones of practical formal verification. STTT\u00a02(1), 328\u2013342 (2000)","journal-title":"STTT"},{"key":"36_CR15","first-page":"203","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by finitary abstraction. IC\u00a0163, 203\u2013243 (2000)","journal-title":"IC"},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 1\u201316. Springer, Heidelberg (1998)"},{"key":"36_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 - Concurrency Theory","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariants in action. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013105. Springer, Heidelberg (2002)"},{"key":"36_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-44450-5_12","volume-title":"FSTTCS 2000: Foundations of Software Technology and Theoretical Science","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Fair equivalence relations. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 151\u2013163. Springer, Heidelberg (2000)"},{"key":"36_CR19","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: 30th STOC, pp. 224\u2013233 (1998)","DOI":"10.1145\/276698.276748"},{"key":"36_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/3-540-18088-5_24","volume-title":"Automata, Languages and Programming","author":"K. Lodaya","year":"1987","unstructured":"Lodaya, K., Thiagarajan, P.S.: A modal logic for a subclass of events structures. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 290\u2013303. Springer, Heidelberg (1987)"},{"key":"36_CR21","unstructured":"Manna, Z., Anuchitanukul, A., Bj\u00f8rner, N., Browne, A., Chang, E., Col\u00f3n, M., De Alfaro, L., Devarajan, H., Sipma, H., Uribe, T.E.: STeP. Tech. Report, Stanford (1994)"},{"key":"36_CR22","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: IJCAI (1971)"},{"key":"36_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"36_CR24","doi-asserted-by":"crossref","unstructured":"Safra, S.: Exponential determinization for \u03c9-automata with strong-fairness acceptance condition. In: 24th STOC (1992)","DOI":"10.1145\/129712.129739"},{"key":"36_CR25","first-page":"79","volume":"51","author":"M.Y. Vardi","year":"1991","unstructured":"Vardi, M.Y.: Verification of concurrent programs \u2013 the automata-theoretic framework. APAL\u00a051, 79\u201398 (1991)","journal-title":"APAL"},{"key":"36_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45069-6_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T04:59:49Z","timestamp":1740200389000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45069-6_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405245","9783540450696"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45069-6_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}