Alessandro Aldini

Andrea Esposito, Alessandro Aldini, Marco Bernardo

The theory of noninterference supports the analysis of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on bisimilarity. In a nondeterministic setting, assessing noninterference through weak bisimilarity is adequate for irreversible systems, whereas for reversible ones branching bisimilarity has been recently proven to be more appropriate. In this paper we address the same two families of systems with the difference that probabilities come into play in addition to nondeterminism according to the alternating model of Hansson and Jonsson. For irreversible systems we extend the results of Aldini, Bravetti, and Gorrieri developed in a generative-reactive probabilistic setting, while for reversible systems we extend the results of Esposito, Aldini, Bernardo, and Rossi developed in a purely nondeterministic setting. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities for irreversible and reversible systems, respectively. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with earlier taxonomies. The adequacy of the extended noninterference theory is illustrated via a probabilistic smart contract lottery.

Siraj Munir, Alessandro Aldini

Large Language Models (LLMs) are revolutionizing the landscape of Generative Artificial Intelligence (GenAI), with innovative LLM-backed solutions emerging rapidly. However, when applied to database technologies, specifically query generation for graph databases and Knowledge Graphs (KGs), LLMs still face significant challenges. While research on LLM-driven query generation for Structured Query Language (SQL) exists, similar systems for graph databases remain underdeveloped. This paper presents a comparative study addressing the challenge of generating Cypher queries a powerful language for interacting with graph databases using open-access LLMs. We rigorously evaluate several LLM agents (OpenAI ChatGPT 4o, Claude Sonnet 3.5, Google Gemini Pro 1.5, and a locally deployed Llama 3.1 8B) using a designed few-shot learning prompt and Retrieval Augmented Generation (RAG) backed by Chain-of-Thoughts (CoT) reasoning. Our empirical analysis of query generation accuracy reveals that Claude Sonnet 3.5 outperforms its counterparts in this specific domain. Further, we highlight promising future research directions to address the identified limitations and advance LLM-driven query generation for graph databases.

Alessandro Aldini

This paper combines the classical model of labeled transition systems with the epistemic model for reasoning about knowledge. The result is a unifying framework for modeling and analyzing multi-agent, knowledge-based, dynamic systems. On the modeling side, we propose a process algebraic, agent-oriented specification language that makes such a framework easy to use for practical purposes. On the verification side, we define a modal logic encompassing temporal and epistemic operators.

Marco Bernardo, Edoardo Bontà, Alessandro Aldini

In the original paper, we showed how to enhance the expressiveness of a typical process algebraic architectural description language by including the capability of representing nonsynchronous communications. In particular, we extended the language by means of additional qualifiers enabling the designer to distinguish among synchronous, semi-synchronous, and asynchronous ports. Moreover, we showed how to modify techniques for detecting coordination mismatches such as the compatibility check for star topologies and the interoperability check for cycle topologies, in such a way that those two checks are applicable also in the presence of nonsynchronous communications. In this addendum, we generalize those results by showing that it is possible to verify in a component-oriented way an arbitrary property of a certain class (not only deadlock) over an entire architectural type having an arbitrary topology (not only stars and cycles) by considering also behavioral variations, exogenous variations, endogenous variations, and multiplicity variations, so to deal with the possible presence of nonsynchronous communications. The proofs are at the basis of some results mentioned in the book "A Process Algebraic Approach to Software Architecture Design" by Alessandro Aldini, Marco Bernardo, and Flavio Corradini, published by Springer in 2010.