Formal Methods Laboratory
~ Technical Reports ~

FML-15-02

 [FML-06-02] Ross Horne, Alwen Tiu, Bogdan Aman, Gabriel Ciobanu. Private Names in Non-Commutative Logic.pp 58, May, 2015 ISSN 1842 - 1490 Abstract (click to show/hide) We present an expressive but decidable first-order system (named MAV1) defined by using the calculus of structures, a generalisation of the sequent calculus. In addition to first-order universal and existential quantifiers the system incorporates a pair of nominal quantifiers called new' and wen', distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these operators 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 as required in applications such as the verification of security protocols. Due to the presence of a self-dual non-commutative operator, a direct proof of cut elimination for first-order quantifiers in the calculus of structures is necessary; contrasting to related results for first-order quantifiers in the calculus of structures which rely on a correspondence with the sequent calculus. As a consequence of cut elimination, the complexity classes for provability in MAV1 and several sub-systems are established. Download: pdf (496 KB)

FML-15-01

 [FML-06-02] Andrei Alexandru, Gabriel Ciobanu Consistence of Choice Principles in Finitely Supported Mathematics.pp 28, April, 2015ISSN 1842 - 1490 Abstract (click to show/hide) Finitely Supported Mathematics represents a part of mathematics for experimental sciences which has a continuous evolution in the last century. It is developed according to the Fraenkel-Mostowski axioms of set theory. The axiom of choice is inconsistent in the Finitely Supported Mathematics. We prove that several weaker forms of the axiom of choice are also inconsistent in the Finitely Supported Mathematics. Download: pdf (289 KB)

FML-14-02

 [FML-06-02] Gabriel Ciobanu, Eneia Nicolae Todoran Correct Metric Semantics for a Biologically-Inspired Formalism.pp 41, September, 2014 (Revised: April, 2015) ISSN 1842 - 1490 Abstract (click to show/hide) We investigate a language similar to a process algebra for DNA computing introduced by Cardelli. For such a language we relate two formal semantics. We define a new denotational semantics by using complete metric spaces, in which various semantic functions are defined as fixed points of appropriate higher-order mappings. We compare this denotational semantics with an operational semantics, and establish a formal relationship between them by using an abstraction operator and a fixed point argument. In this way we prove the correctness of the denotational semantics with respect to the operational one. Download: pdf (395 KB)

FML-14-01

 [FML-06-02] Gabriel Ciobanu, Armand Rotaru Phase-Type Approximations for Non-Markovian Systems.pp 35, June, 2014 ISSN 1842 - 1490 Abstract (click to show/hide) We introduce a novel stochastic process algebra, called PHASE, which directly supports phase-type distributions, useful for approximating the dynamics of non-Markovian HCI systems. In order to encourage the effective use of PHASE, we give a step by step account of how PHASE processes can be implemented in PRISM, one of the most powerful and popular probabilistic model checkers currently available. Furthermore, we provide a case study involving a non-Markovian interactive system, as a means of highlighting the advantages of phase-type approximations, in comparison to approximating non-Markovian transitions through single Markovian transitions. Download: pdf (358 KB)

FML-13-02

 [FML-06-02] Andrei Alexandru, Gabriel Ciobanu. Nominal Generalized Multisets.pp 27, September, 2013 ISSN 1842 - 1490 Abstract (click to show/hide) We present generalized multisets both in the Zermelo-Fraenkel and in the Fraenkel-Mostowski frameworks. We extend the notion of generalized multiset over a finite alphabet, and we replace it by the notion of algebraically finitely supported generalized multiset over a possibly infinite alphabet. We study the correspondence between some properties of generalized multisets obtained in the Fraenkel-Mostowski framework where only finitely supported objects are allowed, and those obtained in the classical Zermelo-Fraenkel  framework. Download: pdf (275 KB)

