On Bisimulation in Modal Logics for Games on Graphs: An Algorithmic Study
摘要
We have been discussing modal operators modelling structural changes in graphs represented as moves in different graph games. For this work, the focus is on the corresponding notions of bisimulation that explore the similarities in these graph structures. We provide an algorithmic study of the same, for sabotage modal logic vis-à-vis the sabotage games in particular, paving the way for a general study to check whether different graph game models involving certain structural changes are bisimilar. This, in turn, provides us with the corresponding concepts of logical equivalences, especially for such model-changing modal logics. Through our algorithmic analyses we provide a PSPACE upper bound of the bisimulation/model comparison problem of sabotage modal logic and then generalise the result to similar other model-changing modal logics. We also provide some insight into the higher complexity of the model comparison problem for these logics compared to that for the basic modal logic.