Search

This paper casts coordination of a team of robots within the framework of game theoretic learning algorithms. A novel variant of fictitious play is proposed, by considering multi-model adaptive filters as a method to estimate other players’ strategies. The proposed algorithm can be used as a coordination mechanism between players when they should take decisions under uncertainty. Each player chooses an action after taking into account the actions of the other players and also the uncertainty. In contrast, to other game-theoretic and heuristic algorithms for distributed optimisation, it is not necessary to find the optimal parameters of the algorithm for a specific problem a priori. Simulations are used to test the performance of the proposed methodology against other game-theoretic learning algorithms.

The ambitious aim of CONNECT is to achieve universal interoperability between heterogeneous Networked Systems by means of on-the-fly synthesis of the CONNECTors through which they communicate. The goal of WP5 within CONNECT is to ensure that the non-functional properties required at each side of the connection going to be established are fulfilled, including dependability, performance, security and trust, or, in one overarching term, CONNECTability. To model such properties, we have introduced the CPMM meta-model which establishes the relevant concepts and their relations, and also includes a Complex Event language to express the behaviour associated with the specified properties. Along the four years of project duration, we have developed approaches for assuring CONNECTability both at synthesis time and at run-time. Within CONNECT architecture, these approaches are supported via the following enablers: the Dependability and Performance analysis Enabler, which is implemented in a modular architecture supporting stochastic verification and state-based analysis. Dependability and performance analysis also relies on approaches for incremental verification to adjust CONNECTor parameters at run-time; the Security Enabler, which implements a Security-by-Contract-with-Trust framework to guarantee the expected security policies and enforce them accordingly to the level of trust; the Trust Manager that implements a model-based approach to mediate between different trust models and ensure interoperable trust management. The enablers have been integrated within the CONNECT architecture, and in particular can interact with the CONNECT event-based monitoring enabler (GLIMPSE Enabler released within WP4) for run-time analysis and verification. To support a Model-driven approach in the interaction with the monitor, we have developed a CPMM editor and a translator from CPMM to the GLIMPSE native language (Drools). In this document that is the final deliverable from WP5 we first present the latest advances in the fourth year concerning CPMM, Dependability&Performance Analysis, Incremental Verification and Security. Then, we make an overall summary of main achievements for the whole project lifecycle. In appendix we also include some relevant articles specifically focussing on CONNECTability that have been prepared in the last period.

This document is the final report on use and dissemination of foreground, part of the CONNECT final report. The document provides the lists of: publications, dissemination activities, and exploitable foreground

This document is the final publishable summary report, part of the CONNECT final report.

In this deliverable, we document the progress of WP2 during the fourth year of the CONNECT project. Following the last reviews' recommendations, the work is organized into two main streams. One stream concerns a quantitative extension of the compositional specification theory devised during the previous two years, while the other integrates the WP2 CONNECTor algebra with the specification theory so as to support WP3 CONNECTor synthesis. In particular, the assume-guarantee reasoning framework developed for the compositional specification theory ensures that a CONNECTed system preserves global safety properties by just checking the local properties of its constituent components. The proposed quantitative extension of the compositional specification theory allows the modeling of the real-time performance of networked systems, in addition to enabling the synthesis of CONNECTors that are compatible with both the functional behavior and timing constraints of their environments. Finally, in order to integrate the CONNECTor algebra with the specification theory so as to support WP3 synthesis, we defined a method for the automated synthesis of modular CONNECTors. We prove that the behavior of such a CONNECTor is equivalent to the behaviour of a monolithic WP3 CONNECTor. All of the work is evaluated through an application to relevant CONNECT scenarios, e.g., the GMES (Global Monitoring for Environment and Security) scenario.

We supply details of a compositional specification theory we have been working on for modelling connectors and components. This supports the operations of parallel composition, for examining the structural behaviour of networked systems, logical conjunction, for supporting independent development of components, and quotient for incremental development in the form of component/connector synthesis. Our framework, a portion of which is conceptually similar to interface automata, is unique in that we've provided the first definition of quotient that can act on components exhibiting non-determinism, as well as the first definition of conjunction on this flavour of model. A refinement preorder corresponding to safe-substitutivity allows for the seamless interchanging of components and connectors without violating environmental assumptions. Our formulation of refinement also ensures that the framework enjoys strong algebraic properties. These are necessary for reasoning about components and connectors in a compositional manner.

