GaLOT - Game Logics for Open IT Environments
Project Members:
- Prof. Dr. Jürgen Dix
- Prof. Dr. Leon van der Torre
- Prof. Dr. Sjouke Mauw
Prof. Dr. Valentin Goranko
- PD Dr. Wojciech Jamroga
- Dr. Nils Bulling
- Dr. Matei Popovici
- Dipl.-Inf. Michael Köster
Funding:
432,400 Euros for 24 months financed by the Fonds National de la Recherche Luxembourg (FNR) and Deutsche Forschungsgemeinschaft (DFG).
Duration:
since 03/2013
Project Abstract
Game theory provides basic conceptual tools to assess abilities of players in scenarios involving interaction. On the other hand, mathematical logic has proved useful when addressing qualitative properties of systems. A number of strategic logics (or game logics) have been studied intensively in the last 15 years, that allow to specify properties of games in an abstract way. Unfortunately, most of them 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 this project, we address some of the questions. First, there are many different semantics for ability under uncertainty, but their exact relationship is still unclear. Secondly, there is no unifying framework. Thirdly, verification of abilities under uncertainty is known to be computationally hard, but little work has been done on tractable fragments of the logics. Fourthly, combining knowledge and strategies for stochastic models is almost untouched. We are going to investigate these basic threads by rigorous theoretical analysis. On a more practical level, we plan to provide a preliminary toolbox that allows for verification of information-related properties in open IT environments of relatively small scale.
It is important to emphasize that the focus of this project is theoretical rather than applied. However, study of strategic logics should be driven by practical context. This purpose will be served by scenarios from "IT Ecosystems", a big project which is currently being finished in Clausthal, Braunschweig and Hannover.
Kickoff Workshop
We had a Kickoff-Workshop from February 11-13 for the new project. In the following we summarize the talks as well as provide some slides.
Unifying our Research
Speaker: Jürgen Dix
Abstract: I reflect about several project proposals/submissions that we have worked out in the past few years.
In particular, I talk about the Simulation centre and the project jointly with Jörg Müller, on a Eurocores proposal about organizations, on a project with Peter Novak on planning as model checking and on a project Peter is working on right now in Delft. The aim of all this is to make these different strands of research more confluent and bring them together.
Concrete and Abstract Models of Effectivity in Games
Speaker: Wojtek Jamroga
Abstract: Game theory uses so called "strategic games" to represent the powers of players in game-like scenarios. These can be seen as concrete and simple models of what can happen when some agents interact. A much more abstract (but also more flexible) option is to use effectivity functions from social choice theory. An interesting question is: Which abstract models can be implemented by a concrete model? This kind of correspondence is usually characterized in so called "representation theorems".
In this talk, I present a well known result (Pauly's Representation Theorem), and show that it is in fact incorrect. Furthermore, I propose the correct characterization of the effectivity functions that can be implemented with strategic games.
The talk reports joint work with Valentin Goranko and Paolo Turrini.
Semantic variants of ATL: revocability of strategies
Speaker: Wojtek Jamroga
Abstract: In Alternating-time Temporal Logic (ATL), one can express statements about the strategic ability of an agent (or a coalition of agents) to achieve a given goal Phi. However, strategies in ATL are "revocable" in the sense that in the evaluation of the goal Phi the agents are no longer restricted by the strategy they have chosen in order to reach the state where the goal is evaluated. In this paper we consider alternative variants of ATL where strategies are *irrevocable*. The difference between revocable and irrevocable strategies shows up when we consider the ability to achieve a goal which, again, involves (nested) strategic ability. Furthermore, unlike in the standard semantics of ATL, memory plays an essential role in the semantics based on irrevocable strategies.
The talk reports joint work with Thomas Agotnes and Valentin Goranko.
A logical method for temporal knowledge representation and reasoning
Speaker: Matei Popovici
Abstract: Our method is aimed at representing and reasoning about time-dependent domains which have a non-Markovian evolution. More precisely, we refer to domains in which a future state cannot be predicted based on a finite number of past states. The method relies on a structure called temporal graph in order to store temporal information, and on a language (called LH) which allows expressing complex temporal relations between components of the temporal graph. The evaluation process of a LH formula is called LH model checking. We prove that the LH model checking problem is NP-complete. We also show that First-Order Logic cannot express temporal graph connectivity or the existence of a path between components of a temporal graph. We use this result to motivate the introduction and usage of the language LH.
Also, we describe several applications for LH such as error prediction in HPC systems. Finally, we introduce two game-theoretic concepts suitable for describing optimal time-dependent behavior in Multi-Agent Systems: the Nash Equilibrium and the Strong Nash Equilibrium. We provide complexity results for both solution concepts.
How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games
Speaker: Nils Bulling
Abstract: In my talk I propose a logical framework combining a game-theoretic study of abilities of agents to achieve quantitative objectives in multi-player games by optimizing payoffs or preferences on outcomes with a logical analysis of the abilities of players for achieving qualitative objectives of players, i.e., reaching or maintaining game states with desired properties. I show how to enrich concurrent game models with payoffs for the normal form games associated with the states of the model and propose a quantitative extension of the logic ATL* enabling the combination of quantitative and qualitative reasoning.
The talk reports joint work with Valentin Goranko.
Comparing Variants of Strategic Ability--How Uncertainty and Memory Influence General Properties of Games
Speaker: Nils Bulling
Abstract: Alternating-time temporal logic is a modal logic that allows to reason about agents' abilities in game-like scenarios. Semantic variants of ATL are usually built upon different assumptions about the kind of game that is played, including capabilities of agents (perfect vs. imperfect information, perfect vs. imperfect memory, etc.). ATL has been studied extensively in previous years; however, most of the research focused on model checking. Studies of other decision problems (e.g., satisfiability) and formal meta-properties of the logic (like axiomatization or expressivity) have been relatively scarce, and mostly limited to the basic variant of ATL where agents possess perfect information and perfect memory. In particular, comparison between different semantic variants of the logic is largely left untouched. In my talk I address the question whether different semantic variants of ATL generate different sets of validities (and equivalently, satisfiable formulae). More precisely, I show that different semantics of ability give rise to different validity sets. I argue that this issue is important for several reasons.
The talk reports joint work with Wojtek Jamroga.
Monitoring Norm Violations in Multi-Agent Systems
Speaker: Nils Bulling
Abstract: The use of norms is widely accepted as an effective approach to control and regulate the behaviour of agents in multi-agent systems. Existing work on normative multi-agent systems has mainly focussed on how norms can influence the behaviour of agents by assuming that the agents' behaviours are perfectly monitored. In this talk I focus on monitoring mechanisms, propose different types of monitors, provide a logical analysis of monitors, discuss the relations between monitors and norms to be monitored, and finally give an overview of computational aspects of norm monitoring.
The talk reports joint work with Mehdi Dastani and Max Knobbout
Alternating Epistemic Mu-Calculus
Speaker: Nils Bulling
Abstract: Alternating-time temporal logic s a well-known logic for reasoning about strategic abilities of agents.An important feature that distinguishes variants of ATL for imperfect information scenarios is that the standard fixed point characterizations of temporal modalities do not hold anymore.
In this talk, I show that adding explicit fixed point operators to the ``next-time'' fragment of ATL already allows to capture abilities that could not be expressed in ATL. I also illustrate that the new language allows to specify important kinds of abilities, namely ones where the agents can always recompute their strategy while executing it. Thus, the agents are not assumed to remember their strategy by definition, like in the existing variants of ATL.
Last but not least, I show that verification of such abilities can be cheaper than for all the variants of ``ATL with imperfect information'' considered so far.
The talk reports joint work with Wojtek Jamroga.
Lessons from IT Ecosystems
Speaker: Michael Köster
Abstract: IT Ecosystems is a project started by the Niedersächsische Technische Hochschule (NTH) (a joint venture of the TU Braunschweig, LU Hannover and TU Clausthal) and the NTH Focused Research School for IT Ecosystems.
I present the results of a subproject called LocCom (local communities in IT Ecosystems). In this project we developed methods, concepts, and tools for decentralized IT Ecosystems. Important outcomes are the development of new services and techniques to guarantee certain quality characteristics. We investigated adaptive techniques on all layers ranging from reconfigurable hardware via protocols up to modelling and inference methods. A principal objective is the modeling and implementation of generalized social networks based on mobile devices. Using services and information offered by these devices on one hand, and the needs and duties of users on the other hand, peers will be brought together. Further, recommendations concerning activities and usages will be generated automatically and tailored for the users, by taking into account the autonomy of users and devices.
The Multi-Agent Programming Contest
Speaker: Federico Schlesinger
Abstract: The Multi-Agent Programming Contest (MAPC) is an international, annual competition that aims to facilitate advances in programming multiagent systems (MAS) by (1) developing benchmark problems, (2) enabling head-to-head comparison of MAS's and (3) supporting educational efforts in the design and implementation of MAS's.
In this talk, I give an overview of the MAPC. I discuss first the contest´s modality and underlying infrastructure. Then, I briefly review the 8 years of the contents' history. Finally, I expand on the current "Agents on Mars" scenario.