FML-13-01

 [FML-06-02] Gabriel Ciobanu, Armand Rotaru. Stochastic Process Calculi for Human-Computer Interaction.pp 30, February, 2013 ISSN 1842 - 1490 Abstract (click to show/hide) Several recent studies have shown that stochastic process calculi are very suitable for the modelling of human-computer interaction. In this survey, we review some of the most promising such studies, as a means of highlighting the potential of a formal stochastic approach to analysing interactive systems. For each case study, we describe the context in which the approach is applied, the theoretical tools (i.e., stochastic process calculi and cognitive architectures) underlying the approach, the resulting formal models, and the performance measures which are derived from the models. Also, we identify a set of strong points and weaknesses that are associated with the approach. Download: pdf (1.1 MB)

FML-12-02

 [FML-06-02] Gabriel Ciobanu, Eneia Nicolae Todoran. Abstract Continuation Semantics for Asynchronous Concurrency.pp 36, December, 2012 ISSN 1842 - 1490 Abstract (click to show/hide) The technical report presents a denotational semantics of a simple asynchronous language designed with metric spaces and continuation semantics for concurrency. The denotational model satisfies anoptimality criterion that we call weak abstractness. Download: pdf (343 KB)
FML-12-01

 [FML-06-02] Gabriel Ciobanu, Armand Rotaru. A Probabilistic Query Language for Migrating Processes with Timers.pp 31, November, 2012 ISSN 1842 - 1490 Abstract (click to show/hide) In this paper we present pTiMo, a process algebra in which migrations and interactions depend upon timers and have probabilies. The semantics of the calculus is given in terms of generative probabilistic automata. Quantitative tools (e.g., PRISM) do not explicitly support properties which make use of local clocks, multisets of transitions (generated by the maximal progress policy in pTiMo) and transition provenance (the location at which a transition originates, and/or the processes that participate in the transition). In order to study such properties, we define a quantitative query language PLTM for pTiMo and provide an algorithm for answering PLTM queries. PLTM includes a probabilistic query language over states and/or transitions, for both transient and steady-state behavior, and a set of properties related to cost/reward structures. Download: pdf (312 KB)

FML-11-02

 [FML-06-02] Bogdan Aman, Gabriel Ciobanu. Solving Weak NP-Complete Problems with Mutual Mobile Membrane Systems.pp 26, October, 2011 ISSN 1842 - 1490 Abstract (click to show/hide) Mutual mobile membranes represent a variant of mobile membranes in which endocytosis and exocytosis work whenever the involved membranes agree'' on the movement; this agreement is described by using mutual complement objects placed in the relevant membranes. The paper provides semiuniform polynomial solutions for several NP-complete problems (Knapsack, Subset Sum, Partition) by means of systems of mutual mobile membranes, showing that elementary membrane division and membrane communication suffice (there is no need for polarizations nor non-elementary membrane division). Download: pdf (276 KB)

FML-11-01

 [FML-06-02] Gabriel Ciobanu. Biologically Inspired Process Calculi, Petri Nets and Membrane Computing.pp 121, September, 2011 ISSN 1842 - 1490 Abstract (click to show/hide) This technical report 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. Download: pdf (1.4 MB)

FML-10-03

 [FML-06-02] Andrei Alexandru, Gabriel Ciobanu. A Nominal Approach to Mobility in pi-Calculus.pp 58, November, 2010 ISSN 1842 - 1490 Abstract (click to show/hide) We give a new semantics called the nominal semantics of the pi-calculus which is defined by using nominal techniques. A set of transition rules is given in terms of nominal logic by using a nominal quantifier. The mobility of links in the virtual space of linked processes is described in this new semantics by using a new rule which have no analogue in the other known semantics of the pi-calculus. It is also analyzed the behaviour of the pi-calculus binding operators new and input. The binding operator new is expressed as a freshness operator in terms of an alpha-abstraction. Several properties of new and input, obtained by using this new semantics, are described in section 4. Also, in the last part of this paper, we present an example of how the nominal techniques can be used to rewrite the transition rules from a certain calculi in a compact form, with no logical contradiction. Download: pdf (500 KB)

