Simone Tini

TCS Journal 2024 Journal Article

Robustness for biochemical networks: Step-by-step approach

• Valentina Castiglioni
• Ruggero Lanotte
• Michele Loreti
• Desiree Manicardi
• Simone Tini

We propose two step-by-step approaches to the analysis of robustness in biochemical networks. Our aim is to measure the ability of the network to exhibit step-by-step limited variations on the concentration of a species of interest at varying of the initial concentration of other species. The first approach we propose is reaction-by-reaction, i. e. we compare the states reached by nominal and perturbed networks after they have performed the same number of reactions. We provide a statistical technique allowing for estimating robustness, we implement it in a tool called spebnr (a Simple Python Environment for statistical estimation of Biochemical Network Robustness) and showcase it on three case studies: the EnvZ/OmpR osmoregulatory signaling system of Escherichia Coli, the mechanism of bacterial chemotaxis of Escherichia Coli, and enzyme activity at saturation. Then, we consider a time-by-time approach, in which networks are compared on the basis of the states they reached at the same time point, regardless of how many reactions occurred. This approach is implemented in Stark, and we apply it to the study the robustness of the EnvZ/OmpR osmoregulatory signaling system and the Lotka-Volterra equations.

I&C Journal 2021 Journal Article

A probabilistic calculus of cyber-physical systems

• Ruggero Lanotte
• Massimo Merro
• Simone Tini

Cyber-Physical Systems (CPSs) are integrations of networking and distributed computing systems with physical processes, where feedback loops allow physical processes to affect computations and vice versa. Although CPSs can be found in several real-world domains, their verification often relies on simulation test systems rather than formal methodologies. We propose a hybrid probabilistic process calculus for modelling and reasoning on CPSs. The dynamics of the calculus is expressed in terms of a probabilistic labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based probabilistic behavioural semantics which supports compositional reasonings. For a more careful comparison between CPSs, we provide two compositional probabilistic metrics to formalise the notion of behavioural distance between systems, also in the case of bounded computations. Finally, we provide a non-trivial case study, taken from an engineering application, and use it to illustrate our definitions and our compositional behavioural theory for CPSs.

TCS Journal 2021 Journal Article

A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces

• Ruggero Lanotte
• Simone Tini

Bisimulation metrics are a successful instrument used to estimate the behavioural distance between probabilistic concurrent systems. They have been defined in both discrete and continuous state space models. However, the weak semantics approach, where non-observable actions are abstracted away, has been adopted only in the discrete case. In this paper we fill this gap and provide a weak bisimulation metric for models with continuous state spaces. A technical difficulty is to provide a suitable notion of weak transition, which requires to lift transitions leaving from states to transitions leaving from a continuous distribution over states. We prove that our weak bisimulation metric is non-expansive, thus allowing for compositional reasoning. We prove that systems at distance zero are equated by a suitable notion of probabilistic weak bisimulation. We apply our theory in a case study where continuous distributions derive from the evolution of the physical environment.

TCS Journal 2021 Journal Article

Theoretical Computer Science in Italy

• Alessandra Cherubini
• Nicoletta Sabadini
• Simone Tini

TCS Journal 2020 Journal Article

Probabilistic divide & congruence: Branching bisimilarity

• Valentina Castiglioni
• Simone Tini

Since the seminal paper by Bloom, Fokkink and van Glabbeek, the Divide and Congruence technique allows for the derivation of compositional properties of nondeterministic processes from the SOS-based decomposition of their modal properties. In an earlier paper, we extended their technique to deal also with quantitative aspects of process behavior: we proved the (pre)congruence property for strong (bi)simulations on processes with nondeterminism and probability. In this paper we further extend our decomposition method to favor compositional reasoning with respect to probabilistic weak semantics. In detail, we consider probabilistic branching and rooted probabilistic branching bisimilarity, and we propose logical characterizations for them. These are strongly based on the modal operator 〈 ε 〉 which combines quantitative information and weak semantics by introducing a sort of probabilistic lookahead on process behavior. Our enhanced method will exploit distribution specifications, an SOS-like framework defining the probabilistic behavior of processes, to decompose this particular form of lookahead. We will show how we can apply the proposed decomposition method to derive congruence formats for the considered equivalences from their logical characterizations.

TCS Journal 2020 Journal Article

The metric linear-time branching-time spectrum on nondeterministic probabilistic processes

• Valentina Castiglioni
• Michele Loreti
• Simone Tini

