Author name cluster

Michele Boreale

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

21 papers

2 author rows

GandALF Workshop 2025 Workshop Paper

Parallelizable Feynman-Kac Models for Universal Probabilistic Programming

Michele Boreale
Luisa Collodi

We study provably correct and efficient instantiations of Sequential Monte Carlo (SMC) inference in the context of formal operational semantics of Probabilistic Programs (PPs). We focus on universal PPs featuring sampling from arbitrary measures and conditioning/reweighting in unbounded loops. We first equip Probabilistic Program Graphs (PPGs), an automata-theoretic description format of PPs, with an expectation-based semantics over infinite execution traces, which also incorporates trace weights. We then prove a finite approximation theorem that provides bounds to this semantics based on expectations taken over finite, fixed-length traces. This enables us to frame our semantics within a Feynman-Kac (FK) model, and ensures the consistency of the Particle Filtering (PF) algorithm, an instance of SMC, with respect to our semantics. Building on these results, we introduce VPF, a vectorized version of the PF algorithm tailored to PPGs and our semantics. Experiments conducted with a proof-of-concept implementation of VPF show very promising results compared to state-of- the-art PP inference tools.

PDF Details DOI

I&C Journal 2022 Journal Article

Automatic pre- and postconditions for partial differential equations

Michele Boreale

Based on an automata-theoretic and algebraic framework, we study equational reasoning for Initial Value Problems (ivps) of polynomial Partial Differential Equations (pdes). We first characterize the solutions of a pde system Σ in terms of the final morphism from a coalgebra induced by Σ to the coalgebra of formal power series (fps). fps solutions conservatively extend the classical analytic ones. To express ivps in their general form, we then introduce stratified systems, where the specification of a function can be decomposed into distinct subsystems of pdes. We lift the existence and uniqueness result of fps solutions to stratified systems. We then give a relatively complete algorithm to compute weakest preconditions and strongest postconditions for such systems. To some extent, this result reduces equational reasoning on pde initial value problems to algebraic reasoning. We illustrate some experiments conducted with a proof-of-concept implementation of the method.

MFCS Conference 2019 Conference Paper

On the Coalgebra of Partial Differential Equations

Michele Boreale

We note that the coalgebra of formal power series in commutative variables is final in a certain subclass of coalgebras. Moreover, a system Sigma of polynomial PDEs, under a coherence condition, naturally induces such a coalgebra over differential polynomial expressions. As a result, we obtain a clean coinductive proof of existence and uniqueness of solutions of initial value problems for PDEs. Based on this characterization, we give complete algorithms for checking equivalence of differential polynomial expressions, given Sigma.

TCS Journal 2015 Journal Article

Worst- and average-case privacy breaches in randomization mechanisms

Michele Boreale
Michela Paolini

In a variety of contexts, randomization is regarded as an effective technique to conceal sensitive information. Viewing randomization mechanisms as information-theoretic channels, we start from a semantic notion of security, which expresses absence of any privacy breach above a given level of seriousness ϵ, irrespective of any background information, represented as a prior probability on the secret inputs. We first examine this notion according to two dimensions: worst vs. average case, single vs. repeated observations. In each case, we characterize the security level achievable by a mechanism in a simple fashion that only depends on the channel matrix, and specifically on certain measures of “distance” between its rows, like norm-1 distance and Chernoff Information. We next clarify the relation between our worst-case security notion and differential privacy (dp): we show that, while the former is in general stronger, the two coincide if one confines to background information that can be factorized into the product of independent priors over individuals. We finally turn our attention to expected utility, in the sense of Ghosh et al. , in the case of repeated independent observations. We characterize the exponential growth rate of any reasonable utility function. In the particular case the mechanism provides ϵ-dp, we study the relation of the utility rate with ϵ: we offer either exact expressions or upper-bounds for utility rate that apply to practically interesting cases, such as the (truncated) geometric mechanism.

I&C Journal 2012 Journal Article

A coalgebraic perspective on linear weighted automata

Filippo Bonchi
Marcello Bonsangue
Michele Boreale
Jan Rutten
Alexandra Silva

