arXiv subjects

Alessandro Aldini

Publications and source records attributed to Alessandro Aldini.

15 recordsLinked to original sources

arXiv2026

A Logical 3-valued Semantics for Nondeterministic Choice

We propose a logical formalisation of computational errors in reactive, nondeterministic systems. To this aim, we introduce a new three-valued symmetric nondeterministic disjunction, designed to provide a faithful logical representation of the nondeterministic choice arising in concurrent computations. The connective is defined within the framework of nondeterministic matrices (Nmatrices) and derives from a minimal combination of Kleene's tolerant semantics and Bochvar's symmetric error persistence, thereby eliminating the residual asymmetry induced by sequential evaluation strategies such as McCarthy's logic. The resulting semantics admits genuinely nondeterministic outcomes in mixed cases involving errors, while preserving commutativity and operational symmetry.

cs.LO↗

arXiv2025

A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems

We address the problem of identifying a proof-theoretic framework that enables a compositional analysis of finite-trace properties in concurrent systems, with a particular focus on those specified via prefix-closure. To this end, we investigate the interaction of a prefix-closure operator and its residual (with respect to set-theoretic inclusion) with language intersection, union, and concatenation, and introduce the variety of closure $\ell$-monoids as a minimal algebraic abstraction of finite-trace properties to be conveniently described within an analytic proof system. Closure $\ell$-monoids are division-free reducts of distributive residuated lattices equipped with a forward diamond/backward box residuated pair of unary modal operators, where the diamond is a topological closure operator satisfying $\Diamond(x \cdot y) \leq \Diamond x \cdot \Diamond y$. As a logical counterpart to these structures, we present $\mathsf{LMC}$, a Gentzen-style system based on the division-free fragment of the Distributive Full Lambek Calculus. In $\mathsf{LMC}$, structural terms are built from formulas using Belnap-style structural operators for monoid multiplication, meet, and diamond. The rules for the modalities and the structural diamond are taken from Moortgat's system $\mathsf{NL}(\Diamond)$. We show that the calculus is sound and complete with respect to the variety of closure $\ell$-monoids and that it admits cut elimination.

cs.LO↗

arXiv2025

Privacy-preserving and reward-based mechanisms of proof of engagement

Proof-of-Attendance (PoA) mechanisms are typically employed to demonstrate a specific user's participation in an event, whether virtual or in-person. The goal of this study is to extend such mechanisms to broader contexts where the user wishes to digitally demonstrate her involvement in a specific activity (Proof-of-Engagement, PoE). This work explores different solutions, including DLTs as well as established technologies based on centralized systems. The main aspects we consider include the level of privacy guaranteed to users, the scope of PoA/PoE (both temporal and spatial), the transferability of the proof, and the integration with incentive mechanisms.

cs.CR↗

arXiv2025

Noninterference Analysis of Irreversible Systems and Reversible Systems Featuring both Nondeterminism and Probabilities

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.

cs.CR↗

arXiv2024

Towards Evaluating Large Language Models for Graph Query Generation

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.

cs.ET↗

arXiv2024

Support + Belief = Decision Trust

We present SBTrust, a logical framework designed to formalize decision trust. Our logic integrates a doxastic modality with a novel non-monotonic conditional operator that establishes a positive support relation between statements, and is closely related to a known dyadic deontic modality. For SBTrust, we provide semantics, proof theory and complexity results, as well as motivating examples. Compared to existing approaches, our framework seamlessly accommodates the integration of multiple factors in the emergence of trust.

cs.LO↗

arXiv2024

A process algebraic framework for multi-agent dynamic epistemic systems

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.

cs.AI↗

arXiv2024

A logical perspective on intending to keep a true secret

Logical investigations of the notion of secrecy are typically concentrated on tools for deducing whether private information is well hidden from unauthorized, direct, or indirect access attempts. This paper proposes a multi-agent, normal multi-modal logic to capture salient features of secrecy's intentions. Specifically, we focus on the intentions, beliefs, and knowledge of secret keepers and, more generally, of all the actors involved in secret-keeping scenarios. In particular, we investigate intentions underlying the keeping of a true secret, namely a secret concerning information known (and so true) by the secret keeper. The resulting characterization of intending to keep a true secret provides valuable insights into conditions ensuring or undermining secrecy depending on agents' attitudes and links between secrets and their surrounding context. We present the proposed logical system's soundness, completeness, and decidability results. Furthermore, we outline some theorems with potential applications to several fields, e.g., computer science and the social sciences.

