-
An implicit function theorem for the stream calculus
Authors:
Michele Boreale,
Luisa Collodi,
Daniele Gorla
Abstract:
In the context of the stream calculus, we present an Implicit Function Theorem (IFT) for polynomial systems, and discuss its relations with the classical IFT from calculus. In particular, we demonstrate the advantages of the stream IFT from a computational point of view, and provide a few example applications where its use turns out to be valuable.
In the context of the stream calculus, we present an Implicit Function Theorem (IFT) for polynomial systems, and discuss its relations with the classical IFT from calculus. In particular, we demonstrate the advantages of the stream IFT from a computational point of view, and provide a few example applications where its use turns out to be valuable.
△ Less
Submitted 17 June, 2024; v1 submitted 21 March, 2023;
originally announced March 2023.
-
Algebra and coalgebra of stream products
Authors:
Michele Boreale,
Daniele Gorla
Abstract:
We study connections among polynomials, differential equations and streams over a field K, in terms of algebra and coalgebra. We first introduce the class of (F,G)-products on streams, those where the stream derivative of a product can be expressed as a polynomial of the streams themselves and their derivatives. Our first result is that, for every (F,G)-product, there is a canonical way to constru…
▽ More
We study connections among polynomials, differential equations and streams over a field K, in terms of algebra and coalgebra. We first introduce the class of (F,G)-products on streams, those where the stream derivative of a product can be expressed as a polynomial of the streams themselves and their derivatives. Our first result is that, for every (F,G)-product, there is a canonical way to construct a transition function on polynomials such that the induced unique final coalgebra morphism from polynomials into streams is the (unique) K-algebra homomorphism -- and vice versa. This implies one can reason algebraically on streams, via their polynomial representation. We apply this result to obtain an algebraic-geometric decision algorithm for polynomial stream equivalence, for an underlying generic (F,G)-product. As an example of reasoning on streams, we focus on specific products (convolution, shuffle, Hadamard) and show how to obtain closed forms of algebraic generating functions of combinatorial sequences, as well as solutions of nonlinear ordinary differential equations.
△ Less
Submitted 9 July, 2021;
originally announced July 2021.
-
Approximate Model Counting, Sparse XOR Constraints and Minimum Distance
Authors:
Michele Boreale,
Daniele Gorla
Abstract:
The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, many approximate counters have been developed in the last decade, offering formal guarantees of confidence and accuracy. A popular approach is ba…
▽ More
The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem. For this reason, many approximate counters have been developed in the last decade, offering formal guarantees of confidence and accuracy. A popular approach is based on the idea of using random XOR constraints to, roughly, successively halving the solution set until no model is left: this is checked by invocations to a SAT solver. The effectiveness of this procedure hinges on the ability of the SAT solver to deal with XOR constraints, which in turn crucially depends on the length of such constraints. We study to what extent one can employ sparse, hence short, constraints, keeping guarantees of correctness. We show that the resulting bounds are closely related to the geometry of the set of models, in particular to the minimum Hamming distance between models. We evaluate our theoretical results on a few concrete formulae. Based on our findings, we finally discuss possible directions for improvements of the current state of the art in approximate model counting.
△ Less
Submitted 11 July, 2019;
originally announced July 2019.
-
Algebra, coalgebra, and minimization in polynomial differential equations
Authors:
Michele Boreale
Abstract:
We consider reasoning and minimization in systems of polynomial ordinary differential equations (ode's). The ring of multivariate polynomials is employed as a syntax for denoting system behaviours. We endow this set with a transition system structure based on the concept of Lie-derivative, thus inducing a notion of L-bisimulation. We prove that two states (variables) are L-bisimilar if and only if…
▽ More
We consider reasoning and minimization in systems of polynomial ordinary differential equations (ode's). The ring of multivariate polynomials is employed as a syntax for denoting system behaviours. We endow this set with a transition system structure based on the concept of Lie-derivative, thus inducing a notion of L-bisimulation. We prove that two states (variables) are L-bisimilar if and only if they correspond to the same solution in the ode's system. We then characterize L-bisimilarity algebraically, in terms of certain ideals in the polynomial ring that are invariant under Lie-derivation. This characterization allows us to develop a complete algorithm, based on building an ascending chain of ideals, for computing the largest L-bisimulation containing all valid identities that are instances of a user-specified template. A specific largest L-bisimulation can be used to build a reduced system of ode's, equivalent to the original one, but minimal among all those obtainable by linear aggregation of the original equations. A computationally less demanding approximate reduction and linearization technique is also proposed.
△ Less
Submitted 14 February, 2019; v1 submitted 23 October, 2017;
originally announced October 2017.
-
Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODEs
Authors:
Michele Boreale
Abstract:
A system of polynomial ordinary differential equations (ODEs) is specified via a vector of multivariate polynomials, or vector field, $F$. A safety assertion $ψ\rightarrow[F]φ$ means that the trajectory of the system will lie in a subset $φ$ (the postcondition) of the state-space, whenever the initial state belongs to a subset $ψ$ (the precondition). We consider the case when $φ$ and $ψ$ are algeb…
▽ More
A system of polynomial ordinary differential equations (ODEs) is specified via a vector of multivariate polynomials, or vector field, $F$. A safety assertion $ψ\rightarrow[F]φ$ means that the trajectory of the system will lie in a subset $φ$ (the postcondition) of the state-space, whenever the initial state belongs to a subset $ψ$ (the precondition). We consider the case when $φ$ and $ψ$ are algebraic varieties, that is, zero sets of polynomials. In particular, polynomials specifying the postcondition can be seen as a system's conservation laws implied by $ψ$. Checking the validity of algebraic safety assertions is a fundamental problem in, for instance, hybrid systems. We consider a generalized version of this problem, and offer an algorithm that, given a user specified polynomial set $P$ and an algebraic precondition $ψ$, finds the largest subset of polynomials in $P$ implied by $ψ$ (relativized strongest postcondition). Under certain assumptions on $φ$, this algorithm can also be used to find the largest algebraic invariant included in $φ$ and the weakest algebraic precondition for $φ$. Applications to continuous semialgebraic systems are also considered. The effectiveness of the proposed algorithm is demonstrated on several case studies from the literature.
△ Less
Submitted 29 March, 2020; v1 submitted 17 August, 2017;
originally announced August 2017.
-
Quantitative information flow under generic leakage functions and adaptive adversaries
Authors:
M. Boreale,
Francesca Pampaloni
Abstract:
We put forward a model of action-based randomization mechanisms to analyse quantitative information flow (QIF) under generic leakage functions, and under possibly adaptive adversaries. This model subsumes many of the QIF models proposed so far. Our main contributions include the following: (1) we identify mild general conditions on the leakage function under which it is possible to derive general…
▽ More
We put forward a model of action-based randomization mechanisms to analyse quantitative information flow (QIF) under generic leakage functions, and under possibly adaptive adversaries. This model subsumes many of the QIF models proposed so far. Our main contributions include the following: (1) we identify mild general conditions on the leakage function under which it is possible to derive general and significant results on adaptive QIF; (2) we contrast the efficiency of adaptive and non-adaptive strategies, showing that the latter are as efficient as the former in terms of length up to an expansion factor bounded by the number of available actions; (3) we show that the maximum information leakage over strategies, given a finite time horizon, can be expressed in terms of a Bellman equation. This can be used to compute an optimal finite strategy recursively, by resorting to standard methods like backward induction.
△ Less
Submitted 9 November, 2015; v1 submitted 21 July, 2015;
originally announced July 2015.
-
Proceedings 7th International Workshop on Security Issues in Concurrency
Authors:
Michele Boreale,
Steve Kremer
Abstract:
This volume contains the proceedings of the 7th Workshop on Security Issues in Concurrency (SecCo'09). The workshop was held in Bologna, Italy on September 5th 2009, as a satellite workshop of CONCUR'09. The aim of the SecCo workshop series is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on com…
▽ More
This volume contains the proceedings of the 7th Workshop on Security Issues in Concurrency (SecCo'09). The workshop was held in Bologna, Italy on September 5th 2009, as a satellite workshop of CONCUR'09. The aim of the SecCo workshop series is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on common interests and stimulating discussions on central research questions. In particular, we called for papers dealing with security issues (such as authentication, integrity, privacy, confidentiality, access control, denial of service, service availability, safety aspects, fault tolerance, trust, language-based security, probabilistic and information theoretic models) in emerging fields like web services, mobile ad-hoc networks, agent-based infrastructures, peer-to-peer systems, context-aware computing, global/ubiquitous/pervasive computing.
△ Less
Submitted 22 October, 2009;
originally announced October 2009.
-
A Concurrent Calculus with Atomic Transactions
Authors:
Lucia Acciai,
Michele Boreale,
Silvano Dal Zilio
Abstract:
The Software Transactional Memory (STM) model is an original approach for controlling concurrent accesses to ressources without the need for explicit lock-based synchronization mechanisms. A key feature of STM is to provide a way to group sequences of read and write actions inside atomic blocks, similar to database transactions, whose whole effect should occur atomically. In this paper, we inves…
▽ More
The Software Transactional Memory (STM) model is an original approach for controlling concurrent accesses to ressources without the need for explicit lock-based synchronization mechanisms. A key feature of STM is to provide a way to group sequences of read and write actions inside atomic blocks, similar to database transactions, whose whole effect should occur atomically. In this paper, we investigate STM from a process algebra perspective and define an extension of asynchronous CCS with atomic blocks of actions. Our goal is not only to set a formal ground for reasoning on STM implementations but also to understand how this model fits with other concurrency control mechanisms. We also view this calculus as a test bed for extending process calculi with atomic transactions. This is an interesting direction for investigation since, for the most part, actual works that mix transactions with process calculi consider compensating transactions, a model that lacks all the well-known ACID properties. We show that the addition of atomic transactions results in a very expressive calculus, enough to easily encode other concurrent primitives such as guarded choice and multiset-synchronization (à la join-calculus). The correctness of our encodings is proved using a suitable notion of bisimulation equivalence. The equivalence is then applied to prove interesting ``laws of transactions'' and to obtain a simple normal form for transactions.
△ Less
Submitted 24 October, 2006;
originally announced October 2006.
