abstract: We give a description of a Petri net-based
framework for modelling and analysing biochemical pathways, which
unifies the qualitative, stochastic and continuous worlds. Each
perspective adds its contribution to the understanding of the system,
thus the three approaches do not compete, but complement each other. We
illustrate our approach by applying it to an extended model of the
three stage cascade, which forms the core of the ERK signal
transduction pathway. Consequently our focus is on transient behaviour
analysis. We demonstrate how qualitative descriptions are abstractions
over stochastic or continuous descriptions, and show that the
stochastic and continuous models approximate each other. A key
contribution of the paper consists in a precise definition of
biochemically interpreted stochastic Petri nets. Although our framework
is based on Petri nets, it can be applied more widely to other
formalisms which are used to model and analyse biochemical networks.
This Technical Report represents an extended version of [GHL07] and
replaces [Leh06].
abstract: We report on the results of an investigation into the application of three Petri net approaches for the modelling and analysis of biochemical networks: discrete, continuous and stochastic Petri nets. We mimic the modelling and analysis steps, which have been proposed in [1] for an extended ERK pathway model. We can confirm that analyses based on a discrete Petri net model of the system can be used to derive the sets of initial concentrations required by the corresponding continuous ordinary differential equation model which is equivalent to a continuous Petri net, and no other initial concentrations produce meaningful steady states. Furthermore, we show how a stochastic Petri net model with discrete levels for the concentration of a species can be applied to perform probabilistic model checking, as proposed in [2].
abstract: We report on the results of an investigation into the integration of Petri nets and ordinary differential equations (ODEs) for the modelling and analysis of biochemical networks, and the application of our approach to the model of the influence of the Raf Kinase Inhibitor Protein (RKIP) on the Extracellular signal Regulated Kinase (ERK) signalling pathway. We show that analysis based on a discrete Petri net model of the system can be used to derive the sets of initial concentrations required by the corresponding continuous ordinary differential equation model, and no other initial concentrations produce meaningful steady states. Altogether, this paper represents a tutorial in step-wise modelling and analysis of larger models as well as in structured design of ODEs.
abstract: Model checking is a fully automated approach to formal verification. The main problem of model checking is the state explosion. A number of techniques has been introduced to deal with the problem. Considering Petri Nets, the most efforts have been done on analysis of safe (1-bounded) place/transition nets. Many tools successfully implementing different techniques are available, but there are too few tools supporting efficient analysis of bounded, but not 1-bounded P/T Nets. This paper is a report on the implementation of a symbolic CTL model checker for bounded P/T nets that is based on Interval Decision Diagrams. The implementation supports inhibitor arcs as well as state space construction for a set of initial markings.
Runge, T.:abstract: Computer aided analysis
possibilities are necessary to improve the understanding of the complex
biochemical processes of a cell. The results of kinetic models are
often non-reliable on account of the lack of reliable data. Therefore,
other supplementary methods are indispensable. To increase the
understanding of biochemical systems, a qualitative analysis method —
especially a qualitative path analysis method — is introduced and
applied to a case study. The applicability of low-level Petri nets for
a qualitative analysis has been shown earlier. In this paper, a new
complex hierarchical model of the glycolysis pathway and their
interacting pathways is presented and analysed. The model is a generic
one because it integrates the different pathways of various cell types
into one unified view. At the end of this paper a meta-model
illustrates the analysed invariants/ pathways.
keywords: metabolic pathway, metabolic
Petri net, P-invariant, T-invariant, glycolysis pathway
abstract: This bibliography provides 74 entries in biochemistry, 1 entry for chemistry, 58 entries for medicine, and 14 entries for ecology and environment.
abstract: Partial order semantics of Petri nets have a long history. In this paper, we describe a formalism which combines partial order semantics with the usual notion of markings of a Petri net. We call this formalism concurrent automata. We discuss improvements of the generation algorithm for concurrent automata and present experimental data concerning the effort of our algorithm.
keywords: Concurrent automata; Petri nets; Partial order semantics; Semiwords; Semi languages; Algorithms
abstract: Partial order semantics of Petri nets have a long history. In this paper, we describe a formalism which combines partial order semantics with the usual notion of markings of a Petri net. We call this formalism concurrent automata. We present a generation algorithm for concurrent automata. We show that our algorithm is correct in the sense of semi language equivalence: The generated automaton recognizes essentially the same set of semiwords as the associated Petri net.
keywords: Concurrent automata; Petri nets; Partial order semantics; Semiwords; Semi languages; Least sequential semi languages; Minimal concurrent automata.
abstract: In diesem Bericht wird gezeigt, wie eine Anweisungsliste (AWL) in ein Petri-Netz überführt werden kann, um in diesem dann gewisse Sicherheits- und Fortschrittseigenschaften zu überprüfen. Basissprache der Überführung ist die AWL. Es wird eine Untermenge von AWL gebildet namens AWL0. Zu dieser Untermenge geben wir eine formale Semantik an. Diese formale Semantik erlaubt es, die Überführung in Petri-Netze besser und einfacher darzustellen.
keywords:SPS-Programmierung, Pwtri-Netze, Zertifizierung von SPS-Programmen, Anweisungsliste.
Heiner, M.; Meier, M; Menzel, T.; Mertke, T.:abstract: In diesem Bericht wird gezeigt, wie eine bereits vorhandene Anweisungsliste (AWL) in ein Petri-Netz überführt werden kann, um in diesem dann gewisse Sicherheits- und Fortschrittseigenschaften zu überprüfen. Die Beschreibung dieser Eigenschaften wird mit Hilfe von Formeln der temporalen Logik vorgenommen.
keywords:SPS-Programmierung, Pwtri-Netze, Zertifizierung von SPS-Programmen, Anweisungsliste.
Heiner, M.; Popova-Zeugmann, L.:abstract:This paper deals with computing the minimal and maximal execution durations in a given concurrent system in order to support software dependability engineering by assuring the meeting of prescribed deadlines. For that purpose, a new kind of time-dependent Petri nets - the Duration Interval Petri net - is introduced, and a dedicated reachability graph is defined in a discrete way. Using this reach ability graph, shortest and largest time paths between two arbitrary states of the concurrent system, and by this way minimal and maximal software execution times, can be computed. These results have been applied to a medium-sized reactive system.
keywords:system validation, qualitative and quantitative analysis, performance evaluation, worst-case analysis, time-dependent Petri nets, control systems.
abstract: The development of provably error-free concurrent systems is still a challenge of system engineering. Modelling and analysis of concurrent systems by means of Petri nets is one of the well- known approaches using formal methods. To evaluate the reached practicability degree of available methods and tools to at least medium-sized systems, we demonstrate the Petri net based step-wise development and validation of the control software of a reactive system. The validation of qualitative properties comprises two steps. At first, the context checking of general semantic properties is done by a suitable combination of static and dynamic analysis techniques, mainly of "classical" Petri net theory. Afterwards, the verification of well-defined special semantic properties, especially safety properties, given by a separate specification of the required functionality is performed by model checking. Strong emphasis has been laid on automation of the analyses to be done. This case study has been already investigated by a lot of different formal methods. This paper provides the possibility to take into account also a strongly Petri net-oriented approach to compare advantages and drawbacks inherent to different formal methods.
keywords: Parallel software/system engineering, validation, static analysis, formal methods, Petri nets, temporal logics, control software, production cell.
abstract: Starting from a classification of software validation techniques an innovative Petri net based methodology is proposed to integrate qualitative and quantitative analysis methods of parallel software systems. The approach combines qualitative analysis, monitoring and testing as well as quantitative analysis on the basis of a net-based intermediate representation of the parallel software system under consideration. The validation of qualitative properties comprises two steps. At first, the context checking of general semantic properties is done by a suitable combination of static and dynamic analysis techniques of Petri net theory. Afterwards, the verification of well-defined special semantic properties given by a separate specification of the required functionality is performed. The validation of quantitative properties is based on so-called locally Markovian Object Nets (MONs) which are obtained from the qualitative models by property-preserving structural compression and quantitative expansion. Here, the frequency and delay attributes necessary to generate quantitative models (i.e. the MONs) are provided by the monitoring and testing component. Besides the provision of the quantitative attributes according to the user-driven time abstraction level, the net-based testing method supports a systematic test of parallel systems. Techniques to derive automati cally dedicated test suites and to measure the test coverage obtained are important features of this systematic testing. The basic ideas are highlighted by a small running example.
keywords:Parallel software engineering, process-oriented
imperative languages, software validation, static analysis, testing and
monitoring, performance evaluation, dependability, formal methods,
Petri nets.
