Representation and Verification of Interaction and Knowledge (ReVINK)
EU FP7 project at Institute of Computer Science PAS
In this project, we propose to advance verification of strategic interaction by focusing more on models, and less on algorithms. Our research hypothesis is that model checking algorithms are approaching the limits of their potential when applied to arbitrary abstract models. On the other hand, certain representations can be more succinct or provide better structural properties. For instance, Reaction Systems encourage the modeler to abstract away from features of individual components. Likewise, Modular Interpreted Systems support additional structural information about separation of interacting components.
In order to systematically explore different representations, we identify 3 basic modeling levels for interaction and knowledge. The agent level focuses on actions, mental states, and social features of components. The effectivity level provides a uniform mathematical representation in terms of abstract ability. The population level focuses on interaction between large groups of similar components, and abstracts away from sporadic behaviors. We will begin by establishing mappings between models (and classes of models) from different levels. Based on these mappings, we will identify suitable model equivalences and abstractions that produce more succinct and/or structurally well-behaved models. Finally, we will investigate application of symbolic model checking algorithms to the resulting representations.
Keywords: verification of multi-agent systems, model checking, modal logic, computational complexity, algorithms and tools.
1. Levels of modelling, focused on a formal definition and study of different levels of representations for multi-agent systems.
The metamodel was defined, though not yet published. Given that the definition of the metamodel turned out relatively straightforward, we decided not to publish it in a separate paper. Instead, it will be most likely included in a book on specification and verification of strategic ability in multi-agent systems, to be prepared by Prof. Jamroga and Prof. Penczek. Moreover, we obtained significant technical results on the correspondence between different levels of representing strategic ability. Most notably, we have proposed three representation theorems that establish the correspondence between coalitional effectivity models and coalitional abilities that arise in concurrent game models. First, we characterized effectivity patterns in terms of state effectivity. Secondly, we proposed a representation theorem for path effectivity of memoryless agents. Thirdly, we studied path effectivity of agents with perfect recall of the past. The formal results allowed us to draw interesting conclusions about effectivity in imperfect information scenarios, as well as expose some deficiencies of the well-known stit models of interaction.
2. Verification of well-behaved Agent Level models, focused on development of verification techniques for representations that support better modelling of multi-agent systems.
Our work on this objective has produced scientific results of substantial significance. First, we obtained a semantic characterization of verification for open multi-agent systems by so called module checking. We showed how verification of strategic abilities can be defined for open MAS, and proposed automata-based algorithms for verification (together with theoretical complexity results). Secondly, some interesting theoretical results have been obtained for verification of special types of systems. We considered fully communicating coalitions and showed that the model checking problem reduces to the single-agent case. We also looked at the strategic ability to accumulate knowledge. Among the results, we showed how to embed the Hartley measure of uncertainty, well known in information theory, into the model checking problem for strategic logic. Thirdly, we reported the first step towards using fixpoint approximations of strategic ability under imperfect information.
A new research path concerned multi-valued models and semantics of strategic abilities. In multi-valued semantics, the value of a specification is defined over an arbitrary lattice of logical values. We showed that model checking in this very rich framework can be reduced to the standard 2-valued model checking by a simple and efficient translation scheme. What is more, the correctness and efficiency of the translation does not depend on the type of strategies that is used in the semantics, and thus applies to most (if not all) semantic variants of strategic logics. The theoretical results have been validated in a number of papers that apply strategic reasoning to analysis of information flow security and to specification of receipt-freeness and coercion resistance in voting protocols.
3. Abstraction, focused on obtaining useful reductions of agent models so that the verification becomes computationally easier.
This objective also produced significant results. We used models that abstract away from features of individuals, and allow for analysis of societal behavior in possibly adversarial interaction. Moreover, we investigated the shift from "micro" to "macro" view of a multi-agent system on the example of aggregation of agents' opinions, and proposed an iterative procedure of multi-agent aggregation. We also studied multi-valued abstraction, and its applicability for model checking of agents with imperfect information.
4. Unified semantics of MAS, focused on redefining the fundamental concepts in terms of effectivity functions, and validation of the result by specifications of security requirements in voting scenarios.
Towards this objective, we proposed and studied a novel variant of noninterference (a classical information security concept), based on the strategic ability of the "good" players to avoid information leakage. Furthermore, we proposed a concept of "effective security" where the security of the system is defined by the attacker's strategic ineffectivity to compromise the objective of the system. Finally, we showed how the classical concepts of receipt-freeness and coercion resistance in voting protocols can be formalized in terms of strategic effectivity of the participants.
The tangible outputs obtained in the project are listed on the project website (http://krak.ipipan.waw.pl/~wjamroga/projects/revink/). Of special note is the best paper award for our article on preventing coercion, indicating a successful crossover to the research community working on electronic voting procedures. The grant has also had a lasting effect on the career of the main researcher. Through the project, Wojciech Jamroga obtained his first professorship position, which he continues now, after ReVINK ended. Thanks to the collaboration that emerged within ReVINK, it was also possible to prepare and submit a successful proposal for a bilateral Polish-Luxembourgish project on verification of voting protocols (VoteVerif), which is currently carried out at ICS PAS and the University of Luxembourg, with the total budget of 1.2M EUR.
Surveys and book chapters:
Wojtek Jamroga home page
Institute of Computer Science PAS
Marie Sklodowska-Curie actions
Last modified 2016-10-29