Main objectives

We studied indexed multisets in the context of multiset rewriting systems, using indexes to capture the number of the step in which a rule is applied or an object is produced [L1]. We showed that the evolution of a multiset rewriting system is accurately reflected by its indexed version and we extended this result to maximal parallelism. We analysed situations in which indexed rule application can be postponed, and introduced an equivalence relation based on such situations. We introduced the notions of cause and of causal chains, and showed how adding indexes allows us to decompose evolution into independent causal chains.

We defined a stochastic version of the fusion calculus [L2]. The stochastic nature is evident in the labelled transition system providing the operational semantics of stochastic fusion calculus, where labels represent the rates corresponding to exponential distributions. We extended the notion of hyperbisimulation to stochastic fusion calculus, and prove that the stochastic hyperequivalence is a congruence.

We introduced and studied Scenario Based P Systems in order to model computation inspired by metabolic pathways and networks [L3]. Starting from the classical definition of P systems with symbol objects and multiset rewriting rules, we use regular expressions able to capture the causal dependencies among different executions of the rules. The presented results prove the computational power of this model.

We showed that a class of mobile membranes using only elementary division and mobility can provide a semi-uniform polynomial solutions for the 4QBF problem, ascending to the fourth level in the polynomial hierarchy [L4].

We studied mobile membranes with objects on surface  and used this class of mobile membranes to model the low-density lipoprotein degradation [L5]. A translation of this formalism into colored Petri nets is provided in order to analyze, using CPN Tools, some important properties of mobile membranes: reachability, boundedness, liveness, fairness. CPN Tools (http://cs.au.dk/CPnets/) are a software tool for editing, simulating, and analyzing colored Petri nets.

Mobile membranes represent a variant of membrane systems in which the main operations are inspired by the biological operations of endocytosis and exocytosis. We studied the computational power of mobile membranes, proving an optimal computability result: three membranes are enough to have the same computational power as a Turing machine [L6, L13]. Regarding the computational complexity, we presented a semiuniform polynomial solution for a strong NP-complete problem (SAT problem) by using only endocytosis, exocytosis and elementary division.

We extended the TiMo family by introducing a real-time version named rTiMo [L7, L15]. Real-time constraints are used to control migration and communication in a real-time distributed system. In order to verify several properties of complex mobile systems described in rTiMo, we establish a relationship between rTiMo networks and a class of timed safety automata. The relationship allows the verification of temporal properties of real-time migrating processes using Uppaal capabilities (http://www.uppaal.org/).

We provided 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 [L8, L17]. We identified 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 designed 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 typing.

We defined pTiMo, a process algebra in which migrations and interactions depend upon timers and have probabilities [L9, L18]. The semantics of the calculus is given in terms of labeled, discrete-time Markov chains. The existing quantitative tools do not explicitly support properties which make use of local clocks, multisets of transitions and transition provenance. In order to study such properties, we introduced a probabilistic temporal logic PLTM for pTiMo, provided an algorithm for verifying PLTM properties, and analyzed its time complexity.

We created a tool, called TiMo@PAT, developed by using Process Analysis Toolkit (PAT - http://www.comp.nus.edu.sg/~pat/), an extensible platform for model checkers [L10, L19]. We illustrated the capability of TiMo@PAT by analysing some properties of a distributed system. A review of all research directions related to the family of process calculi Timo was presented in [L16].

We presented two approaches, namely correlative and static causality, to study cause-effect relationships in reaction models and we proposed a framework which integrates them in order to study causality by means of transition P systems [L11]. The proposed framework is based on the fact that statistical analysis can be used to building up a membrane model which can be used to analyze causality relationships in terms of multisets of objects and rules in presence of non-determinism and parallelism.We proved that the P system that is defined by means of correlation analysis provides a correspondence between the static and correlative notions of causality.

We defined a real-time extension of P systems in which each membrane and each object has a lifetime attached to it, and we used these lifetimes to define and study various behavioural equivalences [L12]. We also established sufficient conditions for guaranteeing progression over time.

Inspired by the functioning of the sodium-potassium pump, we introduced and studied a ratio-based type system using thresholds in a bio-inspired formalism [L14]. The intent is to avoid errors in the definition of the formal model used to model biologic processes. For this type system we proved a subject reduction theorem.

We presented the concept of "event structures" in the nominal framework of the Fraenkel-Mostowski model of set theory [L20]. Using specific techniques of nominal logic, we introduce and study the nominal event structures, providing some properties. The analogy between the results obtained by using the Fraenkel-Mostowski axioms and those obtained by using the Zermelo-Fraenkel axioms is discussed.

We presented a nominal semantics of the pi-calculus defined by a set of compact transition employing a nominal quantifier [L21]. We analyzed the behavior of the pi-calculus binding operators new and input, and presented several nominal properties of new and input. We made a comparison of expressiveness between the nominal semantics of the pi-calculus and other known semantics; we proved that the nominal semantics and the late semantics of the pi-calculus have the same expressive power.

We defined a nominal semantics of the monadic version of the fusion calculus (also called update calculus) [L22]. A set of compact transition rules is given in terms of nominal logic by using a specific nominal quantifier. Based on known and new results in nominal logic, we proved an equivalence between the new nominal semantics and the old (original) semantics (Parrow-Victor) of the monadic fusion calculus, emphasizing the benefits of presenting the transition rules by using nominal techniques.

We considered catalytic membrane systems and catalytic Petri nets. We added discrete timers to these classes, and prove that the timed formalisms (𝑡𝐶𝑎𝑡𝑀𝑆 and 𝑡𝐶𝑎𝑡𝑃𝑁) can be expressed by their untimed versions if finite timers are used. We established formal links between these formalisms, and characterized some subclasses in which various properties are decidable and can be analyzed using CPN Tools.

For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. We defined a concise but expressive calculus which models data updates [L24]. The operational semantics of the calculus 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 technical report [TR1] presents some case studies that use stochastic calculi in order to model human computer interactions.

[L5] B. Aman, G. Ciobanu. Mobile Membranes with Objects on Surface as Colored Petri Nets. Lecture Notes in Computer Science, vol.7762, 128-144, 2013.

[L6] B. Aman, G. Ciobanu. Mobile Membranes: Computability and Complexity. Lecture Notes in Computer Science, vol.8049, 59-75, 2013.

[L7] B. Aman, G. Ciobanu. Real-Time Migration Properties of rTiMo Verified in Uppaal. Lecture Notes in Computer Science, vol.8137, 31-45, 2013.

[L8] G. Ciobanu, R. Horne, V. Sassone. Local Type Checking for Linked Data Consumers. Electronic Proceedings in Theoretical Computer Science, vol.123, 19-33-44, 2013.

[L9] G. Ciobanu, A. Rotaru. A Probabilistic Logic for pTiMo. Lecture Notes in Computer Science, vol.8049, 141-158, 2013.

[L10]  G. Ciobanu and M. Zheng, Verifying TiMo systems in PAT. ICECCS, IEEE 2013, 121-124, 2013.

[L11] R. Pagliarini, O. Agrigoroaiei, G. Ciobanu, V. Manca. An Analysis of Correlative and Static Causality in P Systems. Lecture Notes in Computer Science, vol.7762, 323-341, 2013.