Bisimilarity in Logics for Strategic Reasoning
Nash equilibrium is the standard solution concept for multi-player games. Such games have multiple applications in Logic and Semantics, Artificial Intelligence and Multi-Agent Systems, and Verification and Computer Science. Unfortunately, Nash equilibria is not preserved under bisimilarity, one of the most important behavioural equivalences for concurrent systems. In a recent paper it was shown that this problem may not arise when certain models of strategies are considered. In this project the aim is to investigate further implications of considering the new model of strategies. For instance, whether a number of logics for strategic reasoning become invariant under bisimilarity if the new model of strategies is considered, whether some logics that are unable to express Nash equilibria can do so with respect to the new model of strategies, and whether the results already obtained still hold more complex classes of systems, for instance, where nondeterminism has to be considered.
Prerequisites: Discrete Mathematics, Introduction to Formal Proof, Logic and Proof
Desirable: Computer-Aided Formal Verification, Computational Complexity
Project type: theory