AAAI Publications, Fifteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
Prompt Alternating-Time Epistemic Logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger

Last modified: 2016-03-30


In temporal logics, the operator F expresses that at some time in the future something happens, e.g., a request is eventually granted. Unfortunately, there is no bound on the time un- til the eventuality is satisfied which in many cases does not correspond to the intuitive meaning system designers have, namely, that F abstracts the idea that there is a bound on this time although its magnitude is not known. An elegant way to capture this meaning is through Prompt-LTL, which extends LTL with the operator FP ("prompt eventually"). We extend this work by studying alternating-time epistemic temporal logics extended with FP. We study the model-checking problem of the logic Prompt- KATL∗, which is ATL∗ extended with epistemic operators and prompt eventually. We also obtain results for the model-checking problem of some of its fragments. Namely, of Prompt-KATL (ATL with epistemic operators and prompt eventually), Prompt-KCTL∗ (CTL∗ with epistemic operators and prompt eventually), and finally the existential fragments of Prompt-KATL∗ and Prompt-KATL.


Multi Agent Systems, Formal Verification, Alternating Time Temporal Logic, Epsitemic Logic

Full Text: PDF