27 citations · 81 across the 20 of their papers we have counts for
20 papers
A New Syntax and Semantics for Probabilistic Trace Expressions
Davide Ancona, Angelo Ferrando, Viviana Mascardi
Runtime Verification (RV) techniques are typically defined under the assumption of complete observability of system executions. In many realistic settings, however, monitors must o…
RV4Chatbot: Are Chatbots Allowed to Dream of Electric Sheep?
Andrea Gatti, Viviana Mascardi, Angelo Ferrando
Chatbots have become integral to various application domains, including those with safety-critical considerations. As a result, there is a pressing need for methods that ensure cha…
Scalable Verification of Strategy Logic through Three-valued Abstraction
Francesco Belardinelli, Angelo Ferrando, Wojciech Jamroga +2
The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle…
Proceedings of the Third Workshop on Agents and Robots for reliable Engineered Autonomy
Angelo Ferrando, Rafael Cardoso
The volume comprises the proceedings of the Third Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2023), held alongside the 26th European Conference on Artific…
Ain't No Stopping Us Monitoring Now
Luca Ciccone, Francesco Dagnino, Angelo Ferrando
Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable proper…
Extending Attack-Fault Trees with Runtime Verification
Rafael C. Cardoso, Angelo Ferrando, Michael Fisher
Autonomous systems are often complex and prone to software failures and cyber-attacks. We introduce RVAFTs, an extension of Attack-Fault Trees (AFTs) with runtime events that can b…
A Compositional Approach to Verifying Modular Robotic Systems
Matt Luckcuck, Marie Farrell, Angelo Ferrando +3
Robotic systems used in safety-critical scenarios often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic…
RV4JaCa -- Runtime Verification for Multi-Agent Systems
Debora C. Engelmann, Angelo Ferrando, Alison R. Panisson +3
This paper presents a Runtime Verification (RV) approach for Multi-Agent Systems (MAS) using the JaCaMo framework. Our objective is to bring a layer of security to the MAS. This la…
Proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy
Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini +2
This volume contains the proceedings of the Second Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2022), co-located with the 31st International Joint Conferen…
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
Angelo Ferrando, Vadim Malvone
Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify…
Towards the Verification of Strategic Properties in Multi-Agent Systems with Imperfect Information
Angelo Ferrando, Vadim Malvone
In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a techn…
Towards Partial Monitoring: It is Always too Soon to Give Up
Angelo Ferrando, Rafael C. Cardoso
Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour i…
MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest
Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini +3
In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used…
Can determinism and compositionality coexist in RML?
Davide Ancona, Angelo Ferrando, Viviana Mascardi
Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specificat…
Can determinism and compositionality coexist in RML? (extended version)
Davide Ancona, Angelo Ferrando, Viviana Mascardi
Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specificat…
Proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy
Rafael C. Cardoso, Angelo Ferrando, Daniela Briola +2
This volume contains the proceedings of the First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA 2020), co-located with the 24th European Conference on Artifi…
Heterogeneous Verification of an Autonomous Curiosity Rover
Rafael C. Cardoso, Marie Farrell, Matt Luckcuck +2
The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to i…
LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest
Rafael C. Cardoso, Angelo Ferrando, Fabio Papacchini
The 2019 Multi-Agent Programming Contest introduced a new scenario, Agents Assemble, where two teams of agents move around a 2D grid and compete to assemble complex block structure…
Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
Xingyu Zhao, Matt Osborne, Jenny Lantair +6
The battery is a key component of autonomous robots. Its performance limits the robot's safety and reliability. Unlike liquid-fuel, a battery, as a chemical device, exhibits compli…
On the Enactability of Agent Interaction Protocols: Toward a Unified Approach
Angelo Ferrando, Michael Winikoff, Stephen Cranefield +2
Interactions between agents are usually designed from a global viewpoint. However, the implementation of a multi-agent interaction is distributed. This difference can introduce iss…