Behavioral equivalences were introduced as a simple and elegant proof methodology for establishing whether the behavior of two processes cannot be distinguished by an external observer. The knowledge of observers usually depends on the observations that they can make on process behavior. Furthermore, the combination of nondeterminism and probability in concurrent systems leads to several interpretations of process behavior. Clearly, different kinds of observations as well as different interpretations lead to different kinds of behavioral relations, such as (bi)simulations, traces and testing. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes with respect to trace and testing semantics. We study the properties of these metrics, like compositionality (expressed in terms of the non-expansiveness property), and we compare their expressive powers. More precisely, we compare them also to (bi)simulation metrics, thus obtaining the first metric linear time – branching time spectrum.

I&C Journal 2019 Journal Article

Logical characterization of branching metrics for nondeterministic probabilistic transition systems

• Valentina Castiglioni
• Simone Tini

In this paper we propose a logical characterization of (bi)simulation metrics obtained by a probabilistic variant of Hennessy-Milner logic enriched with variables, whose semantics is defined following the equational μ-calculus approach. Our characterization is based on the novel notions of mimicking formulae and syntactical distance on formulae. The former ones are the quantitative analogous to characteristic formulae. The latter is a 1-bounded pseudometric on formulae measuring their syntactical disparities. The characterization is obtained by showing that the (bi)simulation distance between processes corresponds to the syntactical distance between their mimicking formulae. We also discuss the expressive power of mimicking formulae with respect to probabilistic (bi)simulations. We show that two processes are bisimilar if and only if their mimicking formulae are syntactically equivalent. Moreover, we obtain that mimicking formulae of processes coincide with their characteristic formulae for ready simulation and that negation free mimicking formulae coincide with the characteristic formulae for simulation.

MFCS Conference 2017 Conference Paper

Compositional Weak Metrics for Group Key Update

• Ruggero Lanotte
• Massimo Merro
• Simone Tini

We investigate the compositionality of both weak bisimilarity metric and weak similarity quasi- metric semantics with respect to a variety of standard operators, in the context of probabilistic process algebra. We show how compositionality with respect to nondeterministic and probabilistic choice requires to resort to rooted semantics. As a main application, we demonstrate how our results can be successfully used to conduct compositional reasonings to estimate the performances of group key update protocols in a multicast setting.

TCS Journal 2014 Journal Article

Compositional semantics and behavioural equivalences for reaction systems with restriction

• Giovanni Pardini
• Roberto Barbuti
• Andrea Maggiolo-Schettini
• Paolo Milazzo
• Simone Tini

Reaction systems are an abstract model of interactions among biochemical reactions, developed around two opposite mechanisms: facilitation and inhibition. The evolution of a reaction system is driven by the external objects which are sent into the system by the environment at each step. In order to increase the modelling expressiveness of the calculus, we consider an extension of reaction systems with restriction, which allows the hiding of entities, such as those occurring inside membranes. To this purpose, we recently developed the Reaction Algebra, a calculus resembling reaction systems extended with a restriction operator. In the present paper, three equivalent semantics for the Reaction Algebra are presented: a reduction semantics, and two state-abstract compositional semantics. The reduction semantics is meant to capture the behaviour of Reaction Algebra models at a high-level, while the two compositional semantics make the interactive nature of reaction systems explicit. The difference between the two compositional semantics lies in how the behaviour with respect to the contextual entities is described: one uses an extensional description, while the other uses an intensional one. We also define, in the settings of both compositional semantics, a behavioural equivalence subsuming the functional equivalence of reaction systems, which is also shown to be congruence, thus providing a formal ground to the modular description of models. Finally, as an example of application of the techniques developed in the paper, we compare the semantics of two different Reaction Algebra models of the functioning of the lac operon in the E. coli bacterium.

TCS Journal 2012 Journal Article

Foundational aspects of multiscale modeling of biological systems with process algebras

• Roberto Barbuti
• Giulio Caravagna
• Andrea Maggiolo-Schettini
• Paolo Milazzo
• Simone Tini

We propose a variant of the CCS process algebra with new features aiming at allowing multiscale modeling of biological systems. In the usual semantics of process algebras for modeling biological systems actions are instantaneous. When different scale levels of biological systems are considered in a single model, one should take into account that actions at a level may take much more time than actions at a lower level. Moreover, it might happen that while a component is involved in one long lasting high level action, it is involved also in several faster lower level actions. Hence, we propose a process algebra with operations and with a semantics aimed at dealing with these aspects of multiscale modeling. We give both a reduction semantics and an SOS semantics for our new algebra with a result of operational correspondence between the two. Moreover, we study behavioral equivalences for such an algebra and give some examples.

