Scientific motivation and goals:

In many present-day computational systems, the correct functioning of the system depends on the environment in which it is operating. An open system is one which is designed to interact with an environment only partially known in advance. The verification of an open system therefore requires the concept of alternation between system and environment. Related concepts are the construction of winning-strategies in two-player games, agents operating under imperfect knowledge, and controller synthesis for reactive systems. Currently, there are several different (and separate) scientific communities working on the correctness problem for open systems; in the computer aided verification community, it has been recognized that the correctness problem for open systems can be modelled by alternating temporal logics and automata, and there are methods and tools being developed for these formalisms. In the multi-agent-systems community, extensions of agent description languages and logics are being made which focus on the interaction of their objects in an open environment. These languages allow to describe and verify e.g. cryptographic protocols and Byzantine fault-tolerant computing. In an industrial context, test suites and controllers are automatically synthesized from formal descriptions. These artefacts are used to test and control applications such as web services and embedded systems. The goal of this seminar is to bring together researchers from different communities working on the correctness of open systems, in order to enhance the interaction and exchange of ideas. The topics will concentrate on the intersection of the three fields:

• Alternating-time logics, automata and other formalisms for open systems
• Specification and verification of multi-agent systems
• Test generation and controller synthesis for open systems

The purpose of the seminar is to establish a common understanding of the problems in the different terminologies of these application areas. It is expected that the communication between the three fields will stimulate new results and techniques of both theoretical relevance and practical usefulness. Each participant is expected to contribute to the workshop by presenting a survey of his work and / or novel results in the context of the topics of the seminar as well as by giving some open problems he or she is currently working on. It is intended to collect the state of the art and perspectives in a special volume as a “manifesto” of open systems research.

More detailed description :

In many present-day computational systems, the correct functioning of the system depends on the environment in which it is operating. For example, a web service designed for the intranet may not function correctly for the internet, and a car tuned for the Sahara desert may not start in Alaska. Usually, in order to verify or test such a system one considers the composition of the system with its “maximal” or “worst case” environment. This approach, however, may not be adequate, since each possible environment has its own characteristics. Thus, the task of showing that a system is correct for every realistic environment may be different from showing its correctness in the maximal environment. It has been suggested to call a system open, if the main focus of attention is on its interaction with an unknown environment. Likewise, the composition of an open system and a particular environment is called closed, since there are no external interactions. For example, an embedded control circuit can be seen as an open system, since it connects with the plant via sensors and actuators. The loop consisting of controller and plant is a closed system. Often the envisaged environments for an open system are only partially specified; the system however should work correctly in each of them. The task of verifying an open system without closing it by its maximal environment was called module checking by some authors.

Currently, there are several different (and separate) scientific communities working on the correctness problem for open systems:

• In the computer aided verification community, it has been recognized that the correctness problem for open systems can be modelled by alternating temporal logics and automata, and there are methods and tools being developed for these formalisms.
• In the multi-agent-systems community, extensions of agent description languages and logics are being made which focus on the interaction of their objects in an open environment. These languages allow to describe and verify e.g. cryptographic protocols and Byzantine fault-tolerant computing.
• In an industrial context, test suites and controllers are automatically synthesized from formal descriptions. These artefacts are used to test and control applications such as web services and embedded systems.

Formally, the interaction between a system and its environment can be modelled as a two-player game. Thus, the module checking problem is related to the problem of finding winning strategies in certain two-player games. Another way of looking at the problem is as a multi-agent system where the strategy of one agent may be influenced by the strategy of the other agents, which is only partially known. Alternating temporal logics have been defined which allow to specify that an agent can attain a certain goal regardless of how the other agents behave. The satisfaction problem of alternating temporal logics is closely connected to the so-called controller synthesis problem: given a desired behaviour of a plant, the controller is an environment which guarantees that the plant behaves according to this specification. With suitable specification languages, the controller can be automatically generated from the specification. Moreover, it can be used as the test driver in a specification-based testing framework.

Although the problems, theories and procedures in the three abovementioned fields are closely related, it is our impression that there has not been sufficient interaction between the groups. The purpose of this seminar is to bring together researchers from the three fields. A common background for all participants is in logics and automatic verification, formal approaches to testing, and in application of state-of-the-art methods to validation of components. The main research topics to be discussed are

1. modelling formalisms for open systems,
2. logics for multi-agent systems, and
3. test generation and controller synthesis.

Correspondingly, the central themes of the seminar will be the expressiveness and complexity of alternating logics and automata, alternating epistemic logics and multi-player games, and the connections between alternation and the synthesis problem for reactive systems. The seminar, however, is not meant to be a purely theoretical one. Applications of the presented formalisms are in the description and verification of communication protocols for autonomous agents, in the semantics of composition for web services, and in algorithms for computer-aided verification tools. The organizers will try to obtain a “decent mix” of theoretical and practical presentations. In this seminar top level researchers and young researchers with a strong research perspective will congregate. Each participant is expected to contribute to the workshop by presenting his or her novel results in the context of the topics of the seminar as well as by giving some open problems he or she is currently working on. Since the participants are from separate communities, it is to be expected that some of the problems can be solved just by considering them from a different perspective.

Goals and research topics:

Here is a preliminary list of research topics which are to be tackled in this seminar.

• logics and automata for open systems
• component-based approaches and open systems
• correctness criteria for composition of open systems
• integration of verification and testing for open systems
• algorithms for module checking
• logics for multi-agent systems and multi-player games
• test case generation and controller synthesis
• synthesis of winning strategies for games

On the applied side, there are some topics which might be addressed depending on the current interest of the participants:

• testing of epistemic communication protocols
• verification and synthesis based on alternating automata
• correctness and test oracle synthesis for web services
• real-time constraints in web services