arXiv subjects

Bogdan Aman

Publications and source records attributed to Bogdan Aman.

6 recordsLinked to original sources

arXiv2020

Imprecise Probability for Multiparty Session Types in Process Algebra

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 typing 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.

cs.LO↗

arXiv2020

De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic

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 bookkeeping 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.

cs.LO↗

arXiv2019

Probabilities in Session Types

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 typing system which extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its typing system are motivated and illustrated by a running example.

cs.LO↗

arXiv2011

Spatial Dynamic Structures and Mobility in Computation

Membrane computing is a well-established and successful research field which belongs to the more general area of molecular computing. Membrane computing aims at defining parallel and non-deterministic computing models, called membrane systems or P Systems, which abstract from the functioning and structure of the cell. A membrane system consists of a spatial structure, a hierarchy of membranes which do not intersect, with a distinguishable membrane called skin surrounding all of them. A membrane without any other membranes inside is elementary, while a non-elementary membrane is a composite membrane. The membranes define demarcations between regions; for each membrane there is a unique associated region. Since we have a one-to-one correspondence, we sometimes use membrane instead of region, and vice-versa. The space outside the skin membrane is called the environment. In this thesis we define and investigate variants of systems of mobile membranes as models for molecular computing and as modelling paradigms for biological systems. On one hand, we follow the standard approach of research in membrane computing: defining a notion of computation for systems of mobile membranes, and investigating the computational power of such computing devices. Specifically, we address issues concerning the power of operations for modifying the membrane structure of a system of mobile membranes by mobility: endocytosis (moving a membrane inside a neighbouring membrane) and endocytosis (moving a membrane outside the membrane where it is placed). On the other hand, we relate systems of mobile membranes to process algebra (mobile ambients, timed mobile ambients, pi-calculus, brane calculus) by providing some encodings and adding some concepts inspired from process algebra in the framework of mobile membrane computing.

cs.DC↗

arXiv2011

Time Delays in Membrane Systems and Petri Nets

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.

cs.DC↗

arXiv2009

Mutual Mobile Membranes with Timers

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.

cs.FL↗