Prompt Alternating-Time Epistemic Logics

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 F P ("prompt eventually"). We extend this work by studying alternating-time epistemic temporal logics extended with F P . 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.