Qais Hamarneh

Strategy Logic is a highly expressive logic which captures multi-agent behavior in concurrent game systems whilst treating the agents’ strategies as first-class objects. In this work, we analyze Mogavero’s Strategy Logic (SL) and its less expressive but easier to verify fragments, aiming to develop game-theoretic semantics (GTS) for it. Taking advantage of previously developed GTS for the related Alternating-Time Temporal Logic (ATL), we distinguish unbounded, finitely bounded and ordinally bounded games to create individual GTS. We adapt previous approaches to the SL setting taking into consideration the change in domain, as SL considers agents’ strategies first-order objects, and SL’s highly undecidable satisfiability problem.