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 property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this article, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of linear time properties.

Trusting software systems, particularly autonomous ones, is challenging. To address this, formal verification techniques can ensure these systems behave as expected. Runtime Verification (RV) is a leading, lightweight method for verifying system behaviour during execution. However, traditional RV assumes perfect information, meaning the monitoring component perceives everything accurately. This assumption often fails, especially with autonomous systems operating in real-world environments where sensors might be faulty. Additionally, traditional RV considers the monitor to be passive, lacking the capability to interpret the system’s information and thus unable to address incomplete data. In this work, we extend standard RV of Linear Temporal Logic properties to accommodate scenarios where the monitor has imperfect information and behaves rationally. We outline the necessary engineering steps to update the verification pipeline and demonstrate our implementation in a case study involving robotic systems.

The existing approaches to enforcing runtime properties and handling failures in autonomous agents primarily focus on single-agent systems, responding to violations by immediately rejecting unsafe actions. In this paper, we extend the notion of safety shields for Belief-Desire-Intention agents by proposing a revised version where a shield can observe and respond not only to what the agent itself does, but also to changes from other agents, when these affect the shielded agent’s behaviour. Our shields suspend intentions that would break a formal specification and resume them once it is safe to do so. To support this, we introduce recovery shields, a new mechanism that defines when a suspended intention can be safely resumed. Our main contributions are extensions to the reasoning cycle and operational semantics of AgentSpeak(L), as well as an implementation in the JaCaMo platform.

In this paper we describe ChatBDI, a framework for extending Belief-Desire-Intention (BDI) agents implemented in Jason with the ability to understand and generate messages in natural language by exploiting embeddings and Large Language Models (LLMs). Thanks to the generative power of LLMs, the ‘chattification’ of new or legacy multiagent systems (MAS) adds a creative and fluent ‘language actuator’ to BDI agents and serves two main purposes. First, it allows users to enter the MAS and conversate with any other software agent in natural language, as if humans were agents themselves. Second, it allows both the MAS developers and the users to follow the conversation among software agents and to ask them information on their behavior and decisions, acting as a lightweight co-pilot and improving transparency and explainability. The major strength of ChatBDI, and its distinguishing feature w.r.t. related works, is its general purpose nature: by exploiting plan injection and sophisticated meta-programming facilities, ChatBDI can be used to chattify any MAS implemented in Jason or JaCaMo with neither adaptations of the ChatBDI code itself, nor changes to the existing AgentSpeak(L) agents’ source code.

Runtime verification (RV) is a lightweight technique for checking system correctness against formal specifications. Traditional RV assumes full system observability, which rarely holds in distributed and component-based systems where monitors only see partial traces. This leads to inconclusive or incorrect verdicts. To address this, recent work has explored monitors that handle imperfect information and reason about visibility. However, these approaches focus on isolated monitors and overlook coordination in distributed settings. We propose a novel framework for runtime verification with rational multi-monitors, where each monitor is a resource-bounded agent with a local specification. Monitors strategically decide what information to share or request, balancing verification goals with communication costs. We formalise this interaction using multi-agent system techniques and synthesise cooperative strategies through model checking. We implement our approach and evaluate it in a case study, showing that rational coordination improves monitoring conclusiveness over existing approaches.

The verification of Multi-Agent Systems (MAS) poses a significant challenge. Various approaches and methodologies exist to address this challenge; however, tools that support them are not always readily avail able. Even when such tools are accessible, they tend to be hard-coded, lacking in compositionality, and challenging to use due to a steep learning curve. In this paper, we introduce a methodology designed for the formal verification of MAS in a modular and versatile manner, along with an initial prototype, that we named VITAMIN. Unlike existing verification methodologies and frameworks for MAS, VITAMIN is constructed for easy extension to accommodate various logics (for specifying the properties to verify) and models (for deter mining on what to verify such properties).

Digital Product Passports (DPPs) are emerging as foundational tools for transparency, traceability, and sustainability in global supply chains. As regulatory initiatives such as the European Union’s Ecodesign for Sustainable Products Regulation (ESPR) gain momentum, there is increasing demand for technical solutions that support decentralised management and retrieval of product lifecycle data. This paper proposes a lightweight, extensible architecture centred on the DPP Protocol—a general-purpose communication mechanism for interoperable access to product information. The approach is particularly suited to fragmented or highly variable production contexts, such as fashion and other sectors characterised by short product lifecycles, complex supply networks, and limited digital infrastructure. We present two complementary implementations: the DPP Software, a server-side system for managing product data, and the DPP Browser, a stateless client for visualising and querying digital passports. Together, these components demonstrate the feasibility and versatility of the proposed protocol. The solution emphasises interoperability, recursive querying, and role-based access control, offering a foundation for scalable adoption across diverse industrial and regulatory settings.

In 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.

