Revisiting Ability-Based Bisimulation

Bisimulation is a crucial tool for investigating and understanding the semantic properties of labeled transition systems (LTSs) and relational models in general. In particular, it plays a fundamental role in characterizing model equivalence with respect to a given logical language and in guiding the construction of minimal models. In this paper, we study bisimulation in the context of a logic for expressing knowing-how assertions, which are related to an agent's ability to achieve a given goal. We begin by revisiting an existing notion of bisimulation for this logic and reformulating it using purely semantic clauses. We then establish adequacy results for this new notion. Next, we provide a computational analysis of the problem of checking whether two models are bisimilar. In particular, we show that this problem is PSPACE-complete. We also investigate two approaches to model minimization in this setting, each exhibiting different computational properties. Along the way, our systematic study of bisimulation yields additional by-product results, w.r.t., for example, the complexity of the definability problem for this logic.