Game Logics for Open IT Environments
Final Report Abstract
The INTER FNR/DFG project GaLOT (Game Logics for Open IT Environments) has been executed as a collaboration between researchers from University of Luxembourg and Clausthal University of Technology. The focus of the project was on how the formal frameworks of game theory and mathematical logic can contribute to our understanding of heterogeneous complex IT environments, and help to analyze, manage, and control them. Game theory provides basic conceptual tools to assess abilities of players in scenarios involving interaction. On the other hand, mathematical logic proved useful when addressing qualitative properties of systems. A number of strategic logics (or game logics) had been studied intensively since 1990s, that allow to specify properties of games in an abstract way. Unfortunately, most of the logics are based on models of perfect information. Such an assumption is unrealistic when it comes for distributed IT environments. Moreover, it makes the study of information security impossible because the notions of information and knowledge are not properly defined. A multitude of semantic variants were proposed in the recent years to combine knowledge and strategies in a single logical framework, but many questions remain open. In GaLOT we have addressed some of the questions. First, there are many different semantics for ability under uncertainty, but their exact relationship was still unclear. Secondly, there is no unifying framework. Thirdly, verification of abilities under uncertainty is known to be computationally hard, but little work had been done on tractable fragments of the logics. Fourthly, combining knowledge and strategies for stochastic models was almost untouched. We have investigated these basic threads by rigorous theoretical analysis. It is important to emphasize that the focus of the project was theoretical rather than applied. However, our study of strategic logics was driven by practical context. This purpose was served by scenarios from ”IT Ecosystems”, a large project which had been carried out as a joint effort of the universities in Clausthal, Braunschweig and Hannover. Most project goals have been achieved. The project produced a number of important results that advanced the understanding of strategic properties in heterogeneous IT environments, characterized by openness, dynamics, and uncertainty. The theoretical results were further used to come up with novel methods for analysis and verification of such environments. On the practical level, we proposed a number of algorithmic solutions that facilitate verification of information-related properties in small-scale open IT environments, together with a preliminary model checking tool. Some of the results have already been significantly cited by other researchers. Moreover, the outcomes of GaLOT provided the backbone of two subsequent international projects: • Representation and Verification of Interaction and Knowledge (ReVINK), and • Verification of Voter-Verifiable Voting Protocols (VoteVerif).
Publications
- (2014), Agents With Truly Perfect Recall: Expressivity and Validities. Proceedings of the 21st European Conference on Artificial Intelligence ECAI’14, pp. 177-182
Nils Bulling, Wojciech Jamroga, and Matei Popovici
- (2014), Comparing Variants of Strategic Ability: How Uncertainty and Memory Influence General Properties of Games. Journal of Autonomous Agents and Multi-Agent Systems, 28(3)*474–518
Nils Bulling and Wojciech Jamroga
(See online at https://doi.org/10.1007/s10458-013-9231-3) - (2015), A game-theoretic approach to compute stable topologies in mobile ad hoc networks. Journal of Logic and Computation, 25(3)*639–667
Nils Bulling, Matei Popovici
(See online at https://doi.org/10.1093/logcom/exu021) - (2015), Logics for Reasoning About Strategic Abilities in Multi-Player Games. In: J. van Benthem, S. Ghosh, R. Verbrugge (Eds.), Models of Strategic Reasoning. Logics, Games, and Communities. LNCS 8972, pp. 93-136
Nils Bulling, Valentin Goranko, and Wojciech Jamroga
- (2015), On the Boundary of (Un)decidability: Decidable Model- Checking for a Fragment of Resource Agent Logic. In the Proceedings of the 24th International Joint Conference on Artificial Intelligence, AAAI Press
Natasha Alechina, Nils Bulling, Brian Logan and Hoang Nga Nguyen
- (2015), Upwards closed dependencies in team semantics. Information and Computation, 245*124–135
Pietro Galliani
(See online at https://doi.org/10.1016/j.ic.2015.06.008) - Dynamic Logics of Imperfect Information: From Teams and Games to Transitions. In: van Ditmarsch H., Sandu G. (eds) Jaakko Hintikka on Knowledge and Game-Theoretical Semantics. Outstanding Contributions to Logic, vol 12. Springer, Cham, 2018, pp 299-315. 978-3-319-62863-9
Pietro Galliani
(See online at https://doi.org/10.1007/978-3-319-62864-6_12)