math.LO↗

arXiv2023

Noninterference Analysis of Reversible Systems: An Approach Based on Branching Bisimilarity

The theory of noninterference supports the analysis of information leakage and the execution of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics. We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations. As illustrated via a database management system example, the activation of backward computations may trigger information flows that are not observable when proceeding in the standard forward direction. To capture the effects of back-and-forth computations, it is necessary to switch to a more expressive semantics, which has been proven to be branching bisimilarity in a previous work by De Nicola, Montanari, and Vaandrager. In this paper we investigate a taxonomy of noninterference properties based on branching bisimilarity along with their preservation and compositionality features, then we compare it with the taxonomy of Focardi and Gorrieri based on weak bisimilarity.

cs.CR↗

arXiv2020

Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond

Quantitative aspects of computation are related to the use of both physical and mathematical quantities, including time, performance metrics, probability, and measures for reliability and security. They are essential in characterizing the behaviour of many critical systems and in estimating their properties. Hence, they need to be integrated both at the level of system modeling and within the verification methodologies and tools. Along the last two decades a variety of theoretical achievements and automated techniques have contributed to make quantitative modeling and verification mainstream in the research community. In the same period, they represented the central theme of the series of workshops entitled Quantitative Aspects of Programming Languages and Systems (QAPL) and born in 2001. The aim of this survey is to revisit such achievements and results from the standpoint of QAPL and its community.

cs.PL↗

arXiv2020

Proceedings 16th Workshop on Quantitative Aspects of Programming Languages and Systems

This EPTCS volume contains the proceedings of the 16th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2019) held in Prague, Czech Republic, on Sunday 7 April 2019. QAPL 2019 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019). QAPL focuses on quantitative aspects of computations, which may refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (e.g., probabilities) for the characterisation of the behaviour and for determining the properties of systems. Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis or synthesis of systems. The 16th edition of QAPL also focuses on discussing the developments, challenges and results in this area covered by our workshop in its nearly 20-year history.

cs.PL↗

arXiv2018

Process Algebraic Architectural Description Languages: Generalizing Component-Oriented Mismatch Detection in the Presence of Nonsynchronous Communications

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.

cs.SE↗

arXiv2016

A Formal Framework for Modeling Trust and Reputation in Collective Adaptive Systems

Trust and reputation models for distributed, collaborative systems have been studied and applied in several domains, in order to stimulate cooperation while preventing selfish and malicious behaviors. Nonetheless, such models have received less attention in the process of specifying and analyzing formally the functionalities of the systems mentioned above. The objective of this paper is to define a process algebraic framework for the modeling of systems that use (i) trust and reputation to govern the interactions among nodes, and (ii) communication models characterized by a high level of adaptiveness and flexibility. Hence, we propose a formalism for verifying, through model checking techniques, the robustness of these systems with respect to the typical attacks conducted against webs of trust.

cs.LO↗

arXiv2015

Expected-Delay-Summing Weak Bisimilarity for Markov Automata

A new weak bisimulation semantics is defined for Markov automata that, in addition to abstracting from internal actions, sums up the expected values of consecutive exponentially distributed delays possibly intertwined with internal actions. The resulting equivalence is shown to be a congruence with respect to parallel composition for Markov automata. Moreover, it turns out to be comparable with weak bisimilarity for timed labeled transition systems, thus constituting a step towards reconciling the semantics for stochastic time and deterministic time.

cs.LO↗

arXiv2010

Approximate Testing Equivalence Based on Time, Probability, and Observed Behavior

Several application domains require formal but flexible approaches to the comparison problem. Different process models that cannot be related by behavioral equivalences should be compared via a quantitative notion of similarity, which is usually achieved through approximation of some equivalence. While in the literature the classical equivalence subject to approximation is bisimulation, in this paper we propose a novel approach based on testing equivalence. As a step towards flexibility and usability, we study different relaxations taking into account orthogonal aspects of the process observations: execution time, event probability, and observed behavior. In this unifying framework, both interpretation of the measures and decidability of the verification algorithms are discussed.

cs.LO↗