Papers | Parallel Computing
2023
Doriana Medić, Marco Aldinucci
Towards formal model for location aware workflows Proceedings Article
In: Shahriar, Hossain, Teranishi, Yuuichi, Cuzzocrea, Alfredo, Sharmin, Moushumi, Towey, Dave, Majumder, A. K. M. Jahangir Alam, Kashiwazaki, Hiroki, Yang, Ji-Jiang, Takemoto, Michiharu, Sakib, Nazmus, Banno, Ryohei, Ahamed, Sheikh Iqbal (Ed.): 47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023, pp. 1864–1869, IEEE, Torino, Italy, 2023.
Abstract | Links | BibTeX | Tags: eupex, icsc, semantics
@inproceedings{23:medic:formal-model,
title = {Towards formal model for location aware workflows},
author = {Doriana Medić and Marco Aldinucci},
editor = {Hossain Shahriar and Yuuichi Teranishi and Alfredo Cuzzocrea and Moushumi Sharmin and Dave Towey and A. K. M. Jahangir Alam Majumder and Hiroki Kashiwazaki and Ji-Jiang Yang and Michiharu Takemoto and Nazmus Sakib and Ryohei Banno and Sheikh Iqbal Ahamed},
url = {https://iris.unito.it/retrieve/1f9f959c-cd88-4d9c-90ea-54f1c86a15bc/6210-medic.pdf},
doi = {10.1109/COMPSAC57700.2023.00289},
year = {2023},
date = {2023-01-01},
booktitle = {47th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2023},
pages = {1864–1869},
publisher = {IEEE},
address = {Torino, Italy},
abstract = {Designing complex applications and executing them on large-scale topologies of heterogeneous architectures is becoming increasingly crucial in many scientific domains. As a result, diverse workflow modelling paradigms are developed, most of them with no formalisation provided. In these circumstances, comparing two different models or switching from one system to the other becomes a hard nut to crack. This paper investigates the capability of process algebra to model a location aware workflow system. Distributed π-calculus is considered as the base of the formal model due to its ability to describe the communicating components that change their structure as an outcome of the communication. Later, it is discussed how the base model could be extended or modified to capture different features of location aware workflow system. The intention of this paper is to highlight the fact that due to its flexibility, π-calculus, could be a good candidate to represent the behavioural perspective of the workflow system.},
keywords = {eupex, icsc, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Designing complex applications and executing them on large-scale topologies of heterogeneous architectures is becoming increasingly crucial in many scientific domains. As a result, diverse workflow modelling paradigms are developed, most of them with no formalisation provided. In these circumstances, comparing two different models or switching from one system to the other becomes a hard nut to crack. This paper investigates the capability of process algebra to model a location aware workflow system. Distributed π-calculus is considered as the base of the formal model due to its ability to describe the communicating components that change their structure as an outcome of the communication. Later, it is discussed how the base model could be extended or modified to capture different features of location aware workflow system. The intention of this paper is to highlight the fact that due to its flexibility, π-calculus, could be a good candidate to represent the behavioural perspective of the workflow system.
2021
Ivan Lanese, Doriana Medić, Claudio Antares Mezzina
Static versus dynamic reversibility in CCS Journal Article
In: Acta Informatica, vol. 58, pp. 1–34, 2021.
Abstract | Links | BibTeX | Tags: semantics
@article{21:journals:LaneseMM21,
title = {Static versus dynamic reversibility in CCS},
author = {Ivan Lanese and Doriana Medić and Claudio Antares Mezzina},
url = {https://doi.org/10.1007/s00236-019-00346-6},
doi = {10.1007/s00236-019-00346-6},
year = {2021},
date = {2021-01-01},
journal = {Acta Informatica},
volume = {58},
pages = {1–34},
abstract = {The notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Most computational models are not naturally reversible since computation causes loss of information, and history information must be stored to enable reversibility. In the literature, two approaches to reverse the CCS process calculus exist, differing on how history information is kept. Reversible CCS (RCCS), proposed by Danos and Krivine, exploits dedicated stacks of memories attached to each thread. CCS with Keys (CCSK), proposed by Phillips and Ulidowski, makes CCS operators static so that computation does not cause information loss. In this paper we show that RCCS and CCSK are equivalent in terms of LTS isomorphism.},
keywords = {semantics},
pubstate = {published},
tppubtype = {article}
}
The notion of reversible computing is attracting interest because of its applications in diverse fields, in particular the study of programming abstractions for fault tolerant systems. Most computational models are not naturally reversible since computation causes loss of information, and history information must be stored to enable reversibility. In the literature, two approaches to reverse the CCS process calculus exist, differing on how history information is kept. Reversible CCS (RCCS), proposed by Danos and Krivine, exploits dedicated stacks of memories attached to each thread. CCS with Keys (CCSK), proposed by Phillips and Ulidowski, makes CCS operators static so that computation does not cause information loss. In this paper we show that RCCS and CCSK are equivalent in terms of LTS isomorphism.
Clément Aubert, Doriana Medić
Explicit Identifiers and Contexts in Reversible Concurrent Calculus Proceedings Article
In: Reversible Computation - 13th International Conference, RC 2021, Virtual Event, July 7-8, 2021, Proceedings, Springer, 2021.
Abstract | Links | BibTeX | Tags: semantics
@inproceedings{21:RC:AubertM21,
title = {Explicit Identifiers and Contexts in Reversible Concurrent Calculus},
author = {Clément Aubert and Doriana Medić},
url = {https://doi.org/10.1007/978-3-030-79837-6_9},
doi = {10.1007/978-3-030-79837-6_9},
year = {2021},
date = {2021-01-01},
booktitle = {Reversible Computation - 13th International Conference, RC 2021, Virtual Event, July 7-8, 2021, Proceedings},
publisher = {Springer},
abstract = {Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions usual in ?forward-only? process algebras, such as replication or context. Existing formalisms disallow the ?hot-plugging? of processes during their execution in contexts with their own past. They also assume the existence of ?eternally fresh? keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of ?reversible? contexts.},
keywords = {semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions usual in ?forward-only? process algebras, such as replication or context. Existing formalisms disallow the ?hot-plugging? of processes during their execution in contexts with their own past. They also assume the existence of ?eternally fresh? keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of ?reversible? contexts.
2020
Doriana Medić, Claudio Antares Mezzina, Iain Phillips, Nobuko Yoshida
A parametric framework for reversible emph(pi)-calculi Journal Article
In: Information and Computation, vol. 275, pp. 104644, 2020.
Abstract | Links | BibTeX | Tags: semantics
@article{20:journals:MedicMPY20,
title = {A parametric framework for reversible emph(pi)-calculi},
author = {Doriana Medić and Claudio Antares Mezzina and Iain Phillips and Nobuko Yoshida},
url = {https://doi.org/10.1016/j.ic.2020.104644},
doi = {10.1016/j.ic.2020.104644},
year = {2020},
date = {2020-01-01},
journal = {Information and Computation},
volume = {275},
pages = {104644},
abstract = {This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in Pi-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible ?-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible emph(pi)-calculus causal semantics.},
keywords = {semantics},
pubstate = {published},
tppubtype = {article}
}
This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in Pi-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible ?-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible emph(pi)-calculus causal semantics.
Ivan Lanese, Doriana Medić
A General Approach to Derive Uncontrolled Reversible Semantics Proceedings Article
In: 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), pp. 33:1–33:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
Abstract | Links | BibTeX | Tags: semantics
@inproceedings{20:concur:LaneseM20,
title = {A General Approach to Derive Uncontrolled Reversible Semantics},
author = {Ivan Lanese and Doriana Medić},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.33},
doi = {10.4230/LIPIcs.CONCUR.2020.33},
year = {2020},
date = {2020-01-01},
booktitle = {31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)},
volume = {171},
pages = {33:1–33:24},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
series = {LIPIcs},
abstract = {Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone. This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order ?-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.},
keywords = {semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone. This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order ?-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.
Doriana Medić, Claudio Antares Mezzina, Iain Phillips, Nobuko Yoshida
Towards a Formal Account for Software Transactional Memory Proceedings Article
In: Reversible Computation - 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings, pp. 255–263, Springer, 2020.
Abstract | Links | BibTeX | Tags: semantics
@inproceedings{20:RC:MedicM0Y20,
title = {Towards a Formal Account for Software Transactional Memory},
author = {Doriana Medić and Claudio Antares Mezzina and Iain Phillips and Nobuko Yoshida},
url = {https://doi.org/10.1007/978-3-030-52482-1_16},
doi = {10.1007/978-3-030-52482-1_16},
year = {2020},
date = {2020-01-01},
booktitle = {Reversible Computation - 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings},
volume = {12227},
pages = {255–263},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {Software transactional memory (STM) is a concurrency control mechanism for shared memory systems. It is opposite to the lock based mechanism, as it allows multiple processes to access the same set of variables in a concurrent way. Then according to the used policy, the effect of accessing to shared variables can be committed (hence, made permanent) or undone. In this paper, we define a formal framework for describing STMs and show how with a minor variation of the rules it is possible to model two common policies for STM: reader preference and writer preference.},
keywords = {semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Software transactional memory (STM) is a concurrency control mechanism for shared memory systems. It is opposite to the lock based mechanism, as it allows multiple processes to access the same set of variables in a concurrent way. Then according to the used policy, the effect of accessing to shared variables can be committed (hence, made permanent) or undone. In this paper, we define a formal framework for describing STMs and show how with a minor variation of the rules it is possible to model two common policies for STM: reader preference and writer preference.
2019
Doriana Medić
Relative expressiveness of calculi for reversible concurrency Journal Article
In: Bull. EATCS, vol. 129, 2019.
Abstract | Links | BibTeX | Tags: semantics
@article{19:eatcs:Medic19,
title = {Relative expressiveness of calculi for reversible concurrency},
author = {Doriana Medić},
url = {http://bulletin.eatcs.org/index.php/beatcs/article/view/590/601},
year = {2019},
date = {2019-01-01},
journal = {Bull. EATCS},
volume = {129},
abstract = {A number of formalisms have been proposed to model various approaches to reversibility and to better understand its properties and characteristics. However, the relation between these formalisms has hardly been studied. This paper examines the expressiveness of the causal-consistent reversibility in process algebras CCS and emph(pi)-calculus. In particular, we show, by means of encodings, that LTSs of two reversible extensions of CCS, Reversible CCS [1] and CCS with Keys [2], are isomorphic up to some structural transformations of processes. To study different causal semantics for ?-calculus, we devise a uniform framework for reversible emph(pi)-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Depending on the used data structure, different causal semantics can be obtained. We show that reversibility induced by our framework when instantiated with three different data structures is causally-consistent and prove a causal correspondence between certain causal semantics and matching instance of the framework.},
keywords = {semantics},
pubstate = {published},
tppubtype = {article}
}
A number of formalisms have been proposed to model various approaches to reversibility and to better understand its properties and characteristics. However, the relation between these formalisms has hardly been studied. This paper examines the expressiveness of the causal-consistent reversibility in process algebras CCS and emph(pi)-calculus. In particular, we show, by means of encodings, that LTSs of two reversible extensions of CCS, Reversible CCS [1] and CCS with Keys [2], are isomorphic up to some structural transformations of processes. To study different causal semantics for ?-calculus, we devise a uniform framework for reversible emph(pi)-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Depending on the used data structure, different causal semantics can be obtained. We show that reversibility induced by our framework when instantiated with three different data structures is causally-consistent and prove a causal correspondence between certain causal semantics and matching instance of the framework.
2017
Paula Severi, Luca Padovani, Emilio Tuosto, Mariangiola Dezani-Ciancaglini
On Sessions and Infinite Data Journal Article
In: Logical Methods in Computer Science, vol. Volume 13, Issue 2, 2017.
Links | BibTeX | Tags: rephrase, semantics
@article{lmcs:3725,
title = {On Sessions and Infinite Data},
author = {Paula Severi and Luca Padovani and Emilio Tuosto and Mariangiola Dezani-Ciancaglini},
url = {http://lmcs.episciences.org/3725},
doi = {10.23638/LMCS-13(2:9)2017},
year = {2017},
date = {2017-06-01},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {article}
}
Mario Coppo, Mariangiola Dezani-Ciancaglini, Alejandro D'ıaz-Caro, Ines Margaria, Maddalena Zacchi
Retractions in Intersection Types Proceedings Article
In: Kobayashi, Naoki (Ed.): ITRS'16, pp. 31–47, 2017.
Links | BibTeX | Tags: rephrase, semantics
@inproceedings{CDMZ16,
title = {Retractions in Intersection Types},
author = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Alejandro D'ıaz-Caro and Ines Margaria and Maddalena Zacchi},
editor = {Naoki Kobayashi},
url = {http://www.di.unito.it/~dezani/papers/cddmz.pdf},
doi = {10.4204/EPTCS.242.5},
year = {2017},
date = {2017-01-01},
booktitle = {ITRS'16},
volume = {242},
pages = {31–47},
series = {EPTCS},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
2016
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Ugo Liguoro
Secure Multiparty Sessions with Topics Proceedings Article
In: PLACES'16, pp. 1–12, 2016.
Links | BibTeX | Tags: rephrase, semantics
@inproceedings{CDL16,
title = {Secure Multiparty Sessions with Topics},
author = {Ilaria Castellani and Mariangiola Dezani-Ciancaglini and Ugo Liguoro},
url = {http://www.di.unito.it/~dezani/papers/cdl16.pdf},
year = {2016},
date = {2016-01-01},
booktitle = {PLACES'16},
volume = {211},
pages = {1–12},
series = {EPTCS},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Jorge A. Pérez
Self-Adaptation and Secure Information Flow in Multiparty Communications Journal Article
In: Formal Aspects of Computing, vol. 28, no. 4, pp. 669–696, 2016.
Links | BibTeX | Tags: rephrase, semantics
@article{CDP16,
title = {Self-Adaptation and Secure Information Flow in Multiparty Communications},
author = {Ilaria Castellani and Mariangiola Dezani-Ciancaglini and Jorge A. Pérez},
url = {http://www.di.unito.it/~dezani/papers/cdp16.pdf},
year = {2016},
date = {2016-01-01},
journal = {Formal Aspects of Computing},
volume = {28},
number = {4},
pages = {669–696},
publisher = {Springer},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {article}
}
Mario Coppo, Mariangiola Dezani-Ciancaglini, Betti Venneri
Parallel Monitors for Self-adaptive Sessions Proceedings Article
In: PLACES'16, pp. 25–36, 2016.
Links | BibTeX | Tags: rephrase, semantics
@inproceedings{CDV16,
title = {Parallel Monitors for Self-adaptive Sessions},
author = {Mario Coppo and Mariangiola Dezani-Ciancaglini and Betti Venneri},
url = {http://www.di.unito.it/~dezani/papers/cdv16.pdf},
year = {2016},
date = {2016-01-01},
booktitle = {PLACES'16},
volume = {211},
pages = {25–36},
series = {EPTCS},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Nobuko Yoshida
Denotational and Operational Preciseness of Subtyping: A Roadmap Proceedings Article
In: Theory and Practice of Formal Methods, pp. 155–172, 2016.
Links | BibTeX | Tags: rephrase, semantics
@inproceedings{DGJPY16,
title = {Denotational and Operational Preciseness of Subtyping: A Roadmap},
author = {Mariangiola Dezani-Ciancaglini and Silvia Ghilezan and Svetlana Jaksic and Jovanka Pantovic and Nobuko Yoshida},
url = {http://www.di.unito.it/~dezani/papers/dgjpy16.pdf},
doi = {10.1007/978-3-319-30734-3_12},
year = {2016},
date = {2016-01-01},
booktitle = {Theory and Practice of Formal Methods},
volume = {9660},
pages = {155–172},
series = {LNCS},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
Mariangiola Dezani-Ciancaglini, Paola Giannini
Reversible Multiparty Sessions with Checkpoints Proceedings Article
In: EXPRESS/SOS'16, pp. 60–74, 2016.
Links | BibTeX | Tags: rephrase, semantics
@inproceedings{DG16,
title = {Reversible Multiparty Sessions with Checkpoints},
author = {Mariangiola Dezani-Ciancaglini and Paola Giannini},
url = {http://www.di.unito.it/~dezani/papers/dg16.pdf},
year = {2016},
date = {2016-01-01},
booktitle = {EXPRESS/SOS'16},
volume = {222},
pages = {60–74},
series = {EPTCS},
keywords = {rephrase, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
2012
Mario Coppo, Ferruccio Damiani, Maurizio Drocco, Elena Grassi, Eva Sciacca, Salvatore Spinella, Angelo Troina
Simulation techniques for the calculus of wrapped compartments Journal Article
In: Theoretical Computer Science, vol. 431, pp. 75–95, 2012.
Abstract | Links | BibTeX | Tags: semantics
@article{DBLP:journals/tcs/CoppoDDGSST12,
title = {Simulation techniques for the calculus of wrapped compartments},
author = {Mario Coppo and Ferruccio Damiani and Maurizio Drocco and Elena Grassi and Eva Sciacca and Salvatore Spinella and Angelo Troina},
doi = {10.1016/j.tcs.2011.12.063},
year = {2012},
date = {2012-01-01},
journal = {Theoretical Computer Science},
volume = {431},
pages = {75–95},
abstract = {The modelling and analysis of biological systems has deep roots in Mathematics, specifically in the field of Ordinary Differential Equations (ODEs). Alternative approaches based on formal calculi, often derived from process algebras or term rewriting systems, provide a quite complementary way to analyse the behaviour of biological systems. These calculi allow to cope in a natural way with notions like compartments and membranes, which are not easy (sometimes impossible) to handle with purely numerical approaches, and are often based on stochastic simulation methods. Recently, it has also become evident that stochastic effects in regulatory networks play a crucial role in the analysis of such systems. Actually, in many situations it is necessary to use stochastic models. For example when the system to be described is based on the interaction of few molecules, when we are at the presence of a chemical instability, or when we want to simulate the functioning of a pool of entities whose compartmentalised structure evolves dynamically. In contrast, stable metabolic networks, involving a large number of reagents, for which the computational cost of a stochastic simulation becomes an insurmountable obstacle, are efficiently modelled with ODEs. In this paper we define a hybrid simulation method, combining the stochastic approach with ODEs, for systems described in the Calculus of Wrapped Compartments (CWC), a calculus on which we can express the compartmentalisation of a biological system whose evolution is defined by a set of rewrite rules.},
keywords = {semantics},
pubstate = {published},
tppubtype = {article}
}
The modelling and analysis of biological systems has deep roots in Mathematics, specifically in the field of Ordinary Differential Equations (ODEs). Alternative approaches based on formal calculi, often derived from process algebras or term rewriting systems, provide a quite complementary way to analyse the behaviour of biological systems. These calculi allow to cope in a natural way with notions like compartments and membranes, which are not easy (sometimes impossible) to handle with purely numerical approaches, and are often based on stochastic simulation methods. Recently, it has also become evident that stochastic effects in regulatory networks play a crucial role in the analysis of such systems. Actually, in many situations it is necessary to use stochastic models. For example when the system to be described is based on the interaction of few molecules, when we are at the presence of a chemical instability, or when we want to simulate the functioning of a pool of entities whose compartmentalised structure evolves dynamically. In contrast, stable metabolic networks, involving a large number of reagents, for which the computational cost of a stochastic simulation becomes an insurmountable obstacle, are efficiently modelled with ODEs. In this paper we define a hybrid simulation method, combining the stochastic approach with ODEs, for systems described in the Calculus of Wrapped Compartments (CWC), a calculus on which we can express the compartmentalisation of a biological system whose evolution is defined by a set of rewrite rules.
2011
Mario Coppo, Ferruccio Damiani, Maurizio Drocco, Elena Grassi, Mike Guether, Angelo Troina
Modelling Ammonium Transporters in Arbuscular Mycorrhiza Symbiosis Journal Article
In: Transactions on Computational Systems Biology, vol. 6575, no. 13, pp. 85–109, 2011.
Abstract | Links | BibTeX | Tags: semantics
@article{DBLP:journals/tcsb/Coppo/DDGGT11,
title = {Modelling Ammonium Transporters in Arbuscular Mycorrhiza Symbiosis},
author = {Mario Coppo and Ferruccio Damiani and Maurizio Drocco and Elena Grassi and Mike Guether and Angelo Troina},
doi = {10.1007/978-3-642-19748-2_5},
year = {2011},
date = {2011-01-01},
journal = {Transactions on Computational Systems Biology},
volume = {6575},
number = {13},
pages = {85–109},
abstract = {The Stochastic Calculus of Wrapped Compartments (SCWC) is a recently proposed variant of the Stochastic Calculus of Looping Sequences (SCLS), a language for the representation and simulation of biological systems. In this work we apply SCWC to model a newly discovered ammonium transporter. This transporter is believed to play a fundamental role for plant mineral acquisition, which takes place in the arbuscular mycorrhiza, the most wide-spread plant-fungus symbiosis on earth. Investigating this kind of symbiosis is considered one of the most promising ways to develop methods to nurture plants in more natural manners, avoiding the complex chemical productions used nowadays to produce artificial fertilizers. In our experiments the passage of NH3/NH4+ from the fungus to the plant has been dissected in known and hypothetical mechanisms; with the model so far we have been able to simulate the behavior of the system under different conditions. Our simulations confirmed some of the latest experimental results about the LjAMT2;2 transporter. Moreover, by comparing the behaviour of LjAMT2;2 with the behaviour of another ammonium transporter which exists in plants, viz. LjAMT1;1, our simulations support an hypothesis about why LjAMT2;2 is so selectively expressed in arbusculated cells.},
keywords = {semantics},
pubstate = {published},
tppubtype = {article}
}
The Stochastic Calculus of Wrapped Compartments (SCWC) is a recently proposed variant of the Stochastic Calculus of Looping Sequences (SCLS), a language for the representation and simulation of biological systems. In this work we apply SCWC to model a newly discovered ammonium transporter. This transporter is believed to play a fundamental role for plant mineral acquisition, which takes place in the arbuscular mycorrhiza, the most wide-spread plant-fungus symbiosis on earth. Investigating this kind of symbiosis is considered one of the most promising ways to develop methods to nurture plants in more natural manners, avoiding the complex chemical productions used nowadays to produce artificial fertilizers. In our experiments the passage of NH3/NH4+ from the fungus to the plant has been dissected in known and hypothetical mechanisms; with the model so far we have been able to simulate the behavior of the system under different conditions. Our simulations confirmed some of the latest experimental results about the LjAMT2;2 transporter. Moreover, by comparing the behaviour of LjAMT2;2 with the behaviour of another ammonium transporter which exists in plants, viz. LjAMT1;1, our simulations support an hypothesis about why LjAMT2;2 is so selectively expressed in arbusculated cells.
2007
Marco Aldinucci, Marco Danelutto, Peter Kilpatrick
Management in distributed systems: a semi-formal approach Proceedings Article
In: Kermarrec, A. -M., Bougé, L., Priol, T. (Ed.): Proc. of 13th Intl. Euro-Par 2007 Parallel Processing, pp. 651–661, Springer, Rennes, France, 2007, ISBN: 978-3-540-74465-8.
Abstract | Links | BibTeX | Tags: parallel, semantics
@inproceedings{orc:europar:07,
title = {Management in distributed systems: a semi-formal approach},
author = {Marco Aldinucci and Marco Danelutto and Peter Kilpatrick},
editor = {A. -M. Kermarrec and L. Bougé and T. Priol},
url = {http://calvados.di.unipi.it/storage/paper_files/2007_orc_europar.pdf},
doi = {10.1007/978-3-540-74466-5},
isbn = {978-3-540-74465-8},
year = {2007},
date = {2007-08-01},
booktitle = {Proc. of 13th Intl. Euro-Par 2007 Parallel Processing},
volume = {4641},
pages = {651–661},
publisher = {Springer},
address = {Rennes, France},
series = {LNCS},
abstract = {The reverse engineering of a skeleton based programming environment and redesign to distribute management activities of the system and thereby remove a potential single point of failure is considered. The Orc notation is used to facilitate abstraction of the design and analysis of its properties. It is argued that Orc is particularly suited to this role as this type of management is essentially an orchestration activity. The Orc specification of the original version of the system is modified via a series of semi-formally justified derivation steps to obtain a specification of the decentralized management version which is then used as a basis for its implementation. Analysis of the two specifications allows qualitative prediction of the expected performance of the derived version with respect to the original, and this prediction is borne out in practice.},
keywords = {parallel, semantics},
pubstate = {published},
tppubtype = {inproceedings}
}
The reverse engineering of a skeleton based programming environment and redesign to distribute management activities of the system and thereby remove a potential single point of failure is considered. The Orc notation is used to facilitate abstraction of the design and analysis of its properties. It is argued that Orc is particularly suited to this role as this type of management is essentially an orchestration activity. The Orc specification of the original version of the system is modified via a series of semi-formally justified derivation steps to obtain a specification of the decentralized management version which is then used as a basis for its implementation. Analysis of the two specifications allows qualitative prediction of the expected performance of the derived version with respect to the original, and this prediction is borne out in practice.