Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 14

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Specialized Predictor for Reaction Systems with Context Properties
EN
Reaction systems are a qualitative formalism for modeling systems of biochemical reactions characterized by the non-permanency of the elements: molecules disappear if not produced by any enabled reaction. Reaction systems execute in an environment that provides new molecules at each step. Brijder, Ehrenfeucht and Rozemberg introduced the idea of predictors. A predictor of a molecule s, for a given n, is the set of molecules to be observed in the environment to determine whether s is produced or not at step n by the system. We introduced the notion of formula based predictor, that is a propositional logic formula that precisely characterizes environments that lead to the production of s after n steps. In this paper we revise the notion of formula based predictor by defining a specialized version that assumes the environment to provide molecules according to what expressed by a temporal logic formula. As an application, we use specialized formula based predictors to give theoretical grounds to previously obtained results on a model of gene regulation.
2
Content available remote Maximally Parallel Probabilistic Semantics for Multiset Rewriting
EN
Maximally parallel semantics have been proposed for many formalisms as an alternative to the standard interleaving semantics for some modelling scenarios. Nevertheless, in the probabilistic setting an affirmed interpretation of maximal parallelism still lacks. We define a synchronous maximally parallel probabilistic semantics for multiset rewriting tailored to describe, simulate and verify biological systems evolving with maximally parallel steps. Each step of the proposed semantics is parallel as each reaction can happen multiple times, and it is maximal as it leaves no enabled reaction i.e. as many reactions as possible are executed. We define a maximally parallel probabilistic semantics in terms of Discrete Time Markov Chain for systems described by stochastic multiset rewriting. We propose a simple, maximally parallel, model of Caenorhabditis elegans vulval development on which we show probabilistic simulations results.
EN
A formal model for diagnostics of biological systems modelled as P systems is presented. We assume the presence of some biologically motivated changes (frequently pathological) in the systems behavior and investigate when these changes could be diagnosed by an external observer by exploiting some techniques originally developed for reasoning on system security.
EN
The Calculus of Looping Sequences is a formalism for describing evolution of biological systems by means of term rewriting rules. We propose to enrich this calculus by labelling elements of sequences. Since two elements with the same label are considered to be linked, this allows us to represent protein interaction at the domain level. Well-formedness of terms are ensured by both a syntactic constraint and a type system: we discuss the differences between these approaches through the description of a biological system, namely the EGF pathway.
5
Content available remote Timed P Automata
EN
To study systems whose dynamics changes with time, an extension of timed P systems is introduced in which evolution rules may vary with time. The proposed model is a timed automaton with a discrete time domain and in which each state is a timed P system. A result on expressive power and on features of the formalism sufficient for full expressiveness is proved and, as an application example, the model of an ecological system is given.
6
Content available remote P Systems with Transport and Diffusion Membrane Channels
EN
P Systems are computing devices inspired by the structure and the functioning of a living cell. A P System consists of a hierarchy of membranes, each of them containing a multiset of objects, a set of evolution rules, and possibly other membranes. Evolution rules are applied to the objects of the same membrane with maximal parallelism. In this paper we present an extension of P Systems, called P Systems with Membrane Channels (PMC Systems), in which membranes are enriched with channels and objects can pass through a membrane only if there are channels on the membrane that enable such a passage. We show that PMC Systems are universal even if only the simplest form of evolution rules is considered, and we give two application examples.
7
Content available remote A P Systems Flat Form Preserving Step-by-step Behaviour
EN
Starting from a compositional operational semantics of transition P Systems we have previously defined, we face the problem of developing an axiomatization that is sound and complete with respect to some behavioural equivalence. To achieve this goal, we propose to transform the systems into a normal form with an equivalent semantics. As a first step, we introduce axioms which allow the transformation of membrane structures into flat membranes. We leave as future work the further step that leads to the wanted normal form.
8
Content available remote A Calculus of Looping Sequences for Modelling Microbiological Systems
EN
The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent elements and operators of sequencing, looping, containment and parallel composition. The looping operator allows tying up the ends of a sequence, thus creating a circular sequence which can represent a membrane. We show that a membrane calculus recently proposed can be encoded into CLS. We use our calculus to model interactions among bacteria and bacteriophage viruses, and to reason on their properties.
9
Content available remote Abstract Interpretation of an Object Calculus for Synchronization Optimizations
EN
In this paper we present a use of abstract interpretation techniques for reducing synchronization overhead in an object calculus. First we present the new raconcV calculus, an extension of an already existing calculus for supporting reentrant locks. Then we use an abstract form of this calculus to check when synchronization operations may be safely eliminated from statements. Thus our approach may be used to improve performance in object oriented languages by eliminating locks, without the risks caused by "manual" optimizations performed by programmers.
10
Content available remote A Probabilistic Model for Molecular Systems
EN
We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a probabilistic transition system can be derived from it. We use the algorithm in the development of an interpreter for the model, which we use to simulate the evolution of molecular systems. In particular, we show the results of the simulation of a real example of enzymatic activity. Moreover, we apply the probabilistic model checker PRISM to the transition system derived by the model of this example, and we show the results of model checking of some illustrative properties.
11
Content available remote Abstract Interpretation against Races
EN
In this paper we investigate the use of abstract interpretation techniques for statically preventing race conditions. To this purpose we enrich the concurrent object calculus concV by annotating terms with the set of ``locks'' owned at any time. We use an abstract form of the object calculus to check the absence of race conditions. We show that abstract interpretation is more flexible than type analyses, and it allows to certify as ``race free'' a larger class of programs.
12
Content available remote A Decidable Notion of Timed Non-Interference
EN
We present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against attacks.
13
Content available remote A Notion of Non-Interference for Timed Automata
EN
The non-interference property of concurrent systems is a security property concerning the flow of information among different levels of security of the system. In this paper we introduce a notion of timed non-interference for real-time systems specified by timed automata. The notion is presented using an automata based approach and then it is characterized also by operations and equivalence between timed languages. The definition is applied to an example of a time-critical system modeling a simplified control of an airplane.
14
Content available remote Timed Automata with non-Instantaneous Actions
EN
In this paper we propose a model, timed automata with non-instantaneous actions, which allows representing in a suitable way real-time systems. Timed automata with non-instantaneous actions extend the timed automata model by dropping the assumption that actions are instantaneous: in our model an action can take some time to be completed. We investigate the expressiveness of the new model, comparing it with classical timed automata. In particular, we study the set of timed languages which can be accepted by timed automata with non-instantaneous actions. We prove that timed automata with non-instantaneous actions are more expressive than timed automata and less expressive than timed automata with e edges. Moreover we define the parallel composition of timed automata with non-instantaneous actions. We point out how the specification by means of a parallel timed automaton with non-instantaneous actions is, in some cases, more convenient to represent reality.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.