TCS Journal 2010 Journal Article

Non-expansive ϵ -bisimulations for probabilistic processes

• Simone Tini

ϵ -bisimulation equivalence has been proposed in the literature as a technique to study the concept of behavioral distance between probabilistic processes. In this paper we first consider the generative model of probabilistic processes and introduce two stronger equivalence notions: action ϵ -bisimulation and global ϵ -bisimulation. For each of these three equivalence notions we propose an SOS transition rule format ensuring the property of non-expansiveness. Non-expansiveness means that if the behavioral distance between s i and t i is ϵ i, then the behavioral distance between f ( s 1, …, s n ) and f ( t 1, …, t n ) is no more that ϵ 1 + ⋯ + ϵ n. As expected, the stronger the ϵ -bisimulation considered, the weaker the constraints of the transition rule format. Then, we switch to the reactive model of probabilistic processes and we propose a rule format for ϵ -bisimulation and action ϵ -bisimulation, arguing that global ϵ -bisimulation is not needed in such a context.

TCS Journal 2008 Journal Article

Compositional semantics and behavioral equivalences for P Systems

• Roberto Barbuti
• Andrea Maggiolo-Schettini
• Paolo Milazzo
• Simone Tini

The aim of the paper is to give a compositional semantics in the style of the Structural Operational Semantics (SOS) and to study behavioral equivalence notions for P Systems. Firstly, we consider P Systems with maximal parallelism and without priorities. We define a process algebra, called P Algebra, whose terms model membranes, we equip the algebra with a Labeled Transition System (LTS) obtained through SOS transition rules, and we study how some equivalence notions defined over the LTS model apply in our case. Then, we consider P Systems with priorities and extend the introduced framework to deal with them. We prove that our compositional semantics reflects correctly maximal parallelism and priorities.

I&C Journal 2007 Journal Article

Taylor approximation for hybrid systems

• Ruggero Lanotte
• Simone Tini

We propose a new approximation technique for Hybrid Automata. Given any Hybrid Automaton H, we call Approx(H, k) the Polynomial Hybrid Automaton obtained by approximating each formula ϕ in H with the formulae ϕ k obtained by replacing the functions in ϕ with their Taylor polynomial of degree k. We prove that Approx(H, k) is an over-approximation of H. We study the conditions ensuring that, given any ϵ >0, some k 0 exists such that, for all k > k 0, the “distance” between any vector satisfying ϕ k and at least one vector satisfying ϕ is less than ϵ. We study also conditions ensuring that, given any ϵ >0, some k 0 exists such that, for all k > k 0, the “distance” between any configuration reached by Approx(H, k) in n steps and at least one configuration reached by H in n steps is less than ϵ.

TCS Journal 2003 Journal Article

A comparison of Statecharts step semantics

• Andrea Maggiolo-Schettini
• Adriano Peron
• Simone Tini

The paper studies some variants of Statecharts step semantics in the framework of structural operational semantics. The chosen framework allows to study precongruence and congruence properties of behavioral preorders and equivalences and to compare, with respect to these properties, the different step semantics considered.

TCS Journal 2003 Journal Article

Concurrency in timed automata

• Ruggero Lanotte
• Andrea Maggiolo-Schettini
• Simone Tini

We introduce Concurrent Timed Automata (CTAs) where automata running in parallel are synchronized. We consider the subclasses of CTAs obtained by admitting, or not, diagonal clock constraints and constant updates, and by letting, or not, sequential automata to update the same clocks. We prove that such subclasses recognize the same languages but differ w. r. t. the succinctness of the models. Moreover, we distinguish between subclasses that are polynomially closed w. r. t. finite union and finite intersection, and subclasses that do not have such properties.

TCS Journal 2001 Journal Article

An axiomatic semantics for Esterel

• Simone Tini

In this paper we propose an axiomatic semantics for the synchronous language Esterel. We begin with giving a structural operational semantics for Esterel in terms of a labeled transition system (LTS). We prove that bisimulation on LTS states (which correspond to Esterel programs) is a congruence and that our LTS reflects the input/output behavior of programs. So, bisimilar programs are distinguished neither by any Esterel context nor by the external environment, and bisimulation is a reasonable notion of behavioral equivalence. In order to characterize equivalent programs, we give a set of axioms and we prove that they induce an axiomatization over Esterel which is sound and complete modulo bisimulation.