Bisimulations for Logics of Strategies: A Study in Expressiveness and Verification
Résumé
In this paper we advance the state of the art on the subject of
bisimulations for logics of strategies. Bisimulations are a key
notion to study the expressive power of a modal language,
as well as for applications to system verification. In this contribution we present novel notions of bisimulation for several significant fragments of Strategy Logic (SL), and prove
that they preserve the interpretation of formulas in the corresponding fragments. In selected cases we are able to prove
that such bisimulations enjoy the Hennessy-Milner property.
Finally, we make use of bisimulations to study the expressiveness of the various fragment of SL, including the complexity
of their model checking problems.
Origine | Accord explicite pour ce dépôt |
---|