Rocco De Nicola

OVERLAY Workshop 2025 Workshop Paper

Reasoning on Privacy Policies

• Yilian Huang
• Cosimo Perini Brogi
• Rocco De Nicola

FormaliSE Conference 2020 Conference Paper

Verification of Privacy-Enhanced Collaborations

• Sara Belluccini
• Rocco De Nicola
• Marlon Dumas
• Pille Pullonen
• Barbara Re 0001
• Francesco Tiezzi 0001

In a distributed scenario it is possible to find systems consisting of independent parties that collaboratively execute a business process, but cannot disclose a subset of the data used in this process to each other. Such systems can be modelled using the PE-BPMN notation: a privacy-enhanced extension of the BPMN process modeling notation. Given a PE-BPMN model, we address the problem of verifying that the content of certain data objects is not leaked to unauthorized parties. To this end, we formalise the semantics of PE-BPMN collaboration diagrams via a translation into process algebraic specifications. This formalisation enables us to apply model checking to detect unintended data leakages in a PE-BPMN model. We specifically consider data leakages in the context of secret sharing technology. The approach has been implemented on top of the mCRL2 toolset, and integrated into the Pleak toolset supporting privacy analysis of business processes. The proposal has been evaluated using real scenarios.

I&C Journal 2019 Journal Article

A calculus for collective-adaptive systems and its behavioural theory

• Yehia Abd Alrahman
• Rocco De Nicola
• Michele Loreti

We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account “connections” as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labelled Transition Systems that are also used to define bisimilarity between components. Labelled bisimilarity is in full agreement with a barbed congruence, defined by relying on simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding aspects of broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.

TAAS Journal 2014 Journal Article

A Formal Approach to Autonomic Systems Programming

• Rocco De Nicola
• Michele Loreti
• Rosario Pugliese
• Francesco Tiezzi

The autonomic computing paradigm has been proposed to cope with size, complexity, and dynamism of contemporary software-intensive systems. The challenge for language designers is to devise appropriate abstractions and linguistic primitives to deal with the large dimension of systems and with their need to adapt to the changes of the working environment and to the evolving requirements. We propose a set of programming abstractions that permit us to represent behaviors, knowledge, and aggregations according to specific policies and to support programming context-awareness, self-awareness, and adaptation. Based on these abstractions, we define SCEL (Software Component Ensemble Language), a kernel language whose solid semantic foundations lay also the basis for formal reasoning on autonomic systems behavior. To show expressiveness and effectiveness of SCEL;’s design, we present a Java implementation of the proposed abstractions and show how it can be exploited for programming a robotics scenario that is used as a running example for describing the features and potential of our approach.

TCS Journal 2014 Journal Article

Relating strong behavioral equivalences for processes with nondeterminism and probabilities

• Marco Bernardo
• Rocco De Nicola
• Michele Loreti

We present a comparison of behavioral equivalences for nondeterministic and probabilistic processes whose activities are all observable. In particular, we consider trace-based, testing, and bisimulation-based equivalences. For each of them, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via schedulers. The first approach compares two resolutions with respect to the probability distributions of all considered events. The second approach requires that the probabilities of the set of events of a resolution be individually matched by the probabilities of the same events in possibly different resolutions. The third approach only compares the extremal probabilities of each event stemming from the different resolutions. The three approaches have very reasonable motivations and, when applied to fully nondeterministic processes or fully probabilistic processes, give rise to the classical well studied relations. We shall see that, for processes with nondeterminism and probability, they instead give rise to a much wider variety of behavioral relations, whose discriminating power is thoroughly investigated here in the case of deterministic schedulers.

I&C Journal 2013 Journal Article

A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences

• Marco Bernardo
• Rocco De Nicola
• Michele Loreti

Labeled transition systems are typically used as behavioral models of concurrent processes. Their labeled transitions define a one-step state-to-state reachability relation. This model can be generalized by modifying the transition relation to associate a state reachability distribution with any pair consisting of a source state and a transition label. The state reachability distribution is a function mapping each possible target state to a value that expresses the degree of one-step reachability of that state. Values are taken from a preordered set equipped with a minimum that denotes unreachability. By selecting suitable preordered sets, the resulting model, called ULTraS from Uniform Labeled Transition System, can be specialized to capture well-known models of fully nondeterministic processes (LTS), fully probabilistic processes (ADTMC), fully stochastic processes (ACTMC), and nondeterministic and probabilistic (MDP) or nondeterministic and stochastic (CTMDP) processes. This uniform treatment of different behavioral models extends to behavioral equivalences. They can be defined on ULTraS by relying on appropriate measure functions that express the degree of reachability of a set of states when performing multi-step computations. It is shown that the specializations of bisimulation, trace, and testing equivalences for the different classes of ULTraS coincide with the behavioral equivalences defined in the literature over traditional models except when nondeterminism and probability/stochasticity coexist; then new equivalences pop up.

