[{"intvolume":"      1466","extern":"1","abstract":[{"text":"Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as “Does the implementation refine the set A of specification components without constraining the components not in A?” In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components.","lang":"eng"}],"volume":1466,"title":"Alternating refinement relations","scopus_import":"1","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:42Z","conference":{"start_date":"1998-09-08","name":"CONCUR: Concurrency Theory","end_date":"1998-09-11","location":"Nice, France"},"publist_id":"104","type":"conference","day":"01","citation":{"apa":"Alur, R., Henzinger, T. A., Kupferman, O., &#38; Vardi, M. (1998). Alternating refinement relations. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 163–178). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055622\">https://doi.org/10.1007/BFb0055622</a>","ista":"Alur R, Henzinger TA, Kupferman O, Vardi M. 1998. Alternating refinement relations. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 163–178.","chicago":"Alur, Rajeev, Thomas A Henzinger, Orna Kupferman, and Moshe Vardi. “Alternating Refinement Relations.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:163–78. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055622\">https://doi.org/10.1007/BFb0055622</a>.","ama":"Alur R, Henzinger TA, Kupferman O, Vardi M. Alternating refinement relations. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:163-178. doi:<a href=\"https://doi.org/10.1007/BFb0055622\">10.1007/BFb0055622</a>","short":"R. Alur, T.A. Henzinger, O. Kupferman, M. Vardi, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–178.","ieee":"R. Alur, T. A. Henzinger, O. Kupferman, and M. Vardi, “Alternating refinement relations,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 163–178.","mla":"Alur, Rajeev, et al. “Alternating Refinement Relations.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 163–78, doi:<a href=\"https://doi.org/10.1007/BFb0055622\">10.1007/BFb0055622</a>."},"doi":"10.1007/BFb0055622","quality_controlled":"1","oa_version":"None","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"},{"full_name":"Vardi, Moshe","first_name":"Moshe","last_name":"Vardi"}],"acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9504469, CCR-9628400, and CCR-9700061, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, by the SRC contract 97-DC-324.041, and by a grant from the Intel Corporation.","status":"public","date_published":"1998-01-01T00:00:00Z","year":"1998","publication_identifier":{"isbn":["978-3-540-64896-3"]},"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","page":"163 - 178","publication_status":"published","date_updated":"2022-08-23T09:50:34Z","_id":"4603","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","month":"01"},{"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","page":"439 - 454","article_processing_charge":"No","year":"1998","publication_identifier":{"isbn":["978-3-540-64896-3"]},"status":"public","date_published":"1998-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"4515","date_updated":"2022-08-23T14:24:08Z","publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","month":"01","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","abstract":[{"text":"We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.","lang":"eng"}],"volume":1466,"extern":"1","intvolume":"      1466","date_created":"2018-12-11T12:09:15Z","conference":{"location":"Nice, France","end_date":"1998-09-11","name":"CONCUR: Concurrency Theory","start_date":"1998-09-08"},"language":[{"iso":"eng"}],"alternative_title":["LNCS"],"scopus_import":"1","title":"It's about time: Real-time logics reviewed","citation":{"ama":"Henzinger TA. It’s about time: Real-time logics reviewed. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:439-454. doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>","ieee":"T. A. Henzinger, “It’s about time: Real-time logics reviewed,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 439–454.","short":"T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–454.","chicago":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:439–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>.","apa":"Henzinger, T. A. (1998). It’s about time: Real-time logics reviewed. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 439–454). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>","ista":"Henzinger TA. 1998. It’s about time: Real-time logics reviewed. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 439–454.","mla":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–54, doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>."},"day":"01","type":"conference","publist_id":"214","oa_version":"None","quality_controlled":"1","doi":"10.1007/BFb0055640"}]