1,721,105 research outputs found
An Unexpected Journey: Towards Runtime Verification of Multiagent Systems and Beyond
No full textThe Trace Expression formalism derives from works started in 2012 and is
mainly used to specify and verify interaction protocols at runtime, but other
applications have been devised. More specically, this thesis describes how
to extend and apply such formalism in the engineering process of distributed
articial intelligence systems (such as Multiagent systems).
This thesis extends the state of the art through four dierent contributions:
1. Theoretical: the thesis extends the original formalism in order to represent
also parametric and probabilistic specications (parametric trace
expressions and probabilistic trace expressions respectively).
2. Algorithmic: the thesis proposes algorithms for verifying trace expressions
at runtime in a decentralized way. The algorithms have been
designed to be as general as possible, but their implementation and
experimentation address scenarios where the modelled and observed
events are communicative events (interactions) inside a multiagent system.
3. Application: the thesis analyzes the relations between runtime and static
verication (e.g. model checking) proposing hybrid integrations in both
directions. First of all, the thesis proposes a trace expression model
checking approach where it shows how to statically verify LTL property
on a trace expression specication. After that, the thesis presents a
novel approach for supporting static verication through the addition
of monitors at runtime (post-process).
4. Implementation: the thesis presents RIVERtools, a tool supporting the
writing, the syntactic analysis and the decentralization of trace expressions
Reasoning about Decidability of Strategic Logics with Imperfect Information and Perfect Recall Strategies
Full text linkIn logics for strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall strategies. In this work, we show the combination of two techniques to approximate the verification of Alternating-time Temporal Logic (ATL∗) under imperfect information and perfect recall, which is known to be undecidable. Given a model M and a formula φ, we propose a verification procedure that generates sub-models of M in which each sub-model M′ satisfies a sub-formula φ′ of φ and the verification of φ′ in M′ is decidable. Then, we use CTL∗ model checking to provide a verification result of φ on M. In case the previous step does not give a final result, we exploit a runtime verification mechanism to provide some intermediate result. We prove that our procedure is sound and in the same complexity class of ATL∗ model checking under perfect information and perfect recall. Moreover, we present a tool that uses our procedure and provide experimental results
Agreement Games in Multi-Agent Systems
No full textMulti-Agent Systems are composed of distributed intelligent components, known as agents. In real-world scenarios, these agents often lack sufficient resources or access to global system information to achieve their objectives. In such cases, intelligent information sharing can enable agents to collaborate effectively and reach their goals. This work introduces the concept of Agreement Game as a framework to address these challenges
Improving flexibility and dependability of remote patient monitoring with agent-oriented approaches
No full textContext: Remote Patient Monitoring (RPM) enables physicians to perform diagnosis and/or treatment remotely through sensors connected via a
communication network. Dependability and flexibility are recognized as two key technological requirements for RPM take off. Research question: We address the questions of how RPM systems designed and implemented as multiagent systems (MASs) can ensure flexibility and dependability, and which agent-oriented approach – if any – is more suitable to achieve this goal. Method: We analyzed five state-of-the-art agent-oriented approaches suitable to
engineer dependable and/or flexible systems. We planned to adopt the “winner” approach to realize a working prototype able to show the potential of an agent-oriented approach to RPM.
Results: No approach among the five dominates the others w.r.t. all the ten features that drove our analysis. In absence of a winner, we selected the approach we are more familiar with, namely parametric trace expressions. We used them to verify properties modeling existing medical guidelines and to developed a prototype where newborns suffering from hypoglycemia must be continuously monitored at home.
Conclusions: Parametric trace expressions proved to be suitable for engineering flexible and dependable RPM systems. This finding can be generalized: agent-oriented approaches showing features similar to those of parametric trace expressions can serve to achieve the same goal
Decentralizing MAS Monitoring with DecAMon
No full textWe describe DecAMon, an algorithm for decentralizing the monitoring of the MAS communicative behavior described via an Agent Interaction Protocol (AIP). If some agents in the MAS are grouped together and monitored by the same monitor, instead of individually, a partial decentralization of the monitoring activity can still be obtained even if the "unique point of choice" (a.k.a. local choice) and "connectedness for sequence" (a.k.a. causality) coherence conditions are not satisfied by the protocol.
Given an AIP specification, DecAMon outputs a set of "Monitoring Safe Partitions" of the agents, namely partitions P which ensure that having one monitor in charge for each group of agents in P allows detection of all and only the protocol violations that a fully centralized monitor would detect.
In order to specify AIPs we use "trace expressions": this formalism can express event traces that are not context-free and can model both synchronous and asynchronous communication just by changing the underlying notion of event
Decentralizing MAS Monitoring with DecAMon
No full textWe describe DecAMon, an algorithm for decentralizing the monitoring of the MAS communicative behavior described via an Agent Interaction Protocol (AIP). If some agents in the MAS are grouped together and monitored by the same monitor, instead of individually, a partial decentralization of the monitoring activity can still be obtained even if the "unique point of choice" (a.k.a. local choice) and "connectedness for sequence" (a.k.a. causality) coherence conditions are not satisfied by the protocol.
Given an AIP specification, DecAMon outputs a set of "Monitoring Safe Partitions" of the agents, namely partitions P which ensure that having one monitor in charge for each group of agents in P allows detection of all and only the protocol violations that a fully centralized monitor would detect.
In order to specify AIPs we use "trace expressions": this formalism can express event traces that are not context-free and can model both synchronous and asynchronous communication just by changing the underlying notion of event
Resource Action-Based Bounded ATL: A New Logic for MAS to Express a Cost Over the Actions
No full text- …