TCS Journal 2008 Journal Article

Semantic subtyping for the pi-calculus

• Giuseppe Castagna
• Rocco De Nicola
• Daniele Varacca

Subtyping relations for the π -calculus are usually defined in a syntactic way, by means of structural rules. We propose a semantic characterisation of channel types and use it to derive a subtyping relation. The type system we consider includes read-only and write-only channel types, as well as boolean combinations of types. A set-theoretic interpretation of types is provided, in which boolean combinations of types are interpreted as the corresponding set-theoretic operations. Subtyping is defined as inclusion of the interpretations. We prove decidability of the subtyping relation and sketch the subtyping algorithm. In order to fully exploit the type system, we define a variant of the π -calculus where communication is subjected to pattern matching that performs dynamic typecase.

I&C Journal 2007 Journal Article

Basic observables for a calculus for global computing

• Rocco De Nicola
• Daniele Gorla
• Rosario Pugliese

We develop the semantic theory of a foundational language for modelling applications over global computers whose interconnection structure can be explicitly manipulated. Together with process distribution, process mobility and remote asynchronous communication through distributed data repositories, the language has primitives for explicitly modelling inter-node connections and for dynamically activating and deactivating them. For the proposed language, we define natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing equivalence. We then focus on barbed congruence and provide an alternative characterisation in terms of a labelled bisimulation. To test practical usability of the semantic theory, we model a system of communicating mobile devices and use the introduced proof techniques to verify one of its key properties.

TCS Journal 2007 Journal Article

Model checking mobile stochastic logic

• Rocco De Nicola
• Joost-Pieter Katoen
• Diego Latella
• Michele Loreti
• Mieke Massink

The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous work by the authors for formulating properties of systems specified in StoKlaim, a Markovian extension of Klaim. The main purpose of MoSL is to address key functional aspects of global computing such as distribution awareness, mobility, and security and their integration with performance and dependability guarantees. In this paper, we present MoSL +, an extension of MoSL, which incorporates some basic features of the Modal Logic for MObility (MoMo), a logic specifically designed for dealing with resource management and mobility aspects of concurrent behaviours. We also show how MoSL + formulae can be model-checked against StoKlaim specifications. For this purpose, we show how existing state-based stochastic model-checkers, like e. g. the Markov Reward Model Checker (MRMC), can be exploited by using a front-end for StoKlaim that performs appropriate pre-processing of MoSL + formulae. The proposed approach is illustrated by modelling and verifying a sample system.

TCS Journal 2006 Journal Article

On the expressive power of KLAIM-based calculi

• Rocco De Nicola
• Daniele Gorla
• Rosario Pugliese

We study the expressive power of variants of KLAIM, an experimental language with programming primitives for network-aware programming that combines the process algebra approach with the coordination-oriented one. KLAIM has proved to be suitable for programming a wide range of distributed applications with agents and code mobility, and has been implemented on the top of a runtime system written in Java. In this paper, the expressivity of its constructs is tested by distilling from it a few, more and more foundational, languages and by studying the encoding of each of them into a simpler one. The expressive power of the considered calculi is finally tested by comparing one of them with asynchronous π -calculus.

TCS Journal 2003 Journal Article

Nondeterministic regular expressions as solutions of equational systems

• Rocco De Nicola
• Anna Labella

We define the class of the linear systems whose solution is expressible as a tuple of nondeterministic regular expressions when they are interpreted as trees of actions rather than as sets of sequences. We precisely characterize those systems that have a regular expression as “canonical” solution, and show that any regular expression can be obtained as a canonical solution of a system of the defined class.

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

Algebraic characterizations of trace and decorated trace equivalences over tree-like structures

• Xiao Jun Chen
• Rocco De Nicola