The CONNECT project aims to develop a novel network infrastructure to allow heterogeneous networked systems to freely communicate with each other via on-the-fly synthesis of emergent connectors. The role of Work Package 2 (WP2) is to investigate the foundations and verification methods for composable connectors, so that support is provided for composition of networked systems, whilst enabling automated learning, reasoning and synthesis. In the second year, we focused our attention on providing an underpinning for a framework capable of supporting the dimensions of interest to the project, and the generalisation of assume-guarantee properties beyond probabilistic safety properties, in addition to supporting the automated learning of assumptions. In this deliverable, we report on work carried out in two streams, compositional theory of connector behaviours and compositional assume-guarantee verification for probabilistic automata, which we are beginning to bring together. At the theory level, we first considered several probabilistic models, focusing on their interactive behaviour and asynchronous parallel composition. We then conducted a survey of the different formalisms of component models from the viewpoint of whether they supported a number of operators (e.g. parallel composition, conjunction and quotient) and a refinement relation. Based on this, we concluded that interface automata were one of the most amenable formalisms for basing an algebra of CONNECTors upon. We have formulated a preliminary (non-quantitative) connector algebra for resolving protocol mismatches based on interface automata. A software tool IAAnalyzer was implemented to allow users to create interface automata models using the connector algebra. In order to address the need for a quantitative extension, we have proposed a specification theory based on a probabilistic extension of interface automata. In the second stream, we continued our work on compositional assume-guarantee verification for probabilistic automata, extending the framework to allow, as assumptions and guarantees, a broader class of quantitative multi-objective properties which include probabilistic liveness and expected rewards. We also proposed a novel learning technique based on the L* algorithm, which automatically generates probabilistic (safety) assumptions using the results of queries executed by a probabilistic model checker. These two techniques have been implemented for PRISM, a well-known probabilistic model checker. Finally, we have laid the foundations for a comprehensive framework capable of modelling the quantitative (in particular the probabilistic) behaviour of arbitrary components and associated compositional assume-guarantee proof rules. Connectors arise as certain types of components. This framework is intended to integrate the two streams of work.

The aim of CONNECT is to achieve universal interoperability between heterogeneous Networked Systems. For this, the non-functional properties required at each side of the connection going to be established must be fulfilled. By the one inclusive term "CONNECTability" we comprehend properties belonging to all four non-functional concerns of interest for CONNECT, namely dependability, performance, security and trust. We model such properties in conformance with a meta-model which establishes the relevant concepts and their relations. Then, building on the conceptual models proposed in the first year in Deliverable D5.1, in this document we present the approaches developed for assuring CONNECTability both at synthesis time and at runtime. The contributions include: the Dependability&Performance analysis Enabler, for which we release a modular architecture supporting stochastic verification and state-based analysis; incremental verification and event-based monitoring for runtime analysis; a model-based approach to interoperable trust management; the Security-by-Contract-with-Trust framework, which guarantees and enforces the expected trust levels and security policies.

International audience; We investigate the problem of the verification of multiagent systems by means of parallel algorithms. We present algorithms for CTLK, a logic combining branching time temporal logic with epistemic modalities. We report on an implementation of these algorithms and present the experimental results obtained. The results point to a significant speed-up in the verification step.

International audience; We investigate partial order reduction for model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model chechking step and show preservation properties. We evaluate the technique by discussing the experimental results obtained against well-known examples in the MAS literature

This is the first deliverable of WP5, which covers Conceptual Models for Assessment & Assurance of Dependability, Security and Privacy in the Eternal CONNECTed World. As described in the project DOW, in this document we cover the following topics: • Metrics definition • Identification of limitations of current V&V approaches and exploration of extensions/refinements/ new developments • Identification of security, privacy and trust models WP5 focus is on dependability concerning the peculiar aspects of the project, i.e., the threats deriving from on-the-fly synthesis of CONNECTors. We explore appropriate means for assessing/guaranteeing that the CONNECTed System yields acceptable levels for non-functional properties, such as reliability (e.g., the CONNECTor will ensure continued communication without interruption), security and privacy (e.g., the transactions do not disclose confidential data), trust (e.g., Networked Systems are put in communication only with parties they trust). After defining a conceptual framework for metrics definition, we present the approaches to dependability in CONNECT, which cover: i) Model-based V&V, ii) Security enforcement and iii) Trust management. The approaches are centered around monitoring, to allow for on-line analysis. Monitoring is performed alongside the functionalities of the CONNECTed System and is used to detect conditions that are deemed relevant by its clients (i.e., the other CONNECT Enablers). A unified lifecycle encompassing dependability analysis, security enforcement and trust management is outlined, spanning over discovery time, synthesis time and execution time.

The CONNECT Integrated Project aims to develop a novel networking infrastructure that will support composition of networked systems with on-the-fly connector synthesis. The role of this work package is to investigate the foundations and verification methods for composable connectors. In this deliverable, we set the scene for the formulation of the modelling framework by surveying existing connector modelling formalisms. We covered not only classical connector algebra formalisms, but also, where appropriate, their corresponding quantitative extensions. All formalisms have been evaluated against a set of key dimensions of interest agreed upon in the CONNECT project. Based on these investigations, we concluded that none of the modelling formalisms available at present satisfy our eight dimensions. We will use the outcome of the survey to guide the formulation of a compositional modelling formalism tailored to the specific requirements of the CONNECT project. Furthermore, we considered the range of non-functional properties that are of interest to CONNECT, and reviewed existing specification formalisms for capturing them, together with the corresponding modelchecking algorithms and tool support. Consequently, we described the scientific advances concerning model-checking algorithms and tools, which are partial contribution towards future deliverables: an approach for online verification (part of D2.2), automated abstraction-refinement for probabilistic realtime systems (part of D2.2 and D2.4), and compositional probabilistic verification within PRISM, to serve as a foundation of future research on quantitative assume-guarantee compositional reasoning (part of D2.2 and D2.4).