Weighted automata are a generalisation of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e. g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence. Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours. In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on Set (the category of sets and functions) characterise weighted bisimilarity, while coalgebras on Vect (the category of vector spaces and linear maps) characterise weighted language equivalence. Relying on the second characterisation, we show three different procedures for computing weighted language equivalence. The first one consists in a generalisation of the usual partition refinement algorithm for ordinary automata. The second one is the backward version of the first one. The third procedure relies on a syntactic representation of rational weighted languages.

I&C Journal 2012 Journal Article

Deciding safety properties in infinite-state pi-calculus via behavioural types

Lucia Acciai
Michele Boreale

In the pi-calculus, we consider the decidability of model checking properties expressed in Shallow Logic, a simple spatial logic. We first introduce a behavioural type system that, given a pi-process P that might in general be infinite-control, tries to extract a spatial-behavioural type T, in the form of a ccs term that is logically equivalent to P. Employing techniques based on well-structured transition systems (wsts), we prove that model checking ( T ⊨ ϕ ) is decidable for types, for a fragment of the logic that can be used to encode interesting safety and reachability properties. The wsts technique we rely upon requires first endowing the considered transition system with a well-quasi order, then defining a finite basis for the denotation of each formula. This is achieved by viewing types as forests, with a well-quasi order that corresponds to a form of forest embedding. As a consequence of the logical equivalence between types and processes, we obtain the decidability of the considered fragment of the logic for well-typed pi-processes. We discuss (un)decidability and complexity of model checking also outside the considered decidable fragment of Shallow Logic.

I&C Journal 2010 Journal Article

Spatial and behavioral types in the pi-calculus

Lucia Acciai
Michele Boreale

We present a framework that combines ideas from spatial logics and behavioral type systems. Type systems for the pi-calculus are proposed where newly declared (restricted) names are annotated with spatial process properties, predicating on those names, that are expected to hold in the scope of the declaration. Types are akin to ccs terms and account for the process abstract behavior and “shallow” spatial structure. Type checking relies on spatial model checking, but properties are checked against types rather than against processes. Type soundness theorems ensure that, for a certain class of spatial properties, well-typed programs are also well annotated, in the sense that processes in the scope of any restriction do satisfy the corresponding annotation at run-time. The considered class of properties is rather general. Differently from previous proposals, it includes both safety and liveness ones, and is not limited to invariants. We also elaborate a distinction between locally and globally checkable properties.

I&C Journal 2009 Journal Article

Quantifying information leakage in process calculi

Michele Boreale

Building on simple information-theoretic concepts, we study two quantitative models of information leakage in the pi-calculus. The first model presupposes an attacker with an essentially unlimited computational power. The resulting notion of absolute leakage, measured in bits, is in agreement with secrecy as defined by Abadi and Gordon: a process has an absolute leakage of zero precisely when it satisfies secrecy. The second model assumes a restricted observation scenario, inspired by the testing equivalence framework, where the attacker can only conduct repeated success-or-failure experiments on processes. Moreover, each experiment has a cost in terms of communication effort. The resulting notion of leakage rate, measured in bits per action, is in agreement with the first model: the maximum amount of information that can be extracted by repeated experiments coincides with the absolute leakage A of the process. Moreover, the overall extraction cost is at least A / R, where R is the rate of the process. The compositionality properties of the two models are also investigated.

TCS Journal 2008 Journal Article

Responsiveness in process calculi

Lucia Acciai
Michele Boreale

A system guarantees responsive usage of a channel r if a communication along r is guaranteed to eventually take place. Responsiveness is important, for instance, to ensure that any request to a service be eventually replied. We propose two distinct type systems, each of which statically guarantees responsive usage of names in well-typed pi-calculus processes. In the first system, we achieve responsiveness by combining techniques for deadlock and livelock avoidance with linearity and receptiveness. The latter is a guarantee that a name is ready to receive as soon as it is created. These conditions imply relevant limitations on the nesting of actions and on multiple use of names in processes. In the second system, we relax these requirements so as to permit certain forms of nested inputs and multiple outputs. We demonstrate the expressive power of the two systems by showing that primitive recursive functions–in the case of the first system–and Cook and Misra’s service orchestration language orc–in the case of the second system–can be encoded into well-typed processes.

TCS Journal 2006 Journal Article

Processes as formal power series: A coinductive approach to denotational semantics

