Characterizing the expressivity of game description languages

Abstract

Bisimulations are a key notion to study the expressive power of a modal language. This paper studies the expressiveness of Game Description Language (GDL) and its epistemic extension EGDL through a bisimulations approach. We first define a notion of bisimulation for GDL and prove that it coincides with the indistinguishability of GDL-formulas. Based on it, we establish a characterization of the definability of GDL in terms of k-bisimulations. Then we define a novel notion of bisimulation for EGDL, and obtain a characterization of the expressive power of EGDL. In particular, we show that a special case of the bisimulation for EGDL can be used to characterize the expressivity of GDL. These characterizations not only justify the notions of bisimulation are appropriate for game description languages, but also provide a powerful tool to identify their expressive power.