FML-10-02

 [FML-06-02] Gabriel Ciobanu, Eneia Nicolae Todoran. Continuation Semantics for Asynchronous Concurrency.pp 41, October, 2010 (Revised: August, 2013) ISSN 1842 - 1490 Abstract (click to show/hide) The paper presents a method of reasoning about the behavior of asynchronous programs in denotational models designed with metric spaces and continuation semantics for concurrency. Download: pdf (364 KB)

FML-10-01

 [FML-06-02] Gabriel Ciobanu, Maciej Koutny. TiMoTy: Timed Mobility with Types.pp 27, January, 2010 ISSN 1842 - 1490 Abstract (click to show/hide) In this paper we introduce a simple process algebra able to model the systems composed of processes which may migrate within a distributed environment comprising a number of distinct locations. Two processes may communicate if they are present in the same location and, in addition, they have appropriate access permissions (put or get) to communicate over a shared channel. Access permissions are dynamic, and processes can acquire new access permissions or lose some existing permissions while moving from one location to another. Finally, timing constraints allow one to control the communication between processes and migration between locations. We define an operational semantics, and introduce a type system aimed at identifying situations when a pro- cess enters a state in which it cannot communicate with other processes due to not having enough access permissions to do so. We then show that the developed type system is sound and complete for ensuring safety of communication for networks of migrating processes. Such a result is of key relevance from the point of view of ensuring security in a dynamic environments involving timed migration and communication. Download: pdf (552 KB)

FML-09-02

 [FML-06-02] Gabriel Ciobanu, Eneia Nicolae Todoran. Continuation Semantics for Concurrency.pp 53, April, 2009 (Revised: January, 2014) ISSN 1842 - 1490 Abstract (click to show/hide) This paper presents a continuation semantics satisfying the basic laws of concurrent systems. This semantics is illustrated for a simple CSP-like language extended with communication on multiple channels and synchronization based on join patterns, which also provides operators for nondeterministic choice, sequential and parallel composition. For the language under investigation we present a denotational semantics. Then we prove that the semantic operators designed with continuations obey the concurrency laws such as the associativity or the commutativity of parallel composition. The significance of the results is given mainly by the flexibility provided by the continuations technique which can thus be used to describeconcurrent behaviour. Download: pdf (401k KB)

FML-09-01

 [FML-06-02] Gabriel Ciobanu, Calin Juravle. MCTools: A Software Platform for Mobility and Timed Interaction.pp 28, February, 2009 ISSN 1842 - 1490 Abstract (click to show/hide) TiMo is a process algebra using timeouts for interactions and adaptable migration between explicit locations. Starting from is a process algebra using timeouts for interactions and adaptable migration between explicit locations. Starting from this formalism, we have implemented a software framework for agent migration, separating the migration mechanism such that it can be reused for other systems with mobility. We describe the frameworks architectures and functionalities, the software modules and some implementation details, emphasizing the novel aspects and comparing with similar implementations. The implementation corresponds rigorously to the semantics of TiMo. An example illustrates the use of the migration framework for a simple problem. Download: pdf (860 KB)

FML-08-03

 [FML-06-02] Andreas Resios, Gabriel Ciobanu. Abstract Machine for Mobile Ambients. pp 25, October, 2008 ISSN 1842 - 1490 Abstract (click to show/hide) In this paper we study aspects of agent mobility in distributed systems. We propose a formalism for describing such systems that deals with two fundamental problems: agent interference and agent synchronization. The formalism, named safeCMA, is based on ambient calculus and it combines aspects from Safe Ambients and Coordinated Mobile Ambients to adequately model the agents behavior in such systems. To develop a software language for such systems we introduce an abstract machine for safeCMA. We facilitate the study of distributed systems by providing a software implementation for the abstract machine. Download: pdf (508 KB)

