Refine
Document Type
- Doctoral thesis (6)
- Report (3)
Has Fulltext
- yes (9)
Is part of the Bibliography
- no (9)
Keywords
- Petri-Netz (9) (remove)
Institute
MARCIE manual
(2016)
This manual gives an overview on MARCIE – Model Checking And Reachability analysis done effiCIEntly. MARCIE was originally developed as a symbolic model checker for stochastic Petri nets, building on its predecessor – IDDMC – Interval Decision Diagram based Model Checking – which has been previously developed for the qualitative analysis of bounded Place/Transition nets extended by special arcs. Over the last years the tool has been enriched to allow also quantitative analysis of extended stochastic Petri nets. We concentrate here on the user viewpoint. For a detailed introduction to the relevant formalisms, formal definitions and algorithms we refer to related literature.
The work described in this report can be broadly divided into two sections. The first section considers two export features. We describe how the export for stochastic Petri nets to SBML level 1 has been added to the Petri net modelling and simulation tool Snoopy. This task was accomplished by making appropriate changes to the existing export code to generate SBML level 2. Also we demonstrate in detail, how the direct export for coloured Petri nets to both levels (i.e. 1 and 2) of SBML was realised. The next section summarises the performed comparison of different stochastic simulation tools for biochemical reaction networks. We first compare BioNetGen and SSC with each other by performing simulations on non-coloured Petri nets. Then, we compare the remaining four tools, i.e. Cain, Marcie, Snoopy and Stochkit with each other by performing simulation on coloured Petri nets.
This work builds on results by Aman Sinha [19].
This report compares some stochastic simulation tools for biochemical reaction networks. The stochastic simulation tools are selected on the basis of some selection criteria. Simulations are performed for the different stochastic simulation tools on different benchmark models. This report gives an overview of how the comparison is carried out for the chosen tools.
The tools are compared on a common evaluation protocol. The evaluation protocol comprises a set of benchmark models along with the parameters which are provided as input to the tools. The benchmark models are represented as Petri nets and fed in SBML (System Biology Markup Language) to the different tools. Experiments are performed on each tool and the results are recorded. The tools are finally compared based on the comparison criteria.
Computational steering is an interactive remote control of a long running application. The user can adopt it to adjust the simulation parameters on the fly. Correspondingly, simulation of large scale biochemical networks is computationally expensive, particularly stochastic and hybrid simulation. Such extremely intensive computations necessitate an interactive mechanism to permit users to try different paths and ask simultaneously "what-if" questions while the simulation is in progress. Furthermore, with the progress of computational modelling and the simulation of biochemical networks, there is a need to manage multi-scale models, which may contain species or reactions at different scales (called also stiff systems). In this context, Petri nets are of considerable importance in the modelling and analysis of biochemical networks, since they provide an intuitive visual representation of reaction networks. The contributions of this thesis are twofold: firstly, we introduce the definition and present simulation algorithms of Generalised Hybrid Petri Nets (GHPNbio) to represent and simulate stiff biochemical networks where fast reactions are represented and simulated continuously, while slow reactions are carried out stochastically. GHPNbio provide rich modelling and simulation functionalities by combining all features of Continuous Petri Nets (CPN) and Extended Stochastic Petri Nets (XSPN), including three types of deterministic transitions. Moreover, the partitioning of the reaction networks can either be done off-line before the simulation starts or on-line while the simulation is in progress. Secondly, we introduce a novel framework which combines Petri nets and computational steering for the representation and interactive simulation of biochemical networks. The main merits of the framework proposed in this thesis are: the tight coupling of simulation and visualisation, distributed; collaborative; and interactive simulation, and intuitive representation of biochemical networks by means of Petri nets. Generalised hybrid Petri nets and computational steering will together provide an invaluable tool for systems biologists to help them to obtain a deeper system level understanding. GHPNbio speed up the simulation and simultaneously preserve accuracy, while computational steering enables users of different background to share, collaborate and interactively simulate biochemical models. Finally, the implementation of the proposed framework is given as part of Snoopy - a tool to design and animate/simulate hierarchical graphs, among them qualitative, stochastic, continuous and hybrid Petri nets.
Modeling plays a crucial role in Systems Biology in order to provide a system-level understanding of biological systems. With the rapid development of systems biology, modeling of biological systems has shifted from single scales to multiple scales. This introduces a series of challenges that should be addressed, e.g. repetition of components such as genes and cells, variation of components, or hierarchical organization of components. Traditional modeling approaches, e.g. Petri nets, cannot afford to cope with these challenges, which, however, can be tackled using colored Petri nets. This thesis aims to present a technology based on colored Petri nets and associated techniques to address challenges introduced by multiscale modeling in systems biology and to implement them in our modeling tool, Snoopy. To this aim, we present a colored Petri net framework for systems biology, which relates three modeling paradigms: colored qualitative Petri net (QPNC), colored stochastic Petri net (SPNC) and colored continuous Petri net (CPNC). Using this framework, we can model and analyze a biological system from three different perspectives: qualitative, stochastic and continuous by converting them into each other. We implement this framework in our modeling tool, Snoopy, and therefore in this thesis we explore three key problems concerning the implementation of colored Petri nets. For animating/simulating colored Petri nets, we present an efficient algorithm for the computation of enabled transition instances. In order to utilize the analysis techniques of Petri nets we present an efficient unfolding algorithm for large-scale colored Petri nets. In addition, we discuss three special cases for automatic folding (colorizing): colorizing T-invariants, master nets and twin nets in order to reduce the amount of work for folding Petri nets. Petri nets offer a large variety of analysis techniques ranging from informal techniques, e.g. animation/simulation to formal techniques, e.g. model checking. We summarize those analysis techniques that can be used for colored Petri nets, e.g. structural analysis, numerical and simulative model checking from the application point of view. We discuss some scenarios to illustrate the potential capability of colored Petri nets to cope with challenges in systems biology. Moreover, we apply our colored Petri net technology and techniques to three case studies, C. elegans vulval development, coupled Ca2+ channels and membrane systems. These case studies not only demonstrate how to use the colored Petri net framework and related analysis techniques for modeling and analyzing biological systems, but also show how to address the challenges of systems biology.
Nature protection has been a challenge for a long time due to continuous activities that reduced ecological processes and functions of the natural environment. These ecological processes and function provide huge benefits to humans and their communities known as Ecosystem Services (ES). ES are the benefits people derive from natural ecosystems. Many policy measures such as legal and voluntary protections have been used to preserve ES. But continuous increasing threats on the natural environment show that additional policy instruments are needed to achieve targets for environmental protection and sustainability. There are increasing land degradation, desertification, flooding, water shortage, climate change, which is mainly due to the sinks in ES. The problem is that ES are often considered as free goods making it different for their preservation. Even though tax policy for payment for ES has been used to encourage their preservation, they are reducing in supply. This is due to social dilemmas like differences in preferences, free riders and “tragedy of the Common” problems that are usually the case in resource distribution. Therefore tax systems may not lead to substantial preservation of ES. This has been argued on using utility theories and introduced market-base instruments for preserving ES as one way of achieving policy targets for nature protection. But for this Market for Ecosystem Services (MES) to grow, incentive and motivation schemes are needed to encourage multi-actors interaction in them. This has led to the establishment of a Community-based Financial Participation (CFP) framework as incentive and motivation schemes for business development for preserving ES. This thesis uses socio-economic and ecological concepts to argue for MES and developed a business modelling framework with Petri net. This involves multi-actors’ interaction for the demand and supply for ES (multi-agent interaction) that are modelled for estimating their flows over a landscape for supporting policy targets based on market structures. It also modelled future scenario for achieving environmental balancing for preserving ES and provide a management framework for MES. The management scheme comprises of an estimating model for ES, and models for management scheme and CFP. This provides the basis of using Petri net modelling framework for CFP to foster the growth of MES as options for preserving ES. Petri nets modelling techniques is used in simulating multi-agent interaction for the demand and supply of ES that are couple with management and CFP models to form a unified system approach. Petri nets have been used in many disciplines, but this is the first attempt in its use for modelling ES. CFP has also been developed with the framework of the research for this thesis. UNESCO Biosphere Reserve Spreewald (BRSW) in the Lusatian region of south Brandenburg in Germany is taken as an experimental area for testing the concepts and models developed within the thesis research. The results of this thesis show that MES is a potential for achieving targets for preserving ES, which can contribute to nature protection. This has been justified through data sampling, analytical schemes and management support systems that have been provided in the business modelling and simulation framework in this thesis.
The research in this thesis focuses on different techniques which can improve efficiency of the symbolic analysis of Petri nets. Reduced ordered interval decision diagrams (ROIDDs) are employed to encode sets of states of k-bounded nets. We discuss implementation of an ROIDD package and special ROIDD operations needed in symbolic algorithms. We study then how to improve efficiency of the reachability analysis and propose a new saturation approach, which exploits the structure of ROIDDs and the structure of k-bounded P/T nets. It manages to keep sizes of intermediate diagrams smaller than other approaches and can drastically improve efficiency of the symbolic analysis. Saturation techniques are applied in the enumeration of strongly connected components and in model checking. Implementation of symbolic model checkers for k-bounded P/T nets are discussed. We consider CTL and a novel LTL model checker. A number of techniques to improve efficiency of the implementation are considered.
Diese Arbeit widmet sich der Verifikation nebenläufiger Systeme unter Verwendung von Modelcheckingverfahren. Es wurden Modelcheckingverfahren betrachtet und entwickelt, welche die drei Gebiete: Petrinetze als Modellierungssprache, linear-time temporale Logik zur Spezifikation von Systemeigenschaften und binäre Entscheidungsgraphen zur Repräsentation großer Zustandsmengen verbinden. Bei der Entwicklung von Modelcheckingverfahren wurde darauf geachtet, dass durch die Kombination der einzelnen Gebiete deren Vorteile erhalten bleiben und die sich zwischen den Gebieten ergebendnen Synergien ausgenutzt werden. Den wesentlichen innovativen Teil der Arbeit stellt die Entwicklung eines LTL-Modelcheckingverfahrens dar, welches eine symbolische Repräsentierung der Zustände mit einem on-the-fly Verifikationsverfahren verbindet und dabei eine zeitliche Komplexität der klassischen LTL-Modelcheckingverfahren erreicht.
Diese Arbeit behandelt einen Ansatz zur Verifikation verteilter Systeme. Zur Beschreibung des Verhaltens solcher Systeme verwenden wir die sog. Semiwörter, die eine spezielle Form von pomsets darstellen, sowie Mazurkiewiczspuren. Wir weisen nach, daß jedes nebenläufige System (d. h. ein System, für dessen Aktionen eine Unabhängigkeitsrelation angegeben werden kann) als verteiltes System aufgefaßt werden kann. Wir beschreiben eine endliche Repräsentation des Verhaltens nebenläufiger und verteilter Systeme, die auf dem Begriff des Prozeßautomaten beruht, und geben Algorithmen zur Konstruktion derartiger Prozeßautomaten an. Schließlich definieren wir die verteilte, agentenbasierte temporale Logik DCTL. Die Beschreibung eines Modelcheckers für diese Logik, der auf Prozeßautomaten operiert, schließt die Arbeit ab.