-
Imprecise Probability for Multiparty Session Types in Process Algebra
Authors:
Bogdan Aman,
Gabriel Ciobanu
Abstract:
In this paper we introduce imprecise probability for session types. More exactly, we use a probabilistic process calculus in which both nondeterministic external choice and probabilistic internal choice are considered. We propose the probabilistic multiparty session types able to codify the structure of the communications by using some imprecise probabilities given in terms of lower and upper prob…
▽ More
In this paper we introduce imprecise probability for session types. More exactly, we use a probabilistic process calculus in which both nondeterministic external choice and probabilistic internal choice are considered. We propose the probabilistic multiparty session types able to codify the structure of the communications by using some imprecise probabilities given in terms of lower and upper probabilities. We prove that this new probabilistic ty** system is sound, as well as several other results dealing with both classical and probabilistic properties. The approach is illustrated by a simple example inspired by survey polls.
△ Less
Submitted 19 February, 2020;
originally announced February 2020.
-
Finitely Supported Sets Containing Infinite Uniformly Supported Subsets
Authors:
Andrei Alexandru,
Gabriel Ciobanu
Abstract:
The theory of finitely supported algebraic structures represents a reformulation of Zermelo-Fraenkel set theory in which every construction is finitely supported according to the action of a group of permutations of some basic elements named atoms. In this paper we study the properties of finitely supported sets that contain infinite uniformly supported subsets, as well as the properties of finite…
▽ More
The theory of finitely supported algebraic structures represents a reformulation of Zermelo-Fraenkel set theory in which every construction is finitely supported according to the action of a group of permutations of some basic elements named atoms. In this paper we study the properties of finitely supported sets that contain infinite uniformly supported subsets, as well as the properties of finitely supported sets that do not contain infinite uniformly supported subsets. For classical atomic sets, we study whether they contain or not infinite uniformly supported subsets.
△ Less
Submitted 4 September, 2019;
originally announced September 2019.
-
Probabilities in Session Types
Authors:
Bogdan Aman,
Gabriel Ciobanu
Abstract:
This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a ty** system which extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its ty** system are motivated and illu…
▽ More
This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a ty** system which extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its ty** system are motivated and illustrated by a running example.
△ Less
Submitted 4 September, 2019;
originally announced September 2019.
-
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
Authors:
Ross Horne,
Alwen Tiu,
Bogdan Aman,
Gabriel Ciobanu
Abstract:
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' dis…
▽ More
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkee** enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.
△ Less
Submitted 15 January, 2020; v1 submitted 18 February, 2016;
originally announced February 2016.
-
Local Type Checking for Linked Data Consumers
Authors:
Gabriel Ciobanu,
Ross Horne,
Vladimiro Sassone
Abstract:
The Web of Linked Data is the cumulation of over a decade of work by the Web standards community in their effort to make data more Web-like. We provide an introduction to the Web of Linked Data from the perspective of a Web developer that would like to build an application using Linked Data. We identify a weakness in the development stack as being a lack of domain specific scripting languages for…
▽ More
The Web of Linked Data is the cumulation of over a decade of work by the Web standards community in their effort to make data more Web-like. We provide an introduction to the Web of Linked Data from the perspective of a Web developer that would like to build an application using Linked Data. We identify a weakness in the development stack as being a lack of domain specific scripting languages for designing background processes that consume Linked Data. To address this weakness, we design a scripting language with a simple but appropriate type system. In our proposed architecture some data is consumed from sources outside of the control of the system and some data is held locally. Stronger type assumptions can be made about the local data than external data, hence our type system mixes static and dynamic ty**. Throughout, we relate our work to the W3C recommendations that drive Linked Data, so our syntax is accessible to Web developers.
△ Less
Submitted 1 August, 2013;
originally announced August 2013.
-
Proceedings 6th Workshop on Membrane Computing and Biologically Inspired Process Calculi
Authors:
Gabriel Ciobanu
Abstract:
This volume contains the papers presented at the 6th Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2012), a satellite workshop of the 23rd International Conference on Concurrency Theory (CONCUR) held on 8th September 2012 in Newcastle upon Tyne, UK.
This volume contains the papers presented at the 6th Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2012), a satellite workshop of the 23rd International Conference on Concurrency Theory (CONCUR) held on 8th September 2012 in Newcastle upon Tyne, UK.
△ Less
Submitted 14 November, 2012;
originally announced November 2012.
-
A Provenance Tracking Model for Data Updates
Authors:
Gabriel Ciobanu,
Ross Horne
Abstract:
For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. In this paper, a concise but expressive calculus which models data updates is presented. The calculus is used to provide an operational semantics for a system where data and updates interact concurrently. The operational semantics of the calculus also t…
▽ More
For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. In this paper, a concise but expressive calculus which models data updates is presented. The calculus is used to provide an operational semantics for a system where data and updates interact concurrently. The operational semantics of the calculus also tracks the provenance of data with respect to updates. This provides a new formal semantics extending provenance diagrams which takes into account the execution of processes in a concurrent setting. Moreover, a sound and complete model for the calculus based on ideals of series-parallel DAGs is provided. The notion of provenance introduced can be used as a subjective indicator of the quality of data in concurrent interacting systems.
△ Less
Submitted 22 August, 2012;
originally announced August 2012.
-
Proceedings of the 5th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2011)
Authors:
Gabriel Ciobanu
Abstract:
This volume represents the proceedings of the 5th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2011), held together with the 12th International Conference on Membrane Computing on 23rd August 2011 in Fontainebleau, France.
This volume represents the proceedings of the 5th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2011), held together with the 12th International Conference on Membrane Computing on 23rd August 2011 in Fontainebleau, France.
△ Less
Submitted 18 August, 2011; v1 submitted 17 August, 2011;
originally announced August 2011.
-
Biologically Inspired Process Calculi, Petri Nets and Membrane Computing
Authors:
Gabriel Ciobanu
Abstract:
This volume represents the proceedings of the 5th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2011), held together with the 12th International Conference on Membrane Computing on 23rd August 2011 in Fontainebleau, France.
This volume represents the proceedings of the 5th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2011), held together with the 12th International Conference on Membrane Computing on 23rd August 2011 in Fontainebleau, France.
△ Less
Submitted 17 August, 2011;
originally announced August 2011.
-
Time Delays in Membrane Systems and Petri Nets
Authors:
Bogdan Aman,
Gabriel Ciobanu
Abstract:
Timing aspects in formalisms with explicit resources and parallelism are investigated, and it is presented a formal link between timed membrane systems and timed Petri nets with localities. For both formalisms, timing does not increase the expressive power; however both timed membrane systems and timed Petri nets are more flexible in describing molecular phenomena where time is a critical resource…
▽ More
Timing aspects in formalisms with explicit resources and parallelism are investigated, and it is presented a formal link between timed membrane systems and timed Petri nets with localities. For both formalisms, timing does not increase the expressive power; however both timed membrane systems and timed Petri nets are more flexible in describing molecular phenomena where time is a critical resource. We establish a link between timed membrane systems and timed Petri nets with localities, and prove an operational correspondence between them.
△ Less
Submitted 6 July, 2011;
originally announced July 2011.
-
Proceedings Fourth Workshop on Membrane Computing and Biologically Inspired Process Calculi 2010
Authors:
Gabriel Ciobanu,
Maciej Koutny
Abstract:
The 4th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2010) is organized in Jena as a satellite event of the Eleventh International Conference on Membrane Computing (CMC11). Biological membranes play a fundamental role in the complex reactions which take place in cells of living organisms. The importance of this role has been considered in two different types of…
▽ More
The 4th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2010) is organized in Jena as a satellite event of the Eleventh International Conference on Membrane Computing (CMC11). Biological membranes play a fundamental role in the complex reactions which take place in cells of living organisms. The importance of this role has been considered in two different types of formalisms introduced recently. Membrane systems were introduced as a class of distributed parallel computing devices inspired by the observation that any biological system is a complex hierarchical structure, with a flow of biochemical substances and information that underlies their functioning. The modeling and analysis of biological systems has also attracted considerable interest of the process algebra research community. Thus the notions of membranes and compartments have been explicitly represented in a family of calculi, such as ambients and brane calculi. A cross fertilization of these two research areas has recently started. A deeper investigation of the relationships between these related formalisms is interesting, as it is important to understand the crucial similarities and the differences. The main aim of the workshop is to bring together researchers working on membrane computing, in biologically inspired process calculi, and in other related fields, in order to present recent results and to discuss new ideas concerning such formalisms, their properties and relationships.
△ Less
Submitted 30 October, 2010;
originally announced November 2010.
-
Proceedings Third Workshop on Membrane Computing and Biologically Inspired Process Calculi 2009
Authors:
Gabriel Ciobanu
Abstract:
This volume contains the accepted papers at the third Workshop on Membrane Computing and Biologically Inspired Process Calculi, held in Bologna on 5th September 2009. The papers are devoted to both membrane computing and biologically inspired process calculi, as well as to other related formalisms. The papers of this volume are selected by the programme committee due to their quality and relevan…
▽ More
This volume contains the accepted papers at the third Workshop on Membrane Computing and Biologically Inspired Process Calculi, held in Bologna on 5th September 2009. The papers are devoted to both membrane computing and biologically inspired process calculi, as well as to other related formalisms. The papers of this volume are selected by the programme committee due to their quality and relevance; they have defined an exciting programme highlighting interesting problems and stimulating the search for novel ways of describing related biological phenomena. In addition, we had an invited talk given by Luca Cardelli on a spatial process algebra for developmental biology. Membrane systems were introduced as a class of distributed parallel computing devices inspired by the observation that any biological system is a complex hierarchical structure, with a flow of materials and information that underlies their functioning. The emphasis is on the computational properties of the model, and it makes use of automata, languages, and complexity theoretic tools. On the other hand, certain calculi such as mobile ambients and brane calculi work with similar notions (compartments, membranes). These calculi are used to model and analyze the various biological systems. The workshop on Membrane Computing and Biologically Inspired Process Calculi brings together researchers working in these fields to present their recent work and discuss new ideas concerning the formalisms, their properties and relationships.
△ Less
Submitted 30 November, 2009;
originally announced December 2009.
-
Mutual Mobile Membranes with Timers
Authors:
Bogdan Aman,
Gabriel Ciobanu
Abstract:
A feature of current membrane systems is the fact that objects and membranes are persistent. However, this is not true in the real world. In fact, cells and intracellular proteins have a well-defined lifetime. Inspired from these biological facts, we define a model of systems of mobile membranes in which each membrane and each object has a timer representing their lifetime. We show that systems…
▽ More
A feature of current membrane systems is the fact that objects and membranes are persistent. However, this is not true in the real world. In fact, cells and intracellular proteins have a well-defined lifetime. Inspired from these biological facts, we define a model of systems of mobile membranes in which each membrane and each object has a timer representing their lifetime. We show that systems of mutual mobile membranes with and without timers have the same computational power. An encoding of timed safe mobile ambients into systems of mutual mobile membranes with timers offers a relationship between two formalisms used in describing biological systems.
△ Less
Submitted 7 October, 2009;
originally announced October 2009.
