Refine
Document Type
- Report (2)
- Doctoral thesis (1)
Has Fulltext
- yes (3)
Is part of the Bibliography
- no (3)
Language
- English (3)
Keywords
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.
Hybrid simulation of biological processes becomes widely used to overcome the limitations of the pure stochastic or the complete deterministic simulation. In this manual, we present easy-to-follow steps for constructing and executing hybrid models via Snoopy [HHL+12]. Snoopy is a tool to design and animate or simulate hierarchical graphs, i.e., qualitative, stochastic, continuous, and hybrid Petri nets. This manual is concerned with hybrid Petri nets (HPN) [HH12] as well as their coloured counterpart (HPNC) [HLR14]. HPN combine the merits of stochastic and continuous Petri nets into one single class. Moreover, HPN in Snoopy supports state of the art hybrid simulation algorithms (e.g., [HH16]) to execute the constructed HPN models. Simulating a model using Snoopy's hybrid simulation involves first constructing the reaction network via HPN notations and afterwards executing such model.
Stochastic modelling of biochemical reaction networks is getting more and more popular. Throughout the past decades typical biological models increased in their size and complexity, because of advances in systems and molecular biology, in particular through the high-throughput omic technologies. Here biochemical networks of different levels of detail are modelled, starting with simple chemical reactions and signal transduction networks, up to individual cells and entire organisms. This increases the demand for efficient analysis methods.
A Petri net is a mathematical modelling language for the description of concurrent behaviour of distributed systems. Its advantage is the ease of scalability of the models, which relates to the network’s state space, as well as the structure of the network itself.
In this work, we recall several stochastic simulation algorithms, e.g., exact as well as approximate methods. Furthermore, we introduce an approach to improve the efficiency of stochastic simulation for large and dense networks by a new approximate stochastic simulation algorithm called discrete-time leap method. We depict the wide range of simulative analyses of complex stochastic systems ranging from trace generation to the computation of transient solutions and steady state distributions. We set forth advanced analysis of stochastic models by means of simulative model checking. For the use of simulative model checking, we integrate the continuous stochastic (reward) logic (CS(R)L) and the probabilistic linear-time temporal logic with constraints (PLTLc). Simulative model checking has some limitations compared to the numerical methods, e.g., in principle it is possible to consider nested probabilistic formulas in CS(R)L, but not practical, since the calculation is not feasible in a reasonable period of time. In addition to the transient analysis, the steady state analysis is often of interest; therefore we have implemented two on-the-fly steady state detection methods. The first one is based on a “sample batch means” algorithm and is used in the linear-time temporal logic. The second approximates the steady state distribution and checks for convergence. We apply the aforementioned techniques to several case studies from systems biology and technical systems.
The main contributions of this thesis to scientific knowledge are the development of the discrete-time leap method for the simulation of stochastic models, the approximations of transient solutions and steady state distributions by use of stochastic simulation for stochastic models and Markov reward models, the development of an infinite time horizon model checking algorithm exploiting the steady state property for PLTLc and CSL, and the first simulative model checking algorithm for CSRL incorporating state and impulse rewards. All presented algorithms and methods are implemented in the advanced analysis tool MARCIE.