Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Alternating-time Temporal Logic
| |
|
Alternating-time Temporal Logic
Rajeev Alur6, 7  , Thomas A. Henzinger8 and Orna Kupferman8
| (6) |
Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, 19104 |
| (7) |
Bell Laboratories, Computing Science Research Center, Murray Hill, NJ, 07974 |
| (8) |
Department of Electrical Engineering and Computer Sciences, University of California, Berkeley, CA, 94720 |
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.
Depending on whether we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time
temporal logics ATL and ATL. We interpret the formulas of ATL and ATL over alternating transition systems. While in ordinary transition systems, each transition corresponds to a possible step of the system, in alternating transition
systems, each transition corresponds to a possible move in the game between the system and the environment. Fair alternating
transition systems can capture both synchronous and asynchronous compositions of open systems. For synchronous systems, the
expressive power of ATL beyond CTL comes at no cost: the model-checking complexity of synchronous ATL is linear in the size
of the system and the length of the formula. The symbolic model-checking algorithm for CTL extends with few modifications
to synchronous ATL, and with some work, also to asynchronous ATL, whose model-checking complexity is quadratic. This makes
ATL an obvious candidate for the automatic verification of open systems. In the case of ATL, the model-checking problem is
closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time for both synchronous
and asynchronous systems.
A preliminary version of this paper appeared in the Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (FOCS 1997), pp. 100–109.
This work was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant
CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892,
and by the SRC contract 97-DC-324.041.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|