1,721,034 research outputs found
Space, Geometry, Motion and Interactions in Modeling Biological Systems: the BioShape Approach
No full textWe present BioShape, a modeling and simulation environment for
biological systems at different scales. The basic assumption is that
the system is modeled using autonomous entities that have a physical shape, move in a geometrical 3D space and can interact in different ways. The modeled biological phenomenon will be observed and analyzed as the emerging behavior of the entities' behaviors in the in-silico experiment (simulation) that is set up. We show several application areas of our approach at different levels: molecular, cellular and tissue. Moreover, we show that different levels can be specified uniformly within BioShape, making it a powerful multiscale environment
Timed automata with urgent transitions
No full textIn this paper we propose an extension to the formalism of timed automata by allowing urgent transitions. An urgent transition is a transition which must be taken within a fixed time interval from its enabling time and it has higher priority than other non-urgent transitions enabled in the same state. We give a set of rules formally describing the behavior of urgent transitions and we show that, from a language theoretic point of view, the addition of urgency does not improve the expressive power of timed automata. From a specification point of view, the use of urgent transitions allows shorter and clear specifications of behaviors involving urgency and priority. We use timed automata with urgent transitions for specifying a multicast protocol for mobile computing
A Decidable Notion of Timed Non-Interference
No full textWe 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
A formal language for classifying RNA secondary structures
Full text linkWe introduce a formal language for representing RNA secondary structures as interactions of loops towards a topological shape language. A base loop is an hairpin. All the other loops, such as bulge, helix, inner loop and multiple loop, are compositions of hairpins. Two loops are sequentially connected by base pair weak interactions. We introduce a set of operators to manipulate loops and interactions between loops. The grammar of the resulting language of RNA secondary structure allows us to generate both pseudoknot free and pseudoknotted RNA secondary structures starting from the RNA sequences. Moreover, we can represent a pseudoknot free RNA secondary structure in a “canonical form”, thus we have a way to tell whether two given structures differ by a loop. We will investigate the characterization of the higher order language corresponding to the loops interactions
An algebraic representation for tree alignment of RNA pseudoknotted structures.
Full text linkThe methods proposed in the literature for RNA comparison focus mainly on pseudoknot free structures. The comparison of pseudoknotted structures is still a challenge. In this work, we propose a new algebraic representation of RNA secondary structures based on relations among hairpins in terms of nesting, crossing, and concatenation. Such algebraic representation is obtained from a defined multiple context-free grammar, which maps any kind of RNA secondary structures into extended trees, i.e., ordered trees where internal nodes are labeled with algebraic operators and leaves are labeled with loops. These extended trees permit the definition of the RNA secondary structure comparison as a tree alignment problem
Reversible Graph Grammar for RNA
Full text linkGraph rewriting formalism is widely used for modelling the dynamics of complex systems in direct and intuitive way. It has been used in computational biology in different contexts, such as RNA tertiary structure motifs encoding and biochemical systems modelling. Besides, in our previous work, we have shown how double pushout (DPO) graph rewriting is used to model the RNA folding as a self adaptive system within S[B] paradigm. Accordingly, the graph transformation encodes simultaneously the RNA functional behaviour and its structure.
DPO rewriting rules are applicable whenever the application conditions (identification conditions and dangling conditions) and negative applications conditions are satisfied. The specified conditions can also be used to ensure the reversibility characteristics of DPO. The reversibility of DPO rule has been applied to model dining philosophers problem. Since DPO rules are guaranteed to be reversible (backtrack), we can perform the admissible rewriting rules to model the folding and unfolding pathways of RNA. The backtracking mechanism backtracks out of the dead-ends by undoing all effects of graph rewriting sequences and by selecting the remaining possible rewritings to derive all the possible RNA secondary structures.
In this study, as extension of our previous work, we introduce reversible graph grammar to formalize and complete the definition of the B and S levels of the S[B]. The B-level is represented as a label transition system (LTS) in which the sate space represents the entire folding evolution of the given RNA molecule. The structural level S, represented as a state machine which controls the adaptation dynamics of the B level towards the lowest minimum free energy secondary structure based on state and transition constraints
Adaptability Checking in Multi-Level Complex Systems
No full textA hierarchical model for multi-level adaptive systems is built on two basic levels: a lower behavioural level B accounting for the actual behaviour of the system and an upper structural level S describing the adaptation dynamics of the system. The behavioural level is modelled as a state machine and the structural level as a higher-order system whose states have associated logical formulas (constraints) over observables of the behavioural level. S is used to capture the global and stable features of B, by a defining set of allowed behaviours. The adaptation semantics is such that the upper S level imposes constraints on the lower B level, which has to adapt whenever it no longer can satisfy them. In this context, we introduce weak and strong adaptabil- ity, i.e. the ability of a system to adapt for some evolution paths or for all possible evolutions, respectively. We provide a relational characterisation for these two notions and we show that adaptability checking, i.e. deciding if a system is weak or strong adaptable, can be reduced to a CTL model checking problem. We apply the model and the theoretical results to the case study of motion control of autonomous transport vehicles
Abstract Interpretation Against Races
No full textIn this paper we investigate the use of abstract interpretation techniques for statically preventing race conditions. To this purpose we enrich the concurrent object calculus conc 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
Timed Automata with non-Instantaneous Actions
No full textIn 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, that is an action can take some time to be completed. Thus, for an action , there are two particular time
instants, the initiation of the action and the completion of the action, which may occur at different times. 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 edges. Moreover we define the parallel composition of timed automata with non-instantaneous actions. We show how real systems can be suitably modeled by them, in particular we specify a system which was specified in Alur and Dill (1994) by timed automata. We point out how the specification by means of a parallel timed automata with non-instantaneous actions is, in some cases, more convenient to represent reality
An Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier
No full textThe Java Virtual Machine embodies a verifier that performs a set of checks on Java bytecode programs before their execution. The verifier carries out an efficient data-flow analysis applied to a type-level abstract interpretation of the code. The implementations of the bytecode verifier presented a significant problem with programs compiled with the Sun Java compiler (until version 1.4.1): there were legal Java programs which were correctly compiled into a bytecode that was rejected by the verifier. The problem was fixed by removing, in version
1.4.2 and following, some interesting features in the compilation of the try-finally Java construct. Because removing such features has a cost in terms of memory space, in this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the space efficiency of the previous versions of the compiler. We define an abstract interpretation framework in which we model the enhanced version of the verifier. The defined abstract interpretation framework can be considered a good basis for other static analyses of bytecode programs
- …
