1,720,998 research outputs found
A Constraint-based language for multiparty interactions
Full text linkMultiparty interactions are common place in today's distributed systems. An agent usually communicates, in a single session, with other agents to accomplish a given task. Take for instance an online transaction including the vendor, the client, the credit card system and the bank. When specifying this kind of system, we probably observe a single transaction including several (binary) communications leading to changes in the state of all the involved agents. Multiway synchronization process calculi, that move from a binary to a multiparty synchronization discipline, have been proposed to formally study the behavior of those systems. However, adopting models such as Bodei, Brodo, and Bruni's Core Network Algebra (CNA), where the number of participants in an interaction is not fixed a priori, leads to an exponential blow-up in the number of states/behaviors that can be observed from the system. In this paper we explore mechanisms to tackle this problem. We extend CNA with constraints that declaratively allow the modeler to restrict the interaction that should actually happen. Our extended process algebra, called CCNA, finds application in balancing the interactions in a concurrent system, leading to a simple, deadlock-free and fair solution for the Dinning Philosopher problem. Our definition of constraints is general enough and it offers the possibility of accumulating costs in a multiparty negotiation. Hence, only computations respecting the thresholds imposed by the modeler are observed. We use this machinery to neatly model a Service Level Agreement protocol. We develop the theory of CCNA including its operational semantics and a behavioral equivalence that we prove to be a congruence. We also propose a prototypical implementation that allows us to verify, automatically, some of the systems explored in the paper
La modernità degradata delle periferie: un'analisi di "Berlinguer ti voglio bene"
No full textL'articolo esamina il film 'Berlinguer ti voglio bene' alla luce di una prospettiva periferica, e cioè lo fa nella convinzione che certe rappresentazioni di realtà periferiche gettino una luce importante su aspetti che riguardano il centro o i centri del sistema mondo, e in definitiva su 'tutti noi'
Brane Calculi Systems: A Static Preview of their Possible Behaviour
No full textWe improve the precision of a previous Control Flow Analysis for Brane Calculi, by adding information on the context and introducing causality information on the membranes. This allows us to prove some biological properties on the behaviour of systems specified in Brane Calculi
A process algebraic approach to reaction systems
No full textIn 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
A logical and graphical framework for reaction systems
No full textReaction 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
A framework for monitored dynamic slicing of reaction systems
No full textReaction systems (RSs) are a computational framework inspired by biochemical mechanisms. A RS defines a finite set of reactions over a finite set of entities. Typically each reaction has a local scope, because it is concerned with a small set of entities, but complex models can involve a large number of reactions and entities, and their computation can manifest unforeseen emerging behaviours. When a deviation is detected, like the unexpected production of some entities, it is often difficult to establish its causes, e.g., which entities were directly responsible or if some reaction was misconceived. Slicing is a well-known technique for debugging, which can point out the program lines containing the faulty code. In this paper, we define the first dynamic slicer for RSs and show that it can help to detect the causes of erroneous behaviour and highlight the involved reactions for a closer inspection. To fully automate the debugging process, we propose to distil monitors for starting the slicing whenever a violation from a safety specification is detected. We have integrated our slicer in BioResolve, written in Prolog which provides many useful features for the formal analysis of RSs. We define the slicing algorithm for basic RSs and then enhance it for dealing with quantitative extensions of RSs, where timed processes and linear processes can be represented. Our framework is shown at work on suitable biologically inspired RS models
Control Flow Analysis of Generalised Boolean Networks
No full textGeneralised Boolean Networks are a well known qualitative model used to analyse the evolution of genetic networks as well as generic biological pathways. Despite the qualitative abstraction due to the few threshold concentration values considered for each biological element in the model, the complexity of the execution of a Generalised Boolean model could be non trivial. In this paper, we propose a tailored process algebra, called Sim-πn, reminiscent of the π-calculus to model GBNs. We further apply the Control Flow Analysis methodology to the resulting computational model for making static (and therefore less computationally expensive) predictions on the dynamical evolution of the investigated networks. The scope is twofold: helping in the setting up of the model, for checking its completeness, and checking the evolution of the model, in terms of the possibility to reach particular threshold values of the biological elements in the model, when varying the initial conditions
A Computational Model of the Secondary Hemostasis Pathway in Reaction Systems
Full text linkReaction Systems (RSs) are a computational framework inspired by biochemical mechanisms. An RS defines a finite set of reactions over a finite set of entities (molecules, proteins, etc). Starting from an initial set of entities (the initial state), a computation is performed by applying all reactions to a state in order to produce the following state, giving rise to a sequence of sets of entities. RSs have shown to be a general computational framework whose application ranges from the modeling of biological phenomena to molecular chemistry and computer science. In this paper, we contribute to research on the application of RSs for modeling biological systems. We consider the problem of modeling hemostasis, for which several models have been defined, starting from the 1960s. Previous models are based on sets of ordinary differential equations, while we develop a discrete model in RSs for pathways of the secondary hemostasis. Then, we implement our model in BioReSolve, a computational framework for RSs that we have previously defined which provides tools for the specification and verification of properties. By using the tools in BioReSolve we derive important observations on the model behaviour for hemostasis, and in particular, we study the role of three important inhibitors, verifying that their presence or absence leads to phenomena such as thrombophilia, or thromboembolism, or excessive coagulation, etc. We can also study computationally the causality relations between the molecules involved in the reactions showing which entities play a fundamental role, thus contributing to the design of more effective and specialized drugs. Our work can hence help to show how to model complex biological systems in RSs and derive computationally and biologically relevant properties of the systems
ccReact: a rewriting framework for the formal analysis of reaction systems
No full textReaction Systems (RSs) are a computational framework inspired by biochemical systems, where entities produced by reactions can enable or inhibit other reactions. RSs interact with the environment through a sequence of sets of entities called the context. In this work, we introduce ccReact, a novel interaction language for implementing and verifying RSs. ccReact extends the classical RS model by allowing the specification of recursive, nondeterministic, and conditional context sequences, thus enhancing the interactive capabilities of the models. We provide a rewriting logic (RL) semantics for ccReact, making it executable in the Maude system. We prove that our RL embedding is sound and complete, thereby offering a robust tool for analyzing RSs. Our methods enable various formal analysis techniques for RSs, including simulation of RSs interacting with ccReact processes, verification of reachability properties, model checking of temporal (LTL and CTL) formulas, and exploring the system evolution through a graphical tool to better understand its behavior. We apply our methods to analyze RSs from different domains, including computer science and biological systems. Notably, we examine a complex breast cancer case study, demonstrating that our analysis can suggest improvements to the administration of monoclonal antibody therapeutic treatments in certain scenarios
- …