FML-08-02

 [FML-06-02] Calin Juravle, Gabriel Ciobanu. Distributed Implementation of Mobility based Formalisms. pp 30, October, 2008 ISSN 1842 - 1490 Abstract (click to show/hide) Mobility is a hot topic in both theoretical and practical part of computer science. Lately, an increasing number of formalisms and software applications appeared in order to offer means to reason and experience with mobile agents. We present a simple yet powerful framework for mobility, which purpose is to help one to develop implementation for various mobile systems. In particular, our framework is designed to be a base for implementation of formalisms for mobility, but not restricted to it. It consists of several modules each of them offering specific features such as implementations of the common abstract notions from various formalisms for mobility (names, agents, locations etc.); a mobility mechanism which make possible agents migration; an engine for formal simulation of agents described in a specific formalism. Over this platform we implemented two formalism, dpi-calculus and tiMo. We support their soundness through several claims. Download: pdf (792 KB)

FML-08-01

 [FML-06-02] Gabriel Ciobanu, Stefan Rusu. Verifying Adaptative Cruise Control by Using Pi-Calculus and Mobility Workbench. pp 21, October, 2008 ISSN 1842 - 1490 Abstract (click to show/hide) Adaptive Cruise Control is used to maintain the speed of a vehicle in a predefined interval. Such an automotive system can automatically adjust the speed in order to maintain a proper distance between vehicles in the same lane. In this paper we first describe Adaptive Cruise Control by using a process algebra called pi-calculus; such a formal description consists of diagrams, equations, formal semantics, properties, system optimizations and verification. Mobility Workbench is used as a software tool for verification. Download: pdf (344 KB)

FML-07-01

 [FML-06-02] Bogdan Aman, Gabriel Ciobanu. Translating Safe Ambients into Mobile Membranes. pp 41, January, 2007 ISSN 1842 - 1490 Abstract (click to show/hide) We establish a relationship between two formalisms used in describing biological systems. We translate some notions from the ambient calculus into the formalism of membrane systems. Thus we consider the exhibit of an ambient, its level, the structural congruence, and the contextual bisimulation in order to define and study in membrane systems the corresponding observation barbs, the depths of a membrane system, the structural congruence and the contextual bisimulation. We describe the sodium-potassium exchange pump in both membrane systems and safe ambients. We also compare the direct description of the pump using the membrane systems with the description obtained through the translation from safe ambients. Download: pdf (360 KB)

FML-06-04

 [FML-06-02] Gabriel Ciobanu, Laura Cornacel. Expressing biological many-to-many interactions by stochastic fusion. pp 28, September, 2006 ISSN 1842 - 1490 Abstract (click to show/hide) In this paper we present a stochastic approach to fusion calculus. Stochastic fusion calculus is suitable to describe the dynamic behaviour of complex systems involving many-to-one or many-to-many interactions. We extend the semantics of the fusion calculus from labelled transition system to stochastic labelled transition system where the evolution of a system is driven by probabilistic distributions. In particular, we analyze the stochastic distribution of the synchronization between interacting processes. We define and study a stochastic hyperequivalence, and present an axiomatic system for it. An example describing the DNA transcription initiation illustrates the modelling power of the new formalism. Download: pdf (312 KB)

FML-06-03

 [FML-06-02]Bogdan Aman, Gabriel Ciobanu. Mobile ambients with time constraints. pp 22, September, 2006 ISSN 1842 - 1490 Abstract (click to show/hide) Mobile ambients calculus is a calculus for mobile computing able to express local communications inside ambients, as well as movement and dissolution of ambients by consuming capabilities. We add timers to communication channels, capabilities and ambients. We provide a static semantic given by a typing system, and an operational semantics of the new calculus given by a reduction relation. The passage of time is given by a (discrete) time stepping function. We prove that structural congruence and passage of time do not interfere with the typing system. A subject reduction result assures that once well-typed, an ambient remains well-typed. We provide some bisimulation relations with regard to the passage of time. A timed extension of the cab protocol illustrates how the new formalism is working. Download: pdf (240 KB)

