{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T02:17:50Z","timestamp":1772158670908,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664253","type":"print"},{"value":"9783540483205","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48320-9_27","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T13:52:42Z","timestamp":1195134762000},"page":"383-398","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Robust Satisfaction"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,19]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proc. 38th IEEE Symposium on Foundations of Computer Science, pages 100\u2013109, 1997.","DOI":"10.1109\/SFCS.1997.646098"},{"issue":"1","key":"27_CR2","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73\u2013132, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"27_CR3","volume-title":"Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the Control-D system","author":"M. Antoniotti","year":"1995","unstructured":"M. Antoniotti. Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the Control-D system. PhD thesis, New York University, New York, 1995."},{"key":"27_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-58179-0_50","volume-title":"Proc. 6th CAV","author":"O. Bernholtz","year":"1994","unstructured":"O. Bernholtz, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In D. L. Dill, editor, Proc. 6th CAV, LNCS 818, pages 142\u2013155, 1994."},{"key":"27_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. Workshop on Logic of Programs","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pages 52\u201371, 1981."},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and M. C. Browne. Reasoning about networks with many identical finite-state processes. In Proc. 5th PODC, pages 240\u2013248, 1986.","DOI":"10.21236\/ADA188743"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"D. L. Dill. Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. Jutla. Tree automata, Mu-calculus and determinacy. In Proc. 32nd IEEE Symposium on Foundations of Computer Science, pages 368\u2013377, San Juan, October 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"27_CR9","unstructured":"E. A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proc. 18th Hawaii International Conference on System Sciences, North Holywood, 1985.Western Periodicals Company."},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, pages 997\u20131072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"27_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-50302-1_11","volume-title":"Proc. Symp. on Formal Techniques in Real-Time and FaultTolerant Systems","author":"M. J. Fischer","year":"1988","unstructured":"M. J. Fischer and L. D. Zuck. Reasoning about uncertainty in fault-tolerant distributed systems. In M. Joseph, editor, Proc. Symp. on Formal Techniques in Real-Time and FaultTolerant Systems, LNCS 331, pages 142\u2013158, 1988."},{"key":"27_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-54430-5_93","volume-title":"Proc. 2nd CONCUR","author":"O. Grumberg","year":"1991","unstructured":"O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. 2nd CONCUR, LNCS 527, pages 250\u2013265, 1991."},{"issue":"3","key":"27_CR13","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D. E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"27_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-58201-0_66","volume-title":"Proc. 21st ICALP","author":"R. Gawlick","year":"1994","unstructured":"R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. In Proc. 21st ICALP, LNCS 820, pages 166\u2013177, 1994."},{"key":"27_CR15","unstructured":"E. Graedel and I. Walukiewicz. Guarded fixed point logic. In Proc. 14th LICS, 1999."},{"issue":"4","key":"27_CR16","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BF01784885","volume":"3","author":"J. Y. Halpern","year":"1989","unstructured":"J. Y. Halpern and R. Fagin. Modelling knowladge and action in distributed systems. Distributed Computing, 3(4):159\u2013179, 1989.","journal-title":"Distributed Computing"},{"key":"27_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-64358-3","volume-title":"Proc. 10th CAV","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger, O. Kupferman, and S. Qadeer. From pre-historic to post-modern symbolic model checking. In Proc. 10th CAV, LNCS 1427, 1998."},{"key":"27_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/3-540-63141-0_18","volume-title":"Proc. 8th CONCUR","author":"D. Harel","year":"1997","unstructured":"D. Harel, O. Kupferman, and M. Y. Vardi. On the complexity of verifying concurrent transition systems. In Proc. 8th CONCUR, LNCS 1243, pages 258\u2013272, 1997. Springer-Verlag."},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"D. Harel and A. Pnueli. On the development of reactive systems. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 477\u2013498. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"27_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-59293-8_200","volume-title":"Proc. TAPSOFT\u2019 95","author":"B. Jonsson","year":"1995","unstructured":"B. Jonsson and Y.-K. Tsay. Assumption\/guarantee specifications in linear-time temporal logic. In Proc. TAPSOFT\u2019 95, LNCS 915, pages 262\u2013276, 1995."},{"key":"27_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03c0-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"27_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-60218-6_31","volume-title":"Proc. 6th CONCUR","author":"O. Kupferman","year":"1995","unstructured":"O. Kupferman and M. Y. Vardi. On the complexity of branchingmodular model checking. In Proc. 6th CONCUR, LNCS 962, pages 408\u2013422, 1995."},{"key":"27_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","volume-title":"Proc. 8th CAV","author":"O. Kupferman","year":"1996","unstructured":"O. Kupferman and M. Y. Vardi. Module checking. In Proc. 8th CAV, LNCS 1102, pages 75\u201386, 1996."},{"key":"27_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-63166-6_7","volume-title":"Proc. 9th CAV","author":"O. Kupferman","year":"1997","unstructured":"O. Kupferman and M. Y. Vardi. Module checking revisited. In Proc. 9th CAV, LNCS 1254, pages 36\u201347, 1997."},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Y. Vardi. Weak alternating automata and tree automata emptiness. In Proc. 30th STOC, pages 224\u2013233, 1998.","DOI":"10.1145\/276698.276748"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d-on the temporal logic of programs. In Proc. 7th POPL, pages 174\u2013185, 1980.","DOI":"10.1145\/567446.567463"},{"key":"27_CR28","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd International Joint Conference on Artificial Intelligence, pages 481\u2013489. British Computer Society, September 1971."},{"key":"27_CR29","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D. E. Muller","year":"1987","unstructured":"D. E. Muller and P. E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54,:267\u2013276, 1987.","journal-title":"Theoretical Computer Science"},{"key":"27_CR30","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D. E. Muller","year":"1995","unstructured":"D. E. Muller and P. E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69\u2013107, 1995.","journal-title":"Theoretical Computer Science"},{"key":"27_CR31","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th POPL, 1989.","DOI":"10.1145\/75277.75293"},{"key":"27_CR33","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th International Symp. on Programming","author":"J. P. Queille","year":"1981","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, LNCS 137, pages 337\u2013351, 1981."},{"key":"27_CR34","doi-asserted-by":"crossref","unstructured":"M. O. Rabin. Weakly definable relations and special automata. In Proc. Symp. Math. Logic and Foundations of Set Theory, pages 1\u201323. North Holland, 1970.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"27_CR35","first-page":"81","volume":"77","author":"P. J. G. Ramadge","year":"1989","unstructured":"P. J. G. Ramadge and W. M. Wonham. The control of descrete event systems. IEEE Transactions on Control Theory, 77:81\u201398, 1989.","journal-title":"IEEE Transactions on Control Theory"},{"issue":"3","key":"27_CR36","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"R. S. Streett","year":"1989","unstructured":"R. S. Streett and E. A. Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 81(3):249\u2013264, 1989.","journal-title":"Information and Computation"},{"key":"27_CR37","unstructured":"J. W. Thatcher. Tree automata: an informal survey. In A. V. Aho, editor, Currents in the theory of computing, pages 143\u2013172. Prentice-Hall, Englewood Cliffs, 1973."},{"issue":"2","key":"27_CR38","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M. Y. Vardi","year":"1986","unstructured":"M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182\u2013221, April 1986.","journal-title":"Journal of Computer and System Science"}],"container-title":["Lecture Notes in Computer Science","CONCUR\u201999 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48320-9_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T10:58:05Z","timestamp":1737543485000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48320-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664253","9783540483205"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-48320-9_27","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"19 April 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}