Runtime Verification is a lightweight formal verification technique used to verify whether a system behaves as expected at runtime. Expected behaviour is typically formally specified using properties, which are used to automatically synthesise monitors. Properties that can be verified at runtime by a monitor are called monitorable , while those that cannot are termed non-monitorable . In this paper, we revisit the notion of monitorability and demonstrate how non-monitorable properties can still be used to generate partial monitors. We tackle this from two different perspectives: (i) by recognising that a monitor can give up on monitoring the property under analysis if it recognises that the monitoring will never conclude the satisfaction or violation of the property; (ii) by recognising that a monitor can give up on events that are not necessary for successful monitoring of the property under analysis. By considering these two aspects, we present how to achieve partial monitoring of Linear Temporal Logic properties by building upon the standard monitor construction. Finally, we present a prototype implementation of our approach and its application to a remote inspection case study, as well as a set of evaluation experiments to stress test our approach using synthetic properties. • How to extend standard monitor construction to handle non-monitorable properties. • Non-monitorable properties can be partially monitored. • Tackling partial monitorability directly on the monitor makes the approach formalism-agnostic. • A monitor can give up on a property if it recognises it will never conclude its verification. • A monitor can give up on events if such events are not of interest for the verification of the property.

The digital twin has emerged as an enhancing technology incorporated in several industries including the water industry, also ecological aspects such as water cycles. In this paper we propose a review of the major works done in this field, in addition, we present our proposed future works.

This paper proposes RVElastic, a Runtime Verification prototype framework for monitoring microservice systems. We present its general architecture and report a possible instantiation wherein Apache Kafka is utilised to create the system and its instrumentation, while OpenSearch is employed as a means to analyse and visualise the verification results. We experiment with RVElastic on a simple case study as a proof of concept and report the results in terms of the overhead introduced by the addition of monitors in the microservice system.

Engineering a software system can be a complex process and prone to failure. This is exacerbated when the system under consideration presents some degree of autonomy, such as in cognitive agents. In this paper, we use runtime verification as a way to enforce safety properties on Belief-Desire-Intention (BDI) agents by enveloping certain plans in safety shields. These shields function as a failure handling mechanism, they can detect and avoid violations in shielded plans. The safety shields also provide automated failure recovery by attempting alternative execution paths to avoid violations.

Most mainstream object-oriented languages provide a notion of equality between objects which can be customized to be weaker than reference equality, and which is coupled with the customizable notion of object hash code. This feature is so pervasive in object-oriented code that incorrect redefinition or use of equality and hash code may have a serious impact on software reliability and safety.

International audience

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 this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of the classic two-valued one for Strategy Logic. Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results.

Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.

Abstract Runtime verification is a lightweight formal verification technique used to verify the runtime behaviour of software (resp. hardware) systems. Given a formal property, one or more monitors are synthesized to verify the latter against a system execution. A monitor can only conclude the violation of a property when it observes such a violation. Unfortunately, in safety-critical scenarios, this might happen too late for the system to react properly. In such scenarios, it is advised to use predictive runtime verification, where monitors are capable of anticipating (by using a model of the system) future events before actually observing them. In this work, instead of assuming such a model is given, we describe a runtime verification workflow where the model is learnt and incrementally refined by using process mining techniques. We present the approach and the resulting prototype tool.

Abstract This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension Multi-Model PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a centralised or a compositional way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.

We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based language based on relational updates rules that has been applied to specify topology-sensitive distributed protocols with asynchronous communication. In this setting, the absence of protocol anomalies can be reduced to a coverability problem in which the initial set of configurations is not fixed a priori (Existential Coverability Problem). Existential Coverability in GLog can naturally be expressed into Parameterized Verification judgements in Cubicle. The encoding is based on a translation of relational update rules into transition rules that modify cells of unbounded arrays. To show the effectiveness of the approach, we discuss several verification problems for distributed protocols and distributed objects, a challenging task for traditional verification tools. The experimental results show the flexibility and robustness of Cubicle for the considered class of protocol examples.

When applying formal verification to a system that interacts with the real world, we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The article discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies: an autonomous cruise control system and a simulation of the Mars Curiosity rover.

Parametric trace expressions are a formalism expressly designed for parametric runtime verification (RV) which has been introduced and successfully employed in the context of runtime monitoring of multiagent systems.

In this paper the authors are presenting their work prepared for the Simulation Exploration Experience (SEE) 2014 event. This initiative has been organized by the Simulation Interoperability Standards Organization (SISO) and other leading companies involved in Modeling and Simulation field, and under NASA coordination. SEE, whose previous name was Smackdown, is a project for Federating Interoperable Simulations of Moon Base Operations by using the latest Technologies (i.e. HLA Evolved). The project shown in the following pages is called IPHITOS and simulates a defensive system provided with long range radars and light interceptors to detect, recognize and defeat incoming threats from outer space.