FML-06-02

 [FML-06-02] Bogdan Aman, Gabriel Ciobanu. On the Relationship Between P Systems and Mobile Ambients. pp 33, July, 2006 ISSN 1842 - 1490 Abstract (click to show/hide) We compare the membrane systems to mobile ambients which represent another modelling formalism used in system biology. We prove several properties regarding the relationship between membrane systems and mobile ambients given by an encoding of the mobile ambients into P systems with mobile membranes and developmental rules. We give an operational correspondence between ambients and their P systems, defining also an operational correspondence. Download: pdf (520 KB)

FML-06-01

 [FML-06-01] Cristian Prisacariu, Gabriel Ciobanu. Technical Aspects of Timed Distributed pi-calculus. pp 41, May, 2006 ISSN 1842 - 1490 Abstract (click to show/hide) Timed distributed pi-calculus extends the distributed pi-calculus of Hennessy and Riely with timers transforming the channels into temporary resources. Distributed pi-calculus describes controlled interactions between processes with restricted access to resources. We allow extra time constraints by considering a notion of timeout for channels. Combining timers with types and locations, timed distributed pi-calculus is a formal framework able to describe complex systems with constraints on time and on resource access. We study the process behaviour by giving twelve barbed bisimulations and comparing their power of distinguishing over the timed located processes. These results are visualised in a lattice. We also extend a technique based on embeddings among languages to prove that tDpi is more expressive than the underlying Dpi. The technique can be used in a general with any message passing calculi as it is based on barbed bisimulation. In order to confer a more realistic model we extend the flat space of locations with locations trees and failures. This enables $tD\pi$ to model systems with hierarchical location structure as are the administrative domains of the Internet or the compartments in biology. Download: pdf (588 KB)

FML-05-02

 [FML-05-02] Laura Cornacel, Gabriel Ciobanu. Translating Probabilistic Labelled Transition Systems into Discrete-Time Markov Chains. pp 25, November, 2005 ISSN 1842 - 1490 Abstract (click to show/hide) In this paper we describe a way of deriving discrete-time Markov chains from generative probabilistic labelled transition systems. We start with some notations and definitions from probability theory, recalling geometric distribution and discrete-time Markov chains which are time-homogeneous. Then we refer to generative probabilistic labelled transition systems which arise from ordinary labelled transition systems. After defining the rules through which such a probabilistic labelled transition system can be inferred, we show how a Markov chain can be derived from a probabilistic labelled transition system. We introduce a language for describing discrete-time Markov chains, together with its operational semantics defined by rules. Then we define the translation from probabilistic labelled transition systems into discrete-time Markov chains; this translation is well-defined and bijective. We introduce a notion of bisimulation for discrete-time Markov chains, and prove a certain operational correspondence: namely, for any two bisimilar generative probabilistic labelled transition systems, their corresponding discrete-time Markov chains are also bisimilar. Download: pdf (492 KB)

FML-05-01

 [FML-05-01] Cristian Prisacariu, Gabriel Ciobanu. Timed Distributed pi-calculus. pp 49, October, 2005 ISSN 1842 - 1490 Abstract (click to show/hide) Timed distributed pi-calculus extends the distributed pi-calculus of Hennessy and Riely with timers transforming the channels into temporary resources. Distributed pi-calculus describes controlled interactions between processes with restricted access to resources. We allow extra time constraints by considering a notion of timeout for channels. Combining timers with types and locations, timed distributed pi-calculus is a formal framework able to describe complex systems with constraints on time and on resource access. We provide a static semantics given by a typing rules system, and an operational semantics given through a reduction relation. The passage of time is simulated with the help of a time-stepping function. It is proved that the passage of time does not interfere with the typing system. The new defined calculus is proved to be sound by using a method based on subject reduction. The modelling power of the framework introduced in this paper is illustrated by examples; one example is related to molecular networks of the immune system, emphasising also the time coordination problem. Download: pdf (584 KB)