We introduce a logic to reason about strategic abilities in finite games under imperfect information. We interpret Alternating-time Temporal Logic on interpreted systems with final states, where agents only have partial observability of the system’s global state. We consider the model checking problem in this setting. We prove that the complexity results available for the case of infinite traces carry over to the finite traces case. We show that when only public actions are allowed, the verification problem under perfect recall becomes decidable. © 2019, Springer Nature Switzerland AG.
Imperfect Information in Alternating-Time Temporal Logic on Finite Traces / Belardinelli, F.; Lomuscio, A.; Murano, A.; Rubin, S.. - 11873 LNAI:(2019), pp. 469-477. (Intervento presentato al convegno 22nd International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2019 tenutosi a Turin; Italy nel 28-31 October 2019) [10.1007/978-3-030-33792-6_31].
Imperfect Information in Alternating-Time Temporal Logic on Finite Traces
Murano, A.;Rubin, S.
2019
Abstract
We introduce a logic to reason about strategic abilities in finite games under imperfect information. We interpret Alternating-time Temporal Logic on interpreted systems with final states, where agents only have partial observability of the system’s global state. We consider the model checking problem in this setting. We prove that the complexity results available for the case of infinite traces carry over to the finite traces case. We show that when only public actions are allowed, the verification problem under perfect recall becomes decidable. © 2019, Springer Nature Switzerland AG.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
