Prompt alternating-time epistemic logics
Benjamin Aminof, Aniello Murano, Sasha Rubin, Florian Zuleger · Principles of Knowledge Representation and Reasoning · 2016
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 until 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.