Author name cluster

Roberto Bruni

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.

14 papers

1 author row

TCS Journal 2025 Journal Article

Broadening the applicability of local completeness analysis with intensional and extensional guarantees

Flavio Ascari
Roberto Bruni
Roberta Gori

Local Completeness Logic (LCL) is a proof system for program analysis rooted in abstract interpretation. The program semantics is under-approximated by any provable postcondition, like incorrectness logic does, but it is also over-approximated by a (locally) complete abstraction of such a postcondition, like Hoare logic does. Therefore, any derivable triple will either prove the program to be correct or unveil true bugs. While the completeness of a program's function with respect to an abstract domain is inherently extensional, LCL's rules demand the preservation of local completeness throughout the abstract interpreter's computations. This characteristic renders LCL analysis intensional, meaning it depends on the way the program is written. Consequently, LCL proof system may not derive all the valid triples. This paper addresses this discrepancy by: 1) designing new rules that allow one to perform part of the intensional analysis in different (complete) abstract domains whenever necessary; and 2) to compare their expressiveness. Notably, some of these new rules enable the derivation of all extensionally valid triples, thereby decoupling the set of provable properties from the way the program is written.

Details DOI

TCS Journal 2021 Journal Article

A logical and graphical framework for reaction systems

Linda Brodo
Roberto Bruni
Moreno Falaschi

Reaction Systems (RSs) are a successful computational framework inspired by biological systems. A RS pairs a set of entities with a set of reactions over them. Entities can be used to enable or inhibit each reaction, and are produced by reactions. Entities can also be provided by an external context sequence to simulate in silico biological experiments. In this paper we define an extension of RSs considering nondeterministic and recursive context operators, and give an original labelled transition system (LTS) for extended RSs in the structural operational semantics (SOS) style. Thanks to extended contexts, a single LTS can now account for several biological experiments. The rich information recorded in transition labels is useful to guarantee the compositionality of SOS inference rules as well as to define an assertion language to tailor behavioural and logical equivalences on some specific properties or entities. The SOS rules have been also exploited to design a flexible prototype implementation in logic programming that allows to inspect the LTS and to extract useful information when performing experiments on a RS. Our implementation provides a rapid prototyping tool for (extensions of) RSs, with a user friendly online interface to our interpreter. A parser allows to introduce the logical formulas and the contexts using the usual comfortable concrete syntax. The user can visualise and inspect the LTS for a RS and make some analysis of its underlying computation patterns, can check if the main RS satisfies a given property and if it is equivalent to a second adversarial RS. Finally, the SOS approach is suited to drive additional enhancements of RSs.

Details DOI

TCS Journal 2021 Journal Article

A process algebraic approach to reaction systems

Linda Brodo
Roberto Bruni
Moreno Falaschi

In the area of Natural Computing, Reaction Systems (RSs) are a qualitative abstraction inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RSs interact with a context, and pose challenges for modularity, compositionality, extendibility and behavioural equivalence. In this paper we define a modular encoding of RSs as processes in the chained Core Network Algebra (cCNA), which is a new variant of the link-calculus. The encoding represents the behaviour of each entity separately and preserves faithfully their features, and we prove its correctness and completeness. Our encoding provides a Labelled Transition System (LTS) semantics for RSs. Based on the LTS semantics, we adapt the classical notion of bisimulation to define a novel equivalence, called bio-similarity, for studying properties of RSs. In particular, we define a new assertion language based on regular expressions, which allows us to specify the properties of interest, and use it to extend Hennessy-Milner logic to our setting. We prove that our bio-similarity relation and the logical equivalence, that are defined parametrically on some assertion of interest, coincide. Finally, we claim that our encoding contributes to increase the expressiveness of RSs, by exploiting the interaction among different RSs.

Details DOI

TCS Journal 2020 Journal Article

Bayesian network semantics for Petri nets

Roberto Bruni
Hernán Melgratti
Ugo Montanari