Michele Boreale
Fabio Gadducci

We characterize must testing equivalence on CSP in terms of the unique homomorphism from the Moore automaton of CSP processes to the final Moore automaton of partial formal power series over a certain semiring. The final automaton is then turned into a CSP-algebra: operators and fixpoints are defined, respectively, via behavioural differential equations and simulation relations. This structure is then shown to be preserved by the final homomorphism. As a result, we obtain a fully abstract compositional model of CSP phrased in purely set-theoretical terms.

TCS Journal 2005 Journal Article

A method for symbolic analysis of security protocols

Michele Boreale
Maria Grazia Buscemi

In security protocols, message exchange between the intruder and honest participants induces a form of state explosion which makes protocol models infinite. We propose a general method for automatic analysis of security protocols based on the notion of frame, essentially a rewrite system plus a set of distinguished terms called messages. Frames are intended to model generic crypto-systems. Based on frames, we introduce a process language akin to Abadi and Fournet's applied pi. For this language, we define a symbolic operational semantics that relies on unification and provides finite and effective protocol models. Next, we give a method to carry out trace analysis directly on the symbolic model. We spell out a regularity condition on the underlying frame, which guarantees completeness of our method for the considered class of properties, including secrecy and various forms of authentication. We show how to instantiate our method to some of the most common crypto-systems, including shared- and public-key encryption, hashing and Diffie–Hellman key exchange.

MFCS Conference 2003 Conference Paper

Denotational Testing Semantics in Coinductive Form

Michele Boreale
Fabio Gadducci

Abstract Building on recent work by Rutten on coinduction and formal power series, we define a denotational semantics for the csp calculus and prove it fully abstract for testing equivalence. The proposed methodology allows for abstract definition of operators in terms of behavioural differential equations and for coinductive reasoning on them, additionally dispensing with continuous order-theoretic structures.

MFCS Conference 2003 Conference Paper

Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation

Michele Boreale
Maria Grazia Buscemi

Abstract Automatic methods developed so far for analysis of security protocols only model a limited set of cryptographic primitives (often, only encryption and concatenation) and abstract from low-level features of cryptographic algorithms. This paper is an attempt towards closing this gap. We propose a symbolic technique and a decision method for analysis of protocols based on modular exponentiation, such as Diffie-Hellman key exchange. We introduce a protocol description language along with its semantics. Then, we propose a notion of symbolic execution and, based on it, a verification method. We prove that the method is sound and complete with respect to the language semantics.

I&C Journal 2002 Journal Article

Trace and Testing Equivalence on Asynchronous Processes

Michele Boreale
Rocco De Nicola
Rosario Pugliese

We study trace and may-testing equivalences in the asynchronous versions of CCS and π-calculus. We start from the operational definition of the may-testing preorder and provide finitary and fully abstract trace-based characterizations for it, along with a complete in-equational proof system. We also touch upon two variants of this theory by first considering a more demanding equivalence notion (must-testing) and then a richer version of asynchronous CCS. The results throw light on the difference between synchronous and asynchronous communication and on the weaker testing power of asynchronous observations.

TCS Journal 2001 Journal Article

Divergence in testing and readiness semantics

Michele Boreale
Rocco De Nicola
Rosario Pugliese

Many variants of must-testing semantics have been put forward that are equally sensitive to deadlock, but differ for the stress they put on divergence, i. e. on the possibility for systems of getting involved in infinite internal computations. Safe-testing is one such variant, that naturally pops up when studying the behavioural pre-congruences induced by certain basic observables. Here, we study the relationship between safe-testing and Olderog's readiness semantics, a semantics induced by a natural process logic. We show that safe-testing is finer than readiness, and coincides with a refinement of readiness obtained by tuning Olderog's definition. For both safe-testing and the original readiness semantics we propose simple complete axiomatizations, which permit a fuller appreciation of their similarities and differences.

TCS Journal 2000 Journal Article

A complexity analysis of bisimilarity for value-passing processes

Michele Boreale
Luca Trevisan

