--- res: bibo_abstract: - 'Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas@eng' bibo_authorlist: - foaf_Person: foaf_givenName: Rajeev foaf_name: Alur, Rajeev foaf_surname: Alur - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Orna foaf_name: Kupferman, Orna foaf_surname: Kupferman bibo_doi: 10.1145/585265.585270 dct_date: 1997^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/0004-5411 dct_language: eng dct_publisher: Association for Computing Machinery (ACM)@ dct_title: Alternating-time temporal logic@ ...