Recent work by the authors equips Petri occurrence nets (PN) with probability distributions which fully replace nondeterminism. To avoid the so-called confusion problem, the construction imposes additional causal dependencies which restrict choices within certain subnets called structural branching cells (s-cells). Bayesian nets (BN) are usually structured as partial orders where nodes define conditional probability distributions. In the paper, we unify the two structures in terms of Symmetric Monoidal Categories (SMC), so that we can apply to PN ordinary analysis techniques developed for BN. Interestingly, it turns out that PN which cannot be SMC-decomposed are exactly s-cells. This result confirms the importance for Petri nets of both SMC and s-cells.

Details DOI

I&C Journal 2020 Journal Article

The link-calculus for open multiparty interactions

Chiara Bodei
Linda Brodo
Roberto Bruni

We present the link-calculus, an extension of π-calculus, that models interactions that are multiparty, i. e. that may involve more than two processes, mutually exchanging data. Communications are seen as chains of suitably combined links (which record the source and the target ends of each hop of interactions), each contributed by one party. Values are exchanged by means of message tuples, still provided by each party. We develop semantic theories and proof techniques for link-calculus and apply them in reasoning about complex distributing computing scenarios, where more than two participants need to synchronise in order to perform a task. In particular, we introduce the notion of linked bisimilarity in analogy with the early bisimilarity of the π-calculus. Differently from the π-calculus case, we can show that it is a congruence with respect to all the link-calculus operators and that is also closed under name substitution.

Details DOI

TCS Journal 2019 Journal Article

A formal approach to open multiparty interactions

Chiara Bodei
Linda Brodo
Roberto Bruni

We present a process algebra aimed at describing interactions that are multiparty, i. e. that may involve more than two processes and that are open, i. e. the number of the processes they involve is not fixed or known a priori. Here we focus on the theory of a core version of a process calculus, without message passing, called Core Network Algebra (CNA). In CNA communication actions are given not in terms of channels but in terms of chains of links that record the source and the target ends of each hop of interactions. The operational semantics of our calculus mildly extends the one of CCS. The abstract semantics is given in the style of bisimulation but requires some ingenuity. Remarkably, the abstract semantics is a congruence for all operators of CNA and also with respect to substitutions, which is not the case for strong bisimilarity in CCS. As a motivating and running example, we illustrate the model of a simple software defined network infrastructure.

Details DOI

TCS Journal 2008 Journal Article

Parametric synchronizations in mobile nominal calculi

Roberto Bruni
Ivan Lanese

