Fundamenta Informaticae - Volume 153, issue 1-2

Authors: Aman, Bogdan | Kleijn, Jetty | Koutny, Maciej | Lucanu, Dorel

Article Type: Other

DOI: 10.3233/FI-2017-1528

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. v-vi, 2017

Authors: Alhumaidan, Abdullah | Steggles, Jason

Article Type: Research Article

Abstract: Qualitative logical modelling techniques play an important role in biology and are seen as crucial for developing scalable methods for modelling and synthesizing biological systems. While a range of interesting work has been done in this area there still exists challenging issues that need to be addressed for the practical application of these modelling techniques. In this paper we present an algebraic framework for exploring these issues by developing techniques for modelling and analysing qualitative biological models using Rewriting Logic (RL) . The aim here is to develop a universal formal framework which is able to integrate models expressed in …different formalisms (e.g. Boolean networks, Petri Nets and process algebra) and provide a basis for new work in this area (e.g. merging models based on different formalisms; compositional model construction and analysis; and tools for synthetic biology). We take as our starting point Multi-valued networks (MVNs) , a simple yet expressive qualitative state based modelling approach widely used in biology. We develop a semantic translation from MVNs to a corresponding RL model and formally show that this translation is correct. We consider both the asynchronous and synchronous update semantics, and investigate the use of rewriting strategies to enable synchronisation to be modelled. We illustrate the RL framework developed and the potential RL analysis possible by presenting two detailed case studies. Show more

Keywords: rewriting logic, qualitative modelling, genetic regulatory networks, multi-valued networks

DOI: 10.3233/FI-2017-1529

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 1-28, 2017

Authors: Bergstra, J.A. | Middelburg, C.A.

Article Type: Research Article

Abstract: In a previous paper, an ACP-style process algebra was proposed in which propositions are used as the visible part of the state of processes and as state conditions under which processes may proceed. This process algebra, called ACPps, is built on classical propositional logic. In this paper, we present a version of ACPps built on a paraconsistent propositional logic which is essentially the same as CLuNs. There are many systems that would have to deal with self-contradictory states if no special measures were taken. For a number of these systems, it is conceivable that accepting self-contradictory states and dealing with …them in a way based on a paraconsistent logic is an alternative to taking special measures. The presented version of ACPps can be suited for the description and analysis of systems that deal with self-contradictory states in a way based on the above-mentioned paraconsistent logic. Show more

Keywords: process algebra, propositional signal, propositional condition, paraconsistent logic

DOI: 10.3233/FI-2017-1530

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 29-55, 2017

Authors: Horne, Ross | Mauw, Sjouke | Tiu, Alwen

Article Type: Research Article

Abstract: Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal …attack trees . Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV, featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains. Show more

Keywords: attack trees, semantics, causality, linear logic, calculus of structures

DOI: 10.3233/FI-2017-1531

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 57-86, 2017

Authors: Păun, Andrei | Rodríguez-Patón, Alfonso

Article Type: Research Article

Abstract: We refine the modeling in the P systems area of the way bacteria transmit genetic information in bacterial colonies, specifically the conjugation process. We study this new model from the computational power perspective using methods and ideas in the area; we are able to prove the universality of these systems. We show that systems working in a homogeneous manner and using only 75 species of objects in the regions and 13 species of “on-membrane” objects are enough for reaching universality. The system starts in a initial state with only few (nine) bacteria needed and the “bacteria” from this system are …homogeneous, all have the same rules. Show more

Keywords: P systems, Bacterial conjugation, universality, small universal machines

DOI: 10.3233/FI-2017-1532

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 87-103, 2017

Authors: Stoenescu, Teodor | Stefanescu, Alin | Predut, Sorina | Ipate, Florentin

Article Type: Research Article

Abstract: We present a binary analysis framework based on symbolic execution with the distinguishing capability to execute stepwise forward and also backward through the execution tree. It was developed internally at Bitdefender and code-named RIVER. The framework provides components such as a taint engine, a dynamic symbolic execution engine, and integration with Z3 for constraint solving. In this paper we will provide details on the framework and give an example of analysis on binary code.

DOI: 10.3233/FI-2017-1533

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 105-124, 2017

Authors: Todoran, Eneia Nicolae | Papaspyrou, Nikolaos

Article Type: Research Article

Abstract: We present a denotational semantics designed in continuation-passing style (CPS) for an abstract language providing operators for nondeterministic choice, sequential and parallel composition, and a general mechanism of interaction between multisets of distributed actions. We show that the basic laws of concurrent systems are satisfied in this semantics. Next, by customizing the behavior of continuations we obtain denotational semantics for a couple of concurrent languages and a nature-inspired formalism. The languages discussed include Hoare’s communicating sequential processes (CSP), and two formalisms based on multiparty interactions: a version of CSP extended with communication and synchronization on multiple channels, and a language …similar to a process algebra for DNA computing introduced by Cardelli. We accomplish the semantic investigation in the mathematical framework of complete metric spaces. Show more

Keywords: continuation-passing style, denotational semantics, metric spaces, concurrency semantics

DOI: 10.3233/FI-2017-1534

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 125-146, 2017

Authors: Valencia-Cabrera, Luis | Orellana-Martín, David | Martínez-del-Amor, Miguel A. | Riscos-Núñez, Agustín | Pérez-Jiménez, Mario J.

Article Type: Research Article

Abstract: Polarizationless P systems with active membranes are non-cooperative systems, that is, the left-hand side of their rules have a single object. Usually, these systems make use of division rules as a mechanism to produce an exponential workspace in linear time. Division rules are inspired by cell division, a process of nuclear division that occurs when a parent cell divides to produce two identical daughter cells. On the other hand, separation rules are inspired by the membrane fission process, a mechanism by which a biological membrane is split into two new ones in such a manner that the contents of the …initial membrane is distributed between the new membranes. In this paper, separation rules are used instead of division rules. The computational efficiency of these models is studied and the role of the (minimal) cooperation in object evolution rules is explored from a computational complexity point of view. Show more

Keywords: Membrane Fission, Membrane Computing, Active membranes, Separation rules, Complexity classes, SAT problem

DOI: 10.3233/FI-2017-1535

Citation: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 147-172, 2017