Behavioural equivalences of labelled transition systems are characterized in terms of homomorphic transformations. This permits relying on algebraic techniques for proving systems properties and reduces equivalence checking of two systems to studying the relationships among the elements of their structures. Different algebraic characterizations of bisimulation-based equivalences in terms of particular transition system homomorphisms have been proposed in the literature. Here, it is shown that trace and decorated trace equivalences can neither be characterized in terms of transition system homomorphisms, nor be defined locally, i. e. , only in terms of action sequences of bounded length and of root-preserving maps. However, results similar to those for bisimulation can be obtained for restricted classes of transition systems. For tree-like systems, we present the algebraic characterizations of trace equivalence and of three well-known decorated trace equivalences, namely ready, ready trace equivalence and failure.

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

Linda-based applicative and imperative process algebras

• Rocco De Nicola
• Rosario Pugliese

The classical algebraic approach to the specification and verification of concurrent systems is tuned to distributed programs that rely on asynchronous communications and permit explicit data exchange. An applicative process algebra, obtained by embedding the Linda primitives for interprocess communication in a CCS/CSP-like language, and an imperative one, obtained from the applicative variant by adding a construct for explicit assignment of values to variables, are introduced. The testing framework is used to define behavioural equivalences for both languages and sound and complete proof systems for them are described together with a fully abstract denotational model (namely, a variant of Strong Acceptance Trees).

TCS Journal 2000 Journal Article

Types for access control

• Rocco De Nicola
• GianLuigi Ferrari
• Rosario Pugliese
• Betti Venneri

KLAIM is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. This paper presents the mathematical foundations of the KLAIM type system; this system permits checking access rights violations of mobile agents. Types are used to describe the intentions (read, write, execute, …) of processes relative to the different localities with which they are willing to interact, or to which they want to migrate. Type checking then determines whether processes comply with the declared intentions, and whether they have been assigned the necessary rights to perform the intended operations at the specified localities. The KLAIM type system encompasses both subtyping and recursively defined types. The former occurs naturally when considering hierarchies of access rights, while the latter is needed to model migration of recursive processes.

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.

TCS Journal 1995 Journal Article

A process algebraic view of input/output automata

• Rocco De Nicola
• Roberto Segala

Input/output automata are a widely used formalism for the specification and verification of concurrent algorithms. Unfortunately, they lack an algebraic characterization, a formalization which has been fundamental for the success of theories like CSP, CCS and ACP. We present a many-sorted algebra for I/O automata that takes into account notions such as interface, input enabling, and local control. It is sufficiently expressive for representing all finitely branching transition systems; hence, all I/O automata with a finitely branching transition relation. Our presentation includes a complete axiomatization of the external trace preorder relation over recursion-free processes with input and output.

MFCS Conference 1994 Conference Paper

A Completeness Theorem fro Nondeterministic Kleene Algebras

• Rocco De Nicola
• Anna Labella

Abstract A generalization of Kleene Algebras (structures with +· *, 0 and 1 operators) is considered to take into account possible nondeterminism expressed by the + operator. It is shown that essentially the same complete axiomatization of Salomaa is obtained except for the elimination of the distribution P·(Q + R) = P·Q + P·R and the idempotence law P + P = P. The main result is that an algebra obtained from a suitable category of labelled trees plays the same role as the algebra of regular events. The algebraic semantics and the axiomatization are then extended by adding Ω and ∥ operator, and the whole set of laws is used as a touchstone for starting a discussion over the laws for deadlock, termination and divergence proposed for models of concurrent systems.

TCS Journal 1993 Journal Article

Universal axioms for bisimulations

• Pierpaolo Degano
• Rocco De Nicola
• Ugo Montanari

Node-labelled graphs, called observation structures, are introduced as a basic model of concurrent distributed systems and as a framework for dealing with observational equivalences over them. In the special case of observation trees, the nodes represent the computations of a system and are labelled by what is observed out of them. The labelling function parametrically maps into different observation domains, e. g. , sequences of actions, partial ordering, mixed ordering, … A language for denoting observation trees is proposed and congruences over its terms are defined as strong, rooted branching and rooted weak bisimulations. Also a new bisimulation, called jumping bisimulation, is defined which naturally arises in the framework of state-labelled structures. Sound and complete axiomatizations, which are independent of the chosen observations, are exhibited for all bisimulations. It is claimed that most of the bisimulation-based congruences known in the literature, for a given process description language, can be recast in terms of congruences on observation structures, by carefully choosing both the bisimulation and the observation domain. Thus, the process of defining the extensional semantics of a process description language can be factorized into a few stages, for each of which several alternatives with clean rationales are available.

TCS Journal 1992 Journal Article

Preface

• Rocco De Nicola
• Ugo Montanari

MFCS Conference 1984 Conference Paper

Models and Operators for Nondeterministic Processes

• Rocco De Nicola