We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like π -calculus, and thus exploits directional (input–output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in π -calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of π -calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.

Details DOI

TCS Journal 2006 Journal Article

A basic algebra of stateless connectors

Roberto Bruni
Ivan Lanese
Ugo Montanari

The conceptual separation between computation and coordination in distributed computing systems motivates the use of peculiar entities commonly called connectors, whose task is managing the interaction among distributed components. Different kinds of connectors exist in the literature at different levels of abstraction. We focus on an algebra of connectors that exploits five kinds of basic connectors (plus their duals), namely symmetry, synchronization, mutual exclusion, hiding and inaction. Basic connectors can be composed in series and in parallel. We first define the operational, observational and denotational semantics of connectors, then we show that the observational and denotational semantics coincide and finally we give a complete normal-form axiomatization. The expressiveness of the framework is witnessed by the ability to model all the (stateless) connectors of the architectural design language CommUnity and of the coordination language Reo.

Details DOI

TCS Journal 2006 Journal Article

Semantic foundations for generalized rewrite theories

Roberto Bruni
José Meseguer

Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications.

Details DOI

TCS Journal 2005 Journal Article

Observational congruences for dynamically reconfigurable tile systems

Roberto Bruni
Ugo Montanari
Vladimiro Sassone

The SOS formats that ensure that bisimilarity is a congruence fail in the presence of structural axioms on states. Dynamic bisimulation, introduced to characterize the coarsest congruence for CCS which is also a weak bisimulation, reconciles the ‘bisimilarity is a congruence’ property with structural axioms and also with the specification of open ended systems, where states can be reconfigured at runtime. We show that the compositional framework offered by tile logic handles structural axioms and specifications of reconfigurable systems successfully. This allows for a finitary presentation of dynamic context closure, as internalized in the tile language. The case study of the π -calculus illustrates the main features of our approach. Moreover, duality is exploited to model a second kind of reconfiguration: dynamic specialization.

Details DOI

TCS Journal 2002 Journal Article

Dynamic connectors for concurrency

Roberto Bruni
Ugo Montanari

We propose a metatheoretic approach to the definition of operational and abstract concurrent semantics for systems where name handling is a key issue. The main ingredients of our framework are connectors and tile logic. The former allow for the modeling of various kinds of graph-like and term-like structures, which can be useful in representing system distribution and causal histories. The latter is used to combine the use of connectors in space and in time (i. e. , according to configurations and computations). As a detailed case study, we show how to define a concurrent operational semantics and causal weak bisimilarity for a flavor of basic parallel processes.

Details DOI

TCS Journal 2002 Journal Article

Normal forms for algebras of connections

Roberto Bruni
Fabio Gadducci
Ugo Montanari

Recent years have seen a growing interest towards algebraic structures that are able to express formalisms different from the standard, tree-like presentation of terms. Many of these approaches reveal a specific interest towards the application to the ‘distributed and concurrent systems’ field, but an exhaustive comparison between them is sometimes difficult, because their presentations can be quite dissimilar. This work is a first step towards a unified view: Focusing on the primitive ingredients of distributed spaces (namely interfaces, links and basic modules), we introduce a general schema for describing a normal form presentation of many algebraic formalisms, and show that those normal forms can be thought of as arrows of suitable monoidal categories.

Details DOI

I&C Journal 2001 Journal Article

Functorial Models for Petri Nets

Roberto Bruni
José Meseguer
Ugo Montanari
Vladimiro Sassone

We show that although the algebraic semantics of place/transition Petri nets under the collective token philosophy can be fully explained in terms of strictly symmetric monoidal categories, the analogous construction under the individual token philosophy is not completely satisfactory, because it lacks universality and also functoriality. We introduce the notion of pre-nets to overcome this, obtaining a fully satisfactory categorical treatment, where the operational semantics of nets yields an adjunction. This allows us to present a uniform logical description of net behaviors under both the collective and the individual token philosophies in terms of theories and theory morphisms in partial membership equational logic. Moreover, since the universal property of adjunctions guarantees that colimit constructions on nets are preserved in our algebraic models, the resulting semantic framework has good compositional properties.

Details DOI

I&C Journal 2000 Journal Article

Zero-Safe Nets: Comparing the Collective and Individual Token Approaches

Roberto Bruni
Ugo Montanari

The main feature of zero-safe nets is a primitive notion of transition synchronization. To this aim, besides ordinary places, called stable places, zero-safe nets are equipped with zero places, which in an observable marking cannot contain any token. This yields the notion of transaction: A basic atomic computation, which may use zero tokens as triggers, but defines an evolution between observable markings only. The abstract counterpart of a generic zero-safe net B consists of an ordinary P/T net whose places are the stable places of B and whose transitions represent the transactions of B. The two nets offer the refined and the abstract models of the same system, respectively, where the former can be much smaller than the latter, because of the transition synchronization mechanism. Depending on the chosen approach—collective vs individual token philosophy—two notions of transaction may be defined, each leading to different operational and abstract models. Their comparison is fully discussed on the basis of a multicasting system example. In the second part of the paper, we make use of category theory to analyze and motivate our framework. More precisely, the two operational semantics of zero-safe nets are characterized as adjunctions, and the derivation of abstract P/T nets as coreflections.

Details DOI