We present a translation that reduces epistemic operators to strategic operators in the context of model checking. The translation is a refinement of one that we proposed some time ago, and it improves on the previous scheme in two ways. First, it does not suffer any blowup in the length of formulae (the previous one). Second, the new translation is defined in a more general setting: additional constraints can be imposed on strategy profiles that agents can execute. We show the applicability of such a general translation on the case of strategic abilities under imperfect information.
Keywords: multi-agent systems, alternating-time temporal logic, epistemic logic, model checking.
|Computational Intelligence Group @ Technical University of Clausthal|
|Human Media Interaction Group @ University of Twente|
|Computer Science Group @ University of Gdansk||Last modified 2008-08-09|