REMASTER: formal methods for Realistic Environments in MAS

Multi-Agent Systems (MAS) consist of several interacting entities that are trying to achieve common or individual goals. Since agents could be software-modules, people, or robots, they are fast becoming ubiquitous in all aspects of today`s technological society, e.g., unmanned vehicles, cloud computing, peer-to-peer computing. In addition, many biological systems can be naturally modeled as MAS. Agents are usually situated in some environment, e.g., physical space like robots in a plant, or virtual environments like computer networks. As the field of MAS has matured, it has shifted from experiments in building individual or multi-agent systems to rigorous theoretical foundations based on sophisticated computational models. In order to analyze the correctness of MAS, the MAS community has started employing formal methods tools based on mathematical logic and other related mathematical formalisms that have been extremely successful in reasoning about all possible behaviors of a system model (e.g., modern microprocessors) in a way which is impossible using standard techniques such as testing. In classical formal methods, a program may either be correct or not. However, in practice, one program may be preferred over another even if both are correct: it may be faster, more efficient, or more resilient. Measuring such requirements is the subject of much recent research in the formal methods community. The need for similar reasoning in MAS is compelling. In particular, MAS should be resilient with respect to their environment, i.e., they should tolerate uncertainty and change. To illustrate, consider for example the Google self-driving cars. These cars use ``super-maps`` which are a complete 3D digitization of the road environment, with a precision of a few inches, including such information as the height of each meter of curb, and the exact position (in 3D space, with the same ultra-precision) of every traffic light. Also, these cars cannot address changes, such as obey temporary traffic lights. Thus, their basic mode of operation assumes a fully-known static environment. Contrast this with a human driver who is able to drive in unfamiliar and changing environments. The current state of research is that very little was done to develop and apply formal methods to automatically analyze or synthesize (i.e., to automatically generate a system from its specification) MAS that are resilient with respect to their environments. The aim of this project is to bridge this gap, i.e., to develop formal methods for reasoning about MAS operating in partially known and/or dynamic environments, in order to better meet the needs of the MAS community for automatic and rigorous design of correct and reliable systems.

A central theme in artificial intelligence (AI) revolves around the concept of an agent, which is any entity that can interact with other agents and/or the environment using sensors and actuators, and is guided by the need or desire to achieve a certain goal or perform a certain task. A system that consists of a group such agents is called a multi-agent system (MAS). Examples include software agents on the Internet, driverless cars, humans or software playing multi-player card games, and robots exploring new and dangerous environments. In all these examples, agents are situated and supported by some environment which provides the surrounding conditions for agents to exist and operate. Aspects of the environment include for example the physical-environment that supports the agents physically (e.g., physical roads, network links); a communication-environment that supports agent communication (e.g., rules, means and protocols); or a social-environment that reflects organizational structure in terms of roles, groups, etc. The ever increasing deployment of AI agents in our society, and the inherent difficulties in designing such agents to operate safely and correctly in the complex environments in which they are being deployed, has recently led to the understanding of the importance of incorporating tools and techniques of formal methods, to the design and analysis of artificial agents and their interactions with their environment. Formal methods provide algorithms, based mainly on logic and automata, for automatically determining whether a mathematical model of a system satisfies a specification, formally expressed in mathematical logic (model-checking) or, alternatively, to automatically construct a system that satisfies a given specification (synthesis). The central results of this project were the development of new formal methods for reasoning about agents operating in complex environments: for example, novel algorithms for model-checking of MAS operating in environments with unknown physical infrastructure were developed, a new specification logic called Probabilistic Strategy Logic for reasoning about MAS operating in stochastic environments was introduced and studied, and core issues of how the environment should be modeled/viewed were revisited, obtaining new and important insights and synthesis algorithms. In addition, a new promising research direction called best-effort synthesis was initiated (and core basic results obtained) with the aim of formally and rigorously addressing the fundamental question of what should an agent do if it cannot ensure that it will achieve its goal regardless of the way the environment acts.