Living cells are constantly subjected to a plethora of environmental stimuli that require integration into an appropriate cellular response. This integration takes place through signal transduction events that form tightly interconnected networks. The understanding of these networks requires capturing their dynamics through computational support and models. ANIMO (analysis of Networks with Interactive Modeling) is a tool that enables the construction and exploration of executable models of biological networks, helping to derive hypotheses and to plan wet-lab experiments. The tool is based on the formalism of Timed Automata, which can be analyzed via the UPPAAL model checker. Thanks to Timed Automata, we can provide a formal semantics for the domain-specific language used to represent signaling networks. This enforces precision and uniformity in the definition of signaling pathways, contributing to the integration of isolated signaling events into complex network models. We propose an approach to discretization of reaction kinetics that allows us to efficiently use UPPAAL as the computational engine to explore the dynamic behavior of the network of interest. A user-friendly interface hides the use of Timed Automata from the user, while keeping the expressive power intact. Abstraction to single-parameter kinetics speeds up construction of models that remain faithful enough to provide meaningful insight. The resulting dynamic behavior of the network components is displayed graphically, allowing for an intuitive and interactive modeling experience.

When analysing complex interaction networks occurring in biological cells, a biologist needs computational support in order to understand the effects of signalling molecules (e.g. growth factors, drugs). ANIMO (Analysis of Networks with Interactive MOdelling) is a tool that allows the user to create and explore executable models of biological networks, helping to derive hypotheses and to plan wet-lab experiments. The tool is based on the formalism of Timed Automata, which can be analysed via the UPPAAL model checker. Thanks to Timed Automata, we can provide a formal semantics for the domain-specific language used to represent signalling networks. This enforces precision and uniformity in the definition of signalling pathways, contributing to the integration of signalling event models into complex, crosstalk-driven networks. We propose an approach to discretization of reaction kinetics that allows us to efficiently use UPPAAL as the computational engine to explore the dynamic cell behaviour. A user friendly interface makes the use of Timed Automata completely transparent to the biologist, while keeping the expressive power intact. This allows to define relatively simple, yet faithful models of complex biological interactions. The resulting timed behaviour is displayed graphically, allowing for an intuitive and interactive modelling experience.

This paper discusses stochastic extensions of a simple process algebra in a causality-based setting. Atomic actions are supposed to happen after a delay that is determined by a stochastic variable with a certain distribution. A simple stochastic type of event structures is discussed, restricting the distribution functions to be exponential. A corresponding operational semantics of this model is given and compared to existing (interleaved) approaches. Secondly, a stochastic variant of event structures is discussed where distributions are of a much more general nature, viz. of phase-type. This includes exponential, Erlang, Coxian and mixtures of exponential distributions.

A view on a database is a mapping that provides a user or application with a suitable way of looking at the data. Updates specified on a view have to be translated into updates on the underlying database. We study the view update translation problem for a relational data model in which the base relations may contain (indexed) nulls. The representative instance is considered to be the correct representation of all data in the database; the class of views that is studied consists of total projections of the representative instance. Only independent database schemes are considered, that is, schemes for which global consistency is implied by local consistency. A view update can be an insertion, a deletion, or a modification of a single view tuple. It is proven that the constant complement method of Bancilhon and Spyratos is too restrictive to be useful in this context. Structural properties of extension joins are derived that are important for understanding views. On the basis of these properties, minimal algorithms for translating a single view-tuple update are given.