We study the complexity of deciding bisimilarity between non-deterministic processes with explicit primitives for manipulating data values. In particular, we consider a language with value-passing (input/output of data) and parametric definitions of processes. We distinguish the case in which data cannot be tested and the case in which a simple equality test over data is permitted. In the first case, our main result shows that the problem is PSPACE-hard for the full calculus. In the second case, we first show that the problem is coNP-complete in the fragment with value-passing and no parametric definitions. We then define a compositional polynomial-time translation of the full calculus to the fragment with parametric definitions but no value-passing. The translation preserves bisimilarity: this fact establishes the decidability of the full calculus and shows that the fragment without value-passing is computationally equivalent to the full calculus. For the latter, bisimilarity is then proved to be EXP-complete. Finally, we add to our language a parallel composition operator and show that, for a certain restricted syntactic format, the bisimilarity problem is still decidable and EXP-complete.

I&C Journal 1999 Journal Article

Basic Observables for Processes

Michele Boreale
Rosario Pugliese

A general approach for defining behavioral preorders over process terms as the maximal precongruences induced by basic observables is examined. Three different observables that provide information about the initial communication capabilities of processes and about the possibility that processes get engaged in divergent computations will be considered. We show that the precongruences induced by our basic observables coincide with intuitive and/or widely studied behavioral preorders. In particular, we retrieve in our setting themust preorderof De Nicola and Hennessy and thefair/should preorderintroduced by Cleaveland and Natarajan and by Brinksma, Rensink, and Vogler. A new form of testing preorder, which we callsafe-must, also emerges. The alternative characterizations we offer shed light on the differences between these pre- orders and on the role played in their definition by tests for divergence.

TCS Journal 1998 Journal Article

On the expressiveness of internal mobility in name-passing calculi

Michele Boreale

We consider πI, a fragment of the π-calculus where only exchange of private names among processes is permitted (internal mobility). The calculus πI enjoys a simpler mathematical treatment, very close to that of CCS. In particular, πI avoids the concept of substitution. We provide an encoding from the asynchronous π-calculus to πI and then prove that two processes are barbed-equivalent in π-calculus if and only if their translations in πI cannot be distinguished, under barbed bisimilarity, by any translated static context. The result shows that, in namepassing calculi, internal mobility is the essential ingredient as far as expressiveness is concerned.

TCS Journal 1998 Journal Article

Some congruence properties for π-calculus bisimilarities

Michele Boreale
Davide Sangiorgi

Both for interleaving and for non-interleaving semantics, several variants of a π-calculus bisimilarity can be given which differ on the requirements imposed on name instantiations. Examples are the late, early, open and ground variants. The ground variant is the simplest because it places no requirements on name instantiations. With the exception of open bisimilarities, none of the bisimilarity considered in the literature is a congruence relation on the full π-calculus language. We show that in the case of (certain forms of) causal bisimulation the late, early, open and ground variants coincide and are congruence relations in the sublanguage of the π-calculus without matching. We also show that to obtain the same results in the case of the interleaving bisimilarity, in addition to forbidding matching it is necessary to constrain the output prefix.

I&C Journal 1996 Journal Article

A Symbolic Semantics for theπ-Calculus

Michele Boreale
Rocco De Nicola

We use symbolic transition systems as a basis for providing theπ-calculus with an alternative semantics. The latter is more amenable to automatic manipulation and sheds light on the logical differences among different forms of bisimulation over algebras of name-passing processes. Symbolic transitions have the form[formula], whereφis a boolean combination of equalities on names that has to hold for the transition to take place, andαis standard aπ-calculus action. On top of the symbolic transition system, a symbolic bisimulation is defined that captures the standard ones. Finally, a sound and complete proof system is introduced for symbolic bisimulation.

MFCS Conference 1996 Conference Paper

Bisimilarity Problems Requiring Exponential Time

Michele Boreale
Luca Trevisan 0001

Abstract We study the complexity of deciding bisimilarity between non-deterministic processes. In particular, we consider a calculus with recursive definitions of processes, value passing (i. e. input/output of data) and an equality test over data. We show that the bisimilarity problem is EXP-complete over this calculus and thus that exponential time is provably necessary in order to solve it. We then prove that, if we add a parallel composition operator to the calculus, and we impose that parallel composition is never used inside recursive definitions, then the bisimilarity problem is still EXP-complete, thus no harder than in the fragment without parallel composition.