Mathematical models are important tools in systems biology, since the regulatory networks in biological cells are too complicated to understand by biological experiments alone. Analytical solutions can be derived only for the simplest models and numerical simulations are necessary in most cases to evaluate the models and their properties and to compare them with measured data. This thesis focuses on the mesoscopic simulation level, which captures both, space dependent behavior by diffusion and the inherent stochasticity of cellular systems. Space is partitioned into compartments by a mesh and the number of molecules of each species in each compartment gives the state of the system. We first examine how to compute the jump coefficients for a discrete stochastic jump process on unstructured meshes from a first exit time approach guaranteeing the correct speed of diffusion. Furthermore, we analyze different methods leading to non-negative coefficients by backward analysis and derive a new method, minimizing both the error in the diffusion coefficient and in the particle distribution. The second part of this thesis investigates macromolecular crowding effects. A high percentage of the cytosol and membranes of cells are occupied by molecules. This impedes the diffusive motion and also affects the reaction rates. Most algorithms for cell simulations are either derived for a dilute medium or become computationally very expensive when applied to a crowded environment. Therefore, we develop a multiscale approach, which takes the microscopic positions of the molecules into account, while still allowing for efficient stochastic simulations on the mesoscopic level. Finally, we compare on- and off-lattice models on the microscopic level when applied to a crowded environment.

For cell-biological processes, it is the complex interaction of their biochemical components, affected by both stochastic and spatial considerations, that create the overall picture. Formal modeling provides a method to overcome the limits of experimental observation in the wet-lab by moving to the abstract world of the computer. The limits of the abstract world again depend on the expressiveness of the modeling language used to formally describe the system under study. In this thesis, reaction constraints for the pi-calculus are proposed as a language for the stochastic and spatial modeling of cell-biological processes. The goal is to develop a language with sufficient expressive power to model dynamic cell structures, like fusing compartments. To this end, reaction constraints are augmented with two language constructs: priority and a global imperative store, yielding two different modeling languages, including non-deterministic and stochastic semantics. By several modeling examples, e.g. of Euglena's phototaxis, and extensive expressiveness studies, e.g. an encoding of the spatial modeling language BioAmbients, including a prove of its correctness, the usefulness of reaction constraints, priority, and a global imperative store for the modeling of cell-biological processes is shown. Thereby, besides dynamic cell structures, different modeling styles, e.g. individual-based vs. population-based modeling, and different abstraction levels, as e.g. provided by reaction kinetics following the law of Mass action or the Michaelis-Menten theory, are considered.

In this thesis, we study two fundamental problems that arise in the modeling of stochastic systems: (i) Validation of stochastic models against behavioral specifications such as temporal logics, and (ii) Discovery of kinetic parameters of stochastic biochemical models from behavioral specifications. We present a new Bayesian algorithm for Statistical Model Checking of stochastic systems based on a sequential version of Jeffreys’ Bayes Factor test. We argue that the Bayesian approach is more suited for application do- mains like systems biology modeling, where distributions on nuisance parameters and priors may be known. We prove that our Bayesian Statistical Model Checking algorithm terminates for a large subclass of prior probabilities. We also characterize the Type I/II errors associated with our algorithm. We experimentally demonstrate that this algorithm is suitable for the analysis of complex biochemical models like those written in the BioNetGen language. We then argue that i.i.d. sampling based Statistical Model Checking algorithms are not an effective way to study rare behaviors of stochastic models and present another Bayesian Statistical Model Checking algorithm that can incorporate non-i.i.d. sampling strategies. We also present algorithms for synthesis of chemical kinetic parameters of stochastic biochemical models from high level behavioral specifications. We consider the setting where a modeler knows facts that must hold on the stochastic model but is not confident about some of the kinetic parameters in her model. We suggest algorithms for discovering these kinetic parameters from facts stated in appropriate formal probabilistic specification languages. Our algorithms are based on our theoretical results characterizing the probability of a specification being true on a stochastic biochemical model. We have applied this algorithm to discover kinetic parameters for biochemical models with as many as six unknown parameters.