Bisimulations for Logics of Strategies: A Study in Expressiveness and Verification
Francesco Belardinelli, Cătălin Dima, Aniello Murano · 2018
In this paper we advance the state of the art on the subject ofbisimulations for logics of strategies. Bisimulations are a keynotion to study the expressive power of a modal language,as well as for applications to system verification. In this con-tribution we present novel notions of bisimulation for sev-eral significant fragments of Strategy Logic (SL), and provethat they preserve the interpretation of formulas in the cor-responding fragments. In selected cases we are able to provethat such bisimulations enjoy the Hennessy-Milner property.Finally, we make use of bisimulations to study the expressive-ness of the various fragment of SL, including the complexityof their model checking problems.