@book{
 title = {Preface},
 type = {book},
 year = {2020},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {12314 LNBI},
 id = {2adfb6ad-cd93-361f-81fc-d68955834e54},
 created = {2020-10-26T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-10-27T18:41:31.876Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 bibtype = {book},
 author = {Abate, A. and Petrov, T. and Wolf, V.}
}

@article{
 title = {Efficient simulation of non-Markovian dynamics on complex networks},
 type = {article},
 year = {2020},
 volume = {15},
 id = {0908acfb-b414-300e-8760-736b24a8af5a},
 created = {2020-11-08T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-13T04:47:42.169Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We study continuous-time multi-agent models, where agents interact according to a network topology. At any point in time, each agent occupies a specific local node state. Agents change their state at random through interactions with neighboring agents. The time until a transition happens can follow an arbitrary probability density. Stochastic (Monte-Carlo) simulations are often the preferred-sometimes the only feasible-approach to study the complex emerging dynamical patterns of such systems. However, each simulation run comes with high computational costs mostly due to updating the instantaneous rates of interconnected agents after each transition. This work proposes a stochastic rejection-based, event-driven simulation algorithm that scales extremely well with the size and connectivity of the underlying contact network and produces statistically correct samples. We demonstrate the effectiveness of our method on different information spreading models.},
 bibtype = {article},
 author = {Großmann, G. and Bortolussi, L. and Wolf, V.},
 doi = {10.1371/journal.pone.0241394},
 journal = {PloS one},
 number = {10}
}

We study continuous-time multi-agent models, where agents interact according to a network topology. At any point in time, each agent occupies a specific local node state. Agents change their state at random through interactions with neighboring agents. The time until a transition happens can follow an arbitrary probability density. Stochastic (Monte-Carlo) simulations are often the preferred-sometimes the only feasible-approach to study the complex emerging dynamical patterns of such systems. However, each simulation run comes with high computational costs mostly due to updating the instantaneous rates of interconnected agents after each transition. This work proposes a stochastic rejection-based, event-driven simulation algorithm that scales extremely well with the size and connectivity of the underlying contact network and produces statistically correct samples. We demonstrate the effectiveness of our method on different information spreading models.

@book{
 title = {Rejection-Based Simulation of Non-Markovian Agents on Complex Networks},
 type = {book},
 year = {2020},
 source = {Studies in Computational Intelligence},
 keywords = {Complex networks,Epidemic modeling,Gillespie simulation,Multi-agent system,Rejection sampling},
 volume = {881 SCI},
 id = {e6c681d6-a3e0-3c1a-8c93-e4cc66bc3901},
 created = {2019-12-28T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2021-03-01T07:15:22.726Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {true},
 abstract = {© 2020, Springer Nature Switzerland AG. Stochastic models in which agents interact with their neighborhood according to a network topology are a powerful modeling framework to study the emergence of complex dynamic patterns in real-world systems. Stochastic simulations are often the preferred—sometimes the only feasible—way to investigate such systems. Previous research focused primarily on Markovian models where the random time until an interaction happens follows an exponential distribution. In this work, we study a general framework to model systems where each agent is in one of several states. Agents can change their state at random, influenced by their complete neighborhood, while the time to the next event can follow an arbitrary probability distribution. Classically, these simulations are hindered by high computational costs of updating the rates of interconnected agents and sampling the random residence times from arbitrary distributions. We propose a rejection-based, event-driven simulation algorithm to overcome these limitations. Our method over-approximates the instantaneous rates corresponding to inter-event times while rejection events counter-balance these over-approximations. We demonstrate the effectiveness of our approach on models of epidemic and information spreading.},
 bibtype = {book},
 author = {Großmann, G. and Bortolussi, L. and Wolf, V.},
 doi = {10.1007/978-3-030-36687-2_29}
}

© 2020, Springer Nature Switzerland AG. Stochastic models in which agents interact with their neighborhood according to a network topology are a powerful modeling framework to study the emergence of complex dynamic patterns in real-world systems. Stochastic simulations are often the preferred—sometimes the only feasible—way to investigate such systems. Previous research focused primarily on Markovian models where the random time until an interaction happens follows an exponential distribution. In this work, we study a general framework to model systems where each agent is in one of several states. Agents can change their state at random, influenced by their complete neighborhood, while the time to the next event can follow an arbitrary probability distribution. Classically, these simulations are hindered by high computational costs of updating the rates of interconnected agents and sampling the random residence times from arbitrary distributions. We propose a rejection-based, event-driven simulation algorithm to overcome these limitations. Our method over-approximates the instantaneous rates corresponding to inter-event times while rejection events counter-balance these over-approximations. We demonstrate the effectiveness of our approach on models of epidemic and information spreading.

@misc{
 title = {A hybrid HMM approach for the dynamics of DNA methylation},
 type = {misc},
 year = {2019},
 source = {arXiv},
 keywords = {DNA Methylation,Hidden Markov Model,Hybrid Stochastic Model},
 id = {6fa82625-7d08-3fa5-8858-67ec7db874fd},
 created = {2020-10-29T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-01T08:09:50.946Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2019, arXiv, All rights reserved. The understanding of mechanisms that control epigenetic changes is an important research area in modern functional biology. Epigenetic modifications such as DNA methylation are in general very stable over many cell divisions. DNA methylation can however be subject to specific and fast changes over a short time scale even in non-dividing (i.e. not-replicating) cells. Such dynamic DNA methylation changes are caused by a combination of active demethylation and de novo methylation processes which have not been investigated in integrated models. Here we present a hybrid (hidden) Markov model to describe the cycle of methylation and demethylation over (short) time scales. Our hybrid model decribes several molecular events either happening at deterministic points (i.e. describing mechanisms that occur only during cell division) and other events occurring at random time points. We test our model on mouse embryonic stem cells using time-resolved data. We predict methylation changes and estimate the efficiencies of the different modification steps related to DNA methylation and demethylation.},
 bibtype = {misc},
 author = {Kyriakopoulos, C. and Giehr, P. and Lück, A. and Walter, J. and Wolf, V.}
}

Copyright © 2019, arXiv, All rights reserved. The understanding of mechanisms that control epigenetic changes is an important research area in modern functional biology. Epigenetic modifications such as DNA methylation are in general very stable over many cell divisions. DNA methylation can however be subject to specific and fast changes over a short time scale even in non-dividing (i.e. not-replicating) cells. Such dynamic DNA methylation changes are caused by a combination of active demethylation and de novo methylation processes which have not been investigated in integrated models. Here we present a hybrid (hidden) Markov model to describe the cycle of methylation and demethylation over (short) time scales. Our hybrid model decribes several molecular events either happening at deterministic points (i.e. describing mechanisms that occur only during cell division) and other events occurring at random time points. We test our model on mouse embryonic stem cells using time-resolved data. We predict methylation changes and estimate the efficiencies of the different modification steps related to DNA methylation and demethylation.

@misc{
 title = {A Stochastic Automata Network Description for Spatial DNA-Methylation Models},
 type = {misc},
 year = {2019},
 source = {arXiv},
 keywords = {DNA Methylation,Spatial Stochastic Model,Stochastic Automata Networks},
 id = {f8767440-27b0-31ff-adea-869125c96117},
 created = {2020-11-01T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-03T18:06:38.924Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2019, arXiv, All rights reserved. DNA methylation is an important biological mechanism to regulate gene expression and control cell development. Mechanistic modeling has become a popular approach to enhance our understanding of the dynamics of methylation pattern formation in living cells. Recent findings suggest that the methylation state of a cytosine base can be influenced by its DNA neighborhood. Therefore, it is necessary to generalize existing mathematical models that consider only one cytosine and its partner on the opposite DNA-strand (CpG), in order to include such neighborhood dependencies. One approach is to describe the system as a stochastic automata network (SAN) with functional transitions. We show that single-CpG models can successfully be generalized to multiple CpGs using the SAN description and verify the results by comparing them to results from extensive Monte-Carlo simulations.},
 bibtype = {misc},
 author = {Lück, A. and Wolf, V.}
}

Copyright © 2019, arXiv, All rights reserved. DNA methylation is an important biological mechanism to regulate gene expression and control cell development. Mechanistic modeling has become a popular approach to enhance our understanding of the dynamics of methylation pattern formation in living cells. Recent findings suggest that the methylation state of a cytosine base can be influenced by its DNA neighborhood. Therefore, it is necessary to generalize existing mathematical models that consider only one cytosine and its partner on the opposite DNA-strand (CpG), in order to include such neighborhood dependencies. One approach is to describe the system as a stochastic automata network (SAN) with functional transitions. We show that single-CpG models can successfully be generalized to multiple CpGs using the SAN description and verify the results by comparing them to results from extensive Monte-Carlo simulations.

@misc{
 title = {Rejection-based simulation of non-markovian agents on complex networks},
 type = {misc},
 year = {2019},
 source = {arXiv},
 keywords = {Complex networks,Epidemic modeling,Gillespie simulation,Multi-agent system,Rejection sampling},
 id = {ca1d6594-2f80-3d32-84aa-5d04c5d76f81},
 created = {2020-11-01T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-04T00:31:51.717Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2019, arXiv, All rights reserved. Stochastic models in which agents interact with their neighborhood according to a network topology are a powerful modeling framework to study the emergence of complex dynamic patterns in real-world systems. Stochastic simulations are often the preferred|sometimes the only feasible|way to investigate such systems. Previous research focused primarily on Markovian models where the random time until an interaction happens follows an exponential distribution. In this work, we study a general framework to model systems where each agent is in one of several states. Agents can change their state at random, inuenced by their complete neighborhood, while the time to the next event can follow an arbitrary probability distribution. Classically, these simulations are hindered by high computational costs of updating the rates of interconnected agents and sampling the random residence times from arbitrary distributions. We propose a rejection-based, event-driven simulation algorithm to overcome these limitations. Our method over-approximates the instantaneous rates corresponding to inter-event times while rejection events counterbalance these over-approximations. We demonstrate the effectiveness of our approach on models of epidemic and information spreading.},
 bibtype = {misc},
 author = {Gromann, G. and Bortolussi, L. and Wolf, V.}
}

Copyright © 2019, arXiv, All rights reserved. Stochastic models in which agents interact with their neighborhood according to a network topology are a powerful modeling framework to study the emergence of complex dynamic patterns in real-world systems. Stochastic simulations are often the preferred|sometimes the only feasible|way to investigate such systems. Previous research focused primarily on Markovian models where the random time until an interaction happens follows an exponential distribution. In this work, we study a general framework to model systems where each agent is in one of several states. Agents can change their state at random, inuenced by their complete neighborhood, while the time to the next event can follow an arbitrary probability distribution. Classically, these simulations are hindered by high computational costs of updating the rates of interconnected agents and sampling the random residence times from arbitrary distributions. We propose a rejection-based, event-driven simulation algorithm to overcome these limitations. Our method over-approximates the instantaneous rates corresponding to inter-event times while rejection events counterbalance these over-approximations. We demonstrate the effectiveness of our approach on models of epidemic and information spreading.

@misc{
 title = {Generalized Method of Moments Estimation for Stochastic Models of DNA Methylation Patterns},
 type = {misc},
 year = {2019},
 source = {arXiv},
 keywords = {DNA Methylation,Generalized Method of Moments,Stochastic Modeling},
 id = {f3a1a235-38b1-3ce3-ba2d-01b620c718b9},
 created = {2020-11-03T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-04T18:13:16.267Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2019, arXiv, All rights reserved. With recent advances in sequencing technologies, large amounts of epigenomic data have become available and computational methods are contributing significantly to the progress of epigenetic research. As an orthogonal approach to methods based on machine learning, mechanistic modeling aims at a description of the mechanisms underlying epigenetic changes. Here, we propose an efficient method for parameter estimation for stochastic models that describe the dynamics of DNA methylation patterns over time. Our method is based on the Generalized Method of Moments (GMM) and gives results with an accuracy similar to that of maximum likelihood-based estimation approaches. However, in contrast to the latter, the GMM still allows an efficient and accurate calibration of parameters even if the complexity of the model is increased by considering longer methylation patterns. We show the usefulness of our method by applying it to hairpin bisulfite sequencing data from mouse ESCs for varying pattern lengths.},
 bibtype = {misc},
 author = {Lück, A. and Wolf, V.}
}

Copyright © 2019, arXiv, All rights reserved. With recent advances in sequencing technologies, large amounts of epigenomic data have become available and computational methods are contributing significantly to the progress of epigenetic research. As an orthogonal approach to methods based on machine learning, mechanistic modeling aims at a description of the mechanisms underlying epigenetic changes. Here, we propose an efficient method for parameter estimation for stochastic models that describe the dynamics of DNA methylation patterns over time. Our method is based on the Generalized Method of Moments (GMM) and gives results with an accuracy similar to that of maximum likelihood-based estimation approaches. However, in contrast to the latter, the GMM still allows an efficient and accurate calibration of parameters even if the complexity of the model is increased by considering longer methylation patterns. We show the usefulness of our method by applying it to hairpin bisulfite sequencing data from mouse ESCs for varying pattern lengths.

@misc{
 title = {Control variates for stochastic simulation of chemical reaction networks},
 type = {misc},
 year = {2019},
 source = {arXiv},
 keywords = {Chemical Master Equation,Chemical Reaction Network,Control Variates,Moment Equations,Stochastic Simulation Algorithm,Variance Reduction},
 id = {cd4e22b9-1605-3ac1-8792-3d9b87638905},
 created = {2020-11-10T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-13T16:09:57.458Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2019, arXiv, All rights reserved. Stochastic simulation is a widely used method for estimating quantities in models of chemical reaction networks where uncertainty plays a crucial role. However, reducing the statistical uncertainty of the corresponding estimators requires the generation of a large number of simulation runs, which is computationally expensive. To reduce the number of necessary runs, we propose a variance reduction technique based on control variates. We exploit constraints on the statistical moments of the stochastic process to reduce the estimators’ variances. We develop an algorithm that selects appropriate control variates in an on-line fashion and demonstrate the efficiency of our approach on several case studies.},
 bibtype = {misc},
 author = {Backenköhler, M. and Bortolussi, L. and Wolf, V.}
}

Copyright © 2019, arXiv, All rights reserved. Stochastic simulation is a widely used method for estimating quantities in models of chemical reaction networks where uncertainty plays a crucial role. However, reducing the statistical uncertainty of the corresponding estimators requires the generation of a large number of simulation runs, which is computationally expensive. To reduce the number of necessary runs, we propose a variance reduction technique based on control variates. We exploit constraints on the statistical moments of the stochastic process to reduce the estimators’ variances. We develop an algorithm that selects appropriate control variates in an on-line fashion and demonstrate the efficiency of our approach on several case studies.

@book{
 title = {Rejection-Based Simulation of Stochastic Spreading Processes on Complex Networks},
 type = {book},
 year = {2019},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 keywords = {Epidemic modeling,Gillespie Algorithm,Monte-Carlo simulation,SIR,Spreading process},
 volume = {11705 LNBI},
 id = {33a3930d-b762-3810-874a-ad373b9c88a3},
 created = {2019-08-23T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2021-01-07T21:17:09.079Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {© 2019, Springer Nature Switzerland AG. Stochastic processes can model many emerging phenomena on networks, like the spread of computer viruses, rumors, or infectious diseases. Understanding the dynamics of such stochastic spreading processes is therefore of fundamental interest. In this work we consider the wide-spread compartment model where each node is in one of several states (or compartments). Nodes change their state randomly after an exponentially distributed waiting time and according to a given set of rules. For networks of realistic size, even the generation of only a single stochastic trajectory of a spreading process is computationally very expensive. Here, we propose a novel simulation approach, which combines the advantages of event-based simulation and rejection sampling. Our method outperforms state-of-the-art methods in terms of absolute runtime and scales significantly better while being statistically equivalent.},
 bibtype = {book},
 author = {Großmann, G. and Wolf, V.},
 doi = {10.1007/978-3-030-28042-0_5}
}

© 2019, Springer Nature Switzerland AG. Stochastic processes can model many emerging phenomena on networks, like the spread of computer viruses, rumors, or infectious diseases. Understanding the dynamics of such stochastic spreading processes is therefore of fundamental interest. In this work we consider the wide-spread compartment model where each node is in one of several states (or compartments). Nodes change their state randomly after an exponentially distributed waiting time and according to a given set of rules. For networks of realistic size, even the generation of only a single stochastic trajectory of a spreading process is computationally very expensive. Here, we propose a novel simulation approach, which combines the advantages of event-based simulation and rejection sampling. Our method outperforms state-of-the-art methods in terms of absolute runtime and scales significantly better while being statistically equivalent.

@book{
 title = {Preface},
 type = {book},
 year = {2019},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {11785 LNCS},
 id = {6b6a38e8-b302-32c5-851a-6fe8ac051ecf},
 created = {2019-10-11T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2021-01-13T11:15:54.646Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 bibtype = {book},
 author = {Parker, D. and Wolf, V.}
}

@article{
 title = {Hidden markov modelling reveals neighborhood dependence of dnmt3a and 3b activity},
 type = {article},
 year = {2019},
 keywords = {DNA methylation,hidden Markov model,spatial stochastic model},
 volume = {16},
 id = {373bf5be-01f4-3b80-b8dd-5a2f8ccea36a},
 created = {2019-10-19T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2021-01-15T12:53:09.985Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {© 2019 Institute of Electrical and Electronics Engineers Inc.. All rights reserved. DNA methylation is an epigenetic mark whose important role in development has been widely recognized. This epigenetic modification results in heritable information not encoded by the DNA sequence. The underlying mechanisms controlling DNA methylation are only partly understood. Several mechanistic models of enzyme activities responsible for DNA methylation have been proposed. Here, we extend existing Hidden Markov Models HMMs for DNA methylation by describing the occurrence of spatial methylation patterns over time and propose several models with different neighborhood dependences. Furthermore, we investigate correlations between the neighborhood dependence and other genomic information. We perform numerical analysis of the HMMs applied to comprehensive hairpin and non-hairpin bisulfite sequencing measurements and accurately predict wild-type data. We find evidence that the activities of Dnmt3a and Dnmt3b responsible for de novo methylation depend on 5' left but not on 3' right neighboring CpGs in a sequencing string.},
 bibtype = {article},
 author = {Luck, A. and Giehr, P. and Nordstrom, K. and Walter, J. and Wolf, V.},
 doi = {10.1109/TCBB.2019.2910814},
 journal = {IEEE/ACM Transactions on Computational Biology and Bioinformatics},
 number = {5}
}

© 2019 Institute of Electrical and Electronics Engineers Inc.. All rights reserved. DNA methylation is an epigenetic mark whose important role in development has been widely recognized. This epigenetic modification results in heritable information not encoded by the DNA sequence. The underlying mechanisms controlling DNA methylation are only partly understood. Several mechanistic models of enzyme activities responsible for DNA methylation have been proposed. Here, we extend existing Hidden Markov Models HMMs for DNA methylation by describing the occurrence of spatial methylation patterns over time and propose several models with different neighborhood dependences. Furthermore, we investigate correlations between the neighborhood dependence and other genomic information. We perform numerical analysis of the HMMs applied to comprehensive hairpin and non-hairpin bisulfite sequencing measurements and accurately predict wild-type data. We find evidence that the activities of Dnmt3a and Dnmt3b responsible for de novo methylation depend on 5' left but not on 3' right neighboring CpGs in a sequencing string.

@article{
 title = {Lumping of degree-based mean-field and pair-approximation equations for multistate contact processes},
 type = {article},
 year = {2018},
 volume = {97},
 id = {d91ea7af-beca-334d-aeb4-a73b0b6cfac6},
 created = {2018-01-18T12:07:21.707Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-01-18T12:07:21.707Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {© 2018 American Physical Society. Contact processes form a large and highly interesting class of dynamic processes on networks, including epidemic and information-spreading networks. While devising stochastic models of such processes is relatively easy, analyzing them is very challenging from a computational point of view, particularly for large networks appearing in real applications. One strategy to reduce the complexity of their analysis is to rely on approximations, often in terms of a set of differential equations capturing the evolution of a random node, distinguishing nodes with different topological contexts (i.e., different degrees of different neighborhoods), such as degree-based mean-field (DBMF), approximate-master-equation (AME), or pair-approximation (PA) approaches. The number of differential equations so obtained is typically proportional to the maximum degree kmax of the network, which is much smaller than the size of the master equation of the underlying stochastic model, yet numerically solving these equations can still be problematic for large kmax. In this paper, we consider AME and PA, extended to cope with multiple local states, and we provide an aggregation procedure that clusters together nodes having similar degrees, treating those in the same cluster as indistinguishable, thus reducing the number of equations while preserving an accurate description of global observables of interest. We also provide an automatic way to build such equations and to identify a small number of degree clusters that give accurate results. The method is tested on several case studies, where it shows a high level of compression and a reduction of computational time of several orders of magnitude for large networks, with minimal loss in accuracy.},
 bibtype = {article},
 author = {Kyriakopoulos, C. and Grossmann, G. and Wolf, V. and Bortolussi, L.},
 doi = {10.1103/PhysRevE.97.012301},
 journal = {Physical Review E},
 number = {1}
}

© 2018 American Physical Society. Contact processes form a large and highly interesting class of dynamic processes on networks, including epidemic and information-spreading networks. While devising stochastic models of such processes is relatively easy, analyzing them is very challenging from a computational point of view, particularly for large networks appearing in real applications. One strategy to reduce the complexity of their analysis is to rely on approximations, often in terms of a set of differential equations capturing the evolution of a random node, distinguishing nodes with different topological contexts (i.e., different degrees of different neighborhoods), such as degree-based mean-field (DBMF), approximate-master-equation (AME), or pair-approximation (PA) approaches. The number of differential equations so obtained is typically proportional to the maximum degree kmax of the network, which is much smaller than the size of the master equation of the underlying stochastic model, yet numerically solving these equations can still be problematic for large kmax. In this paper, we consider AME and PA, extended to cope with multiple local states, and we provide an aggregation procedure that clusters together nodes having similar degrees, treating those in the same cluster as indistinguishable, thus reducing the number of equations while preserving an accurate description of global observables of interest. We also provide an automatic way to build such equations and to identify a small number of degree clusters that give accurate results. The method is tested on several case studies, where it shows a high level of compression and a reduction of computational time of several orders of magnitude for large networks, with minimal loss in accuracy.

@book{
 title = {Student performance prediction and optimal course selection: An MDP approach},
 type = {book},
 year = {2018},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {10729 LNCS},
 id = {c8087882-ff0e-353f-b217-8e1fa594139f},
 created = {2018-02-27T10:31:01.088Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-02-27T10:31:01.088Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {© Springer International Publishing AG 2018. Improving the performance of students is an important challenge for higher education institutions. At most European universities, duration and completion rate of degrees are highly varying and consulting services are offered to increase student achievement. Here, we propose a data analytics approach to determine optimal choices for the courses of the next term. We use machine learning techniques to predict the performance of a student in upcoming courses. These prediction form the transition probabilities of a Markov decision process (MDP) that describes the course of studies of a student. Using this model we plan to explore the effect of different strategies on student performance.},
 bibtype = {book},
 author = {Backenköhler, M. and Wolf, V.},
 doi = {10.1007/978-3-319-74781-1_3}
}

© Springer International Publishing AG 2018. Improving the performance of students is an important challenge for higher education institutions. At most European universities, duration and completion rate of degrees are highly varying and consulting services are offered to increase student achievement. Here, we propose a data analytics approach to determine optimal choices for the courses of the next term. We use machine learning techniques to predict the performance of a student in upcoming courses. These prediction form the transition probabilities of a Markov decision process (MDP) that describes the course of studies of a student. Using this model we plan to explore the effect of different strategies on student performance.

@article{
 title = {Approximate Adaptive Uniformization of Continuous-Time Markov Chains},
 type = {article},
 year = {2018},
 websites = {http://linkinghub.elsevier.com/retrieve/pii/S0307904X18302191},
 month = {5},
 id = {6f8a0895-e09e-3b05-a444-45948367fa45},
 created = {2018-05-28T11:36:14.422Z},
 accessed = {2018-05-28},
 file_attached = {true},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-05-28T11:37:11.111Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We consider the approximation of transient (time dependent) probability distributions ofdiscrete-state continuous-time Markov chains on large, possibly infinite state spaces. A framework for approximate adaptive uniformization is provided, which generalizes the well-known uniformization technique and many of its variants. Based on a birth process and a discrete-time Markov chain a computationally tractable approximating process/model is constructed. We investigate the theoretical properties of this process and prove that it yields computable lower and upper bounds for the desired transient probabilities. Finally, we discuss different specific ways of performing approximate adaptive uniformization and analyze the corresponding approximation errors. The application is illustrated by an example of a stochastic epidemic model.},
 bibtype = {article},
 author = {Andreychesnko, Alexander and Sandmann, Werner and Wolf, Verena},
 doi = {10.1016/j.apm.2018.05.009},
 journal = {Applied Mathematical Modelling}
}

We consider the approximation of transient (time dependent) probability distributions ofdiscrete-state continuous-time Markov chains on large, possibly infinite state spaces. A framework for approximate adaptive uniformization is provided, which generalizes the well-known uniformization technique and many of its variants. Based on a birth process and a discrete-time Markov chain a computationally tractable approximating process/model is constructed. We investigate the theoretical properties of this process and prove that it yields computable lower and upper bounds for the desired transient probabilities. Finally, we discuss different specific ways of performing approximate adaptive uniformization and analyze the corresponding approximation errors. The application is illustrated by an example of a stochastic epidemic model.

@article{
 title = {Simulating the Large-Scale Erosion of Genomic Privacy Over Time},
 type = {article},
 year = {2018},
 keywords = {Bioinformatics,DNA,Genomic privacy,Genomics,Privacy,Sequential analysis,Sociology,Statistics,graphical models,inference,simulations},
 pages = {1},
 id = {d3a2eb93-0e7c-321f-85b9-44f883afac6e},
 created = {2018-08-07T10:22:44.619Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-08-07T10:22:44.619Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 source_type = {JOUR},
 private_publication = {false},
 bibtype = {article},
 author = {Backes, M and Berrang, P and Humbert, M and Shen, X and Wolf, V},
 doi = {10.1109/TCBB.2018.2859380},
 journal = {IEEE/ACM Transactions on Computational Biology and Bioinformatics}
}

@article{
 title = {Stochastic hybrid models of gene regulatory networks – A PDE approach},
 type = {article},
 year = {2018},
 keywords = {Gene regulatory networks,Hybrid stochastic model},
 pages = {170-177},
 volume = {305},
 websites = {http://www.sciencedirect.com/science/article/pii/S0025556418302098},
 id = {266707df-352a-3370-9025-321bc4df3d11},
 created = {2018-10-01T18:32:08.857Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-10-01T18:32:08.857Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 source_type = {JOUR},
 private_publication = {false},
 bibtype = {article},
 author = {Kurasov, Pavel and Lück, Alexander and Mugnolo, Delio and Wolf, Verena},
 doi = {https://doi.org/10.1016/j.mbs.2018.09.009},
 journal = {Mathematical Biosciences}
}

@article{
 title = {Two are better than one: HPoxBS - hairpin oxidative bisulfite sequencing},
 type = {article},
 year = {2018},
 pages = {e88-e88},
 volume = {46},
 websites = {http://dx.doi.org/10.1093/nar/gky422},
 month = {9},
 day = {6},
 id = {92a957ee-931a-3f68-b780-0c548edf5b3c},
 created = {2018-10-01T18:44:58.962Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-10-01T18:44:58.962Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 source_type = {JOUR},
 notes = {10.1093/nar/gky422},
 private_publication = {false},
 abstract = {The controlled and stepwise oxidation of 5mC to 5hmC, 5fC and 5caC by Tet enzymes is influencing the chemical and biological properties of cytosine. Besides direct effects on gene regulation, oxidised forms influence the dynamics of demethylation and re-methylation processes. So far, no combined methods exist which allow to precisely determine the strand specific localisation of cytosine modifications along with their CpG symmetric distribution. Here we describe a comprehensive protocol combining conventional hairpin bisulfite with oxidative bisulfite sequencing (HPoxBS) to determine the strand specific distribution of 5mC and 5hmC at base resolution. We apply this method to analyse the contribution of local oxidative effects on DNA demethylation in mouse ES cells. Our method includes the HPoxBS workflow and subsequent data analysis using our developed software tools. Besides a precise estimation and display of strand specific 5mC and 5hmC levels at base resolution we apply the data to predict region specific activities of Dnmt and Tet enzymes. Our experimental and computational workflow provides a precise double strand display of 5mC and 5hmC modifications at single base resolution. Based on our data we predict region specific Tet and Dnmt enzyme efficiencies shaping the distinct locus levels and patterns of 5hmC and 5mC.},
 bibtype = {article},
 author = {Giehr, Pascal and Kyriakopoulos, Charalampos and Lepikhov, Konstantin and Wallner, Stefan and Wolf, Verena and Walter, Jörn},
 journal = {Nucleic Acids Research},
 number = {15}
}

The controlled and stepwise oxidation of 5mC to 5hmC, 5fC and 5caC by Tet enzymes is influencing the chemical and biological properties of cytosine. Besides direct effects on gene regulation, oxidised forms influence the dynamics of demethylation and re-methylation processes. So far, no combined methods exist which allow to precisely determine the strand specific localisation of cytosine modifications along with their CpG symmetric distribution. Here we describe a comprehensive protocol combining conventional hairpin bisulfite with oxidative bisulfite sequencing (HPoxBS) to determine the strand specific distribution of 5mC and 5hmC at base resolution. We apply this method to analyse the contribution of local oxidative effects on DNA demethylation in mouse ES cells. Our method includes the HPoxBS workflow and subsequent data analysis using our developed software tools. Besides a precise estimation and display of strand specific 5mC and 5hmC levels at base resolution we apply the data to predict region specific activities of Dnmt and Tet enzymes. Our experimental and computational workflow provides a precise double strand display of 5mC and 5hmC modifications at single base resolution. Based on our data we predict region specific Tet and Dnmt enzyme efficiencies shaping the distinct locus levels and patterns of 5hmC and 5mC.

@inproceedings{
 title = {Lumping the Approximate Master Equation for Multistate Processes on Complex Networks},
 type = {inproceedings},
 year = {2018},
 id = {99802f94-e44a-372e-87bb-eff51161536f},
 created = {2018-10-01T18:44:59.056Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-10-01T18:44:59.056Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Großmann, Gerrit and Kyriakopoulos, Charalampos and Luca Bortolussi, V and Wolf, Erena},
 booktitle = {Proceedings of the 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018)}
}

@article{
 title = {Moment-Based Parameter Estimation for Stochastic Reaction Networks in Equilibrium},
 type = {article},
 year = {2018},
 pages = {1180-1192},
 volume = {15},
 websites = {https://doi.org/10.1109/TCBB.2017.2775219},
 month = {7},
 publisher = {IEEE Computer Society Press},
 city = {Los Alamitos, CA, USA},
 id = {304ddb42-0df3-3f22-9c86-a3a2d281629f},
 created = {2018-10-01T18:45:43.315Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-10-01T18:45:43.315Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Backenkohler:2018:MPE:3281080.3281105},
 source_type = {article},
 private_publication = {false},
 bibtype = {article},
 author = {Backenkohler, Michael and Bortolussi, Luca and Wolf, Verena},
 doi = {10.1109/TCBB.2017.2775219},
 journal = {IEEE/ACM Trans. Comput. Biol. Bioinformatics},
 number = {4}
}

@misc{
 title = {Rejection-based simulation of stochastic spreading processes on complex networks},
 type = {misc},
 year = {2018},
 source = {arXiv},
 keywords = {Epidemic modeling,Gillespie algorithm,Monte-Carlo simulation,SIR,Spreading process},
 id = {396170b8-bf97-3ef8-969a-2cf0b9e168f2},
 created = {2020-10-27T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-10-31T03:44:58.369Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2018, arXiv, All rights reserved. Stochastic processes can model many emerging phenomena on networks, like the spread of computer viruses, rumors, or infectious diseases. Understanding the dynamics of such stochastic spreading processes is therefore of fundamental interest. In this work we consider the wide-spread compartment model where each node is in one of several states (or compartments). Nodes change their state randomly after an exponentially distributed waiting time and according to a given set of rules. For networks of realistic size, even the generation of only a single stochastic trajectory of a spreading process is computationally very expensive. Here, we propose a novel simulation approach, which combines the advantages of event-based simulation and rejection sampling. Our method outperforms state-of-the-art methods in terms of absolute runtime and scales significantly better, while being statistically equivalent.},
 bibtype = {misc},
 author = {Großmann, G. and Wolf, V.}
}

Copyright © 2018, arXiv, All rights reserved. Stochastic processes can model many emerging phenomena on networks, like the spread of computer viruses, rumors, or infectious diseases. Understanding the dynamics of such stochastic spreading processes is therefore of fundamental interest. In this work we consider the wide-spread compartment model where each node is in one of several states (or compartments). Nodes change their state randomly after an exponentially distributed waiting time and according to a given set of rules. For networks of realistic size, even the generation of only a single stochastic trajectory of a spreading process is computationally very expensive. Here, we propose a novel simulation approach, which combines the advantages of event-based simulation and rejection sampling. Our method outperforms state-of-the-art methods in terms of absolute runtime and scales significantly better, while being statistically equivalent.

@misc{
 title = {Lumping the approximate master equation for multistate processes on complex networks},
 type = {misc},
 year = {2018},
 source = {arXiv},
 keywords = {AME,Complex Networks,Lumping,Model Reduction,Multistate Processes},
 id = {de3fb765-73fe-3930-8320-026c4fb50c24},
 created = {2020-10-29T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-01T12:16:39.518Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2018, arXiv, All rights reserved. Complex networks play an important role in human society and in nature. Stochastic multistate processes provide a powerful framework to model a variety of emerging phenomena such as the dynamics of an epidemic or the spreading of information on complex networks. In recent years, mean-field type approximations gained widespread attention as a tool to analyze and understand complex network dynamics. They reduce the model’s complexity by assuming that all nodes with a similar local structure behave identically. Among these methods the approximate master equation (AME) provides the most accurate description of complex networks’ dynamics by considering the whole neighborhood of a node. The size of a typical network though renders the numerical solution of multistate AME infeasible. Here, we propose an efficient approach for the numerical solution of the AME that exploits similarities between the differential equations of structurally similar groups of nodes. We cluster a large number of similar equations together and solve only a single lumped equation per cluster. Our method allows the application of the AME to real-world networks, while preserving its accuracy in computing estimates of global network properties, such as the fraction of nodes in a state at a given time.},
 bibtype = {misc},
 author = {Großmann, G. and Kyriakopoulos, C. and Bortolussi, L. and Wolf, V.}
}

Copyright © 2018, arXiv, All rights reserved. Complex networks play an important role in human society and in nature. Stochastic multistate processes provide a powerful framework to model a variety of emerging phenomena such as the dynamics of an epidemic or the spreading of information on complex networks. In recent years, mean-field type approximations gained widespread attention as a tool to analyze and understand complex network dynamics. They reduce the model’s complexity by assuming that all nodes with a similar local structure behave identically. Among these methods the approximate master equation (AME) provides the most accurate description of complex networks’ dynamics by considering the whole neighborhood of a node. The size of a typical network though renders the numerical solution of multistate AME infeasible. Here, we propose an efficient approach for the numerical solution of the AME that exploits similarities between the differential equations of structurally similar groups of nodes. We cluster a large number of similar equations together and solve only a single lumped equation per cluster. Our method allows the application of the AME to real-world networks, while preserving its accuracy in computing estimates of global network properties, such as the fraction of nodes in a state at a given time.

@misc{
 title = {Analytic solutions for stochastic hybrid models of gene regulatory networks},
 type = {misc},
 year = {2018},
 source = {arXiv},
 keywords = {-semigroups -semigroups. 0,Petri networks,Systems of PDEs},
 id = {4411b906-16c1-3a6b-87fc-f87a6212ab8f},
 created = {2020-11-10T23:59:00.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2020-11-13T09:11:03.810Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Copyright © 2018, arXiv, All rights reserved. Discrete-state stochastic models are a popular approach to describe the inherent stochasticity of gene expression in single cells. The analysis of such models is hindered by the fact that the underlying discrete state space is extremely large. Therefore hybrid models, in which protein counts are replaced by average protein concentrations, have become a popular alternative. The evolution of the corresponding probability density functions is given by a coupled system of hyperbolic PDEs. This system has Markovian nature but its hyperbolic structure makes it difficult to apply standard functional analytical methods. We are able to prove convergence towards the stationary solution and determine such equilibrium explicitly by combining abstract methods from the theory of positive operators and elementary ideas from potential analysis.MSC Codes 35B09, 47D06, 93C20, 35F46},
 bibtype = {misc},
 author = {Kurasov, P. and Mugnolo, D. and Wolf, V.}
}

Copyright © 2018, arXiv, All rights reserved. Discrete-state stochastic models are a popular approach to describe the inherent stochasticity of gene expression in single cells. The analysis of such models is hindered by the fact that the underlying discrete state space is extremely large. Therefore hybrid models, in which protein counts are replaced by average protein concentrations, have become a popular alternative. The evolution of the corresponding probability density functions is given by a coupled system of hyperbolic PDEs. This system has Markovian nature but its hyperbolic structure makes it difficult to apply standard functional analytical methods. We are able to prove convergence towards the stationary solution and determine such equilibrium explicitly by combining abstract methods from the theory of positive operators and elementary ideas from potential analysis.MSC Codes 35B09, 47D06, 93C20, 35F46

@article{
 title = {A stochastic model for the formation of spatial methylation patterns},
 type = {article},
 year = {2017},
 keywords = {DNA methylation,Hidden Markov model,Spatial stochastic model},
 volume = {10545 LNBI},
 websites = {https://link.springer.com/chapter/10.1007/978-3-319-67471-1_10},
 id = {c321ad54-fe9f-3e23-98ee-9076f44a9004},
 created = {2017-10-16T22:20:36.889Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-11-29T15:21:33.510Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {© 2017, Springer International Publishing AG. DNA methylation is an epigenetic mechanism whose important role in development has been widely recognized. This epigenetic modification results in heritable changes in gene expression not encoded by the DNA sequence. The underlying mechanisms controlling DNA methylation are only partly understood and recently different mechanistic models of enzyme activities responsible for DNA methylation have been proposed. Here we extend existing Hidden Markov Models (HMMs) for DNA methylation by describing the occurrence of spatial methylation patterns over time and propose several models with different neighborhood dependencies. We perform numerical analysis of the HMMs applied to bisulfite sequencing measurements and accurately predict wild-type data. In addition, we find evidence that the enzymes’ activities depend on the left 5’ neighborhood but not on the right 3’ neighborhood.},
 bibtype = {article},
 author = {Lück, A. and Giehr, P. and Walter, J. and Wolf, V.},
 doi = {10.1007/978-3-319-67471-1_10},
 journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}
}

© 2017, Springer International Publishing AG. DNA methylation is an epigenetic mechanism whose important role in development has been widely recognized. This epigenetic modification results in heritable changes in gene expression not encoded by the DNA sequence. The underlying mechanisms controlling DNA methylation are only partly understood and recently different mechanistic models of enzyme activities responsible for DNA methylation have been proposed. Here we extend existing Hidden Markov Models (HMMs) for DNA methylation by describing the occurrence of spatial methylation patterns over time and propose several models with different neighborhood dependencies. We perform numerical analysis of the HMMs applied to bisulfite sequencing measurements and accurately predict wild-type data. In addition, we find evidence that the enzymes’ activities depend on the left 5’ neighborhood but not on the right 3’ neighborhood.

@article{
 title = {Moment-Based Parameter Estimation for Stochastic Reaction Networks in Equilibrium},
 type = {article},
 year = {2017},
 websites = {http://ieeexplore.ieee.org/document/8115212/},
 publisher = {IEEE},
 id = {9ff37a5f-adc1-3772-9479-4a8c426f889c},
 created = {2017-11-29T15:18:00.188Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-11-29T15:21:33.407Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {backenkohler2017moment},
 source_type = {article},
 private_publication = {false},
 bibtype = {article},
 author = {Backenkohler, Michael and Bortolussi, Luca and Wolf, Verena},
 journal = {IEEE/ACM Transactions on Computational Biology and Bioinformatics}
}

@article{
 title = {Lumping of Degree-Based Mean Field and Pair Approximation Equations for Multi-State Contact Processes},
 type = {article},
 year = {2017},
 volume = {97},
 websites = {https://arxiv.org/pdf/1706.06964.pdf},
 id = {42871d61-424c-322a-8ce6-d2861d81a1d0},
 created = {2018-01-08T09:32:58.692Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2018-01-08T09:32:58.692Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {kyriakopoulos2017lumping},
 source_type = {article},
 private_publication = {false},
 bibtype = {article},
 author = {Kyriakopoulos, Charalampos and Grossmann, Gerrit and Wolf, Verena and Bortolussi, Luca},
 journal = {Physical Review E}
}

@article{
 title = {H(O)TA: estimation of DNA methylation and hydroxylation levels and efficiencies from time course data},
 type = {article},
 year = {2016},
 pages = {Submitted},
 websites = {https://academic.oup.com//bioinformatics/article/33/11/1733/2959907/HOTA-estimation-of-DNA-methylation-and?guestAccessKey=026cfcd9-1f04-405c-b0b3-41716776d5f3},
 id = {fcb997f8-67a3-32ca-9395-3ce6a6bced88},
 created = {2016-06-01T14:28:49.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-11-29T15:18:00.397Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 bibtype = {article},
 author = {Giehr, Pascal and Kyriakopoulos, Charalampos and Wolf, Verena}
}

@article{
 title = {Generalized method of moments for estimating parameters of stochastic reaction networks},
 type = {article},
 year = {2016},
 keywords = {Generalized method,[Biochemical reaction network},
 volume = {10},
 websites = {https://bmcsystbiol.biomedcentral.com/articles/10.1186/s12918-016-0342-8},
 id = {d7c74df1-ed7e-3de1-a349-42cf36f6a175},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-04-07T12:48:15.348Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {© 2016 The Author(s).Background: Discrete-state stochastic models have become a well-established approach to describe biochemical reaction networks that are influenced by the inherent randomness of cellular events. In the last years several methods for accurately approximating the statistical moments of such models have become very popular since they allow an efficient analysis of complex networks. Results: We propose a generalized method of moments approach for inferring the parameters of reaction networks based on a sophisticated matching of the statistical moments of the corresponding stochastic model and the sample moments of population snapshot data. The proposed parameter estimation method exploits recently developed moment-based approximations and provides estimators with desirable statistical properties when a large number of samples is available. We demonstrate the usefulness and efficiency of the inference method on two case studies. Conclusions: The generalized method of moments provides accurate and fast estimations of unknown parameters of reaction networks. The accuracy increases when also moments of order higher than two are considered. In addition, the variance of the estimator decreases, when more samples are given or when higher order moments are included.},
 bibtype = {article},
 author = {Lueck, Alexander and Wolf, Verena},
 doi = {10.1186/s12918-016-0342-8},
 journal = {BMC Systems Biology},
 number = {1}
}

© 2016 The Author(s).Background: Discrete-state stochastic models have become a well-established approach to describe biochemical reaction networks that are influenced by the inherent randomness of cellular events. In the last years several methods for accurately approximating the statistical moments of such models have become very popular since they allow an efficient analysis of complex networks. Results: We propose a generalized method of moments approach for inferring the parameters of reaction networks based on a sophisticated matching of the statistical moments of the corresponding stochastic model and the sample moments of population snapshot data. The proposed parameter estimation method exploits recently developed moment-based approximations and provides estimators with desirable statistical properties when a large number of samples is available. We demonstrate the usefulness and efficiency of the inference method on two case studies. Conclusions: The generalized method of moments provides accurate and fast estimations of unknown parameters of reaction networks. The accuracy increases when also moments of order higher than two are considered. In addition, the variance of the estimator decreases, when more samples are given or when higher order moments are included.

@book{
 title = {Hybrid stochastic simulation of rule-based polymerization models},
 type = {book},
 year = {2016},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 keywords = {Polymerization,Rule-based mod,[Hybrid simulation},
 volume = {9957 LNBI},
 websites = {https://link.springer.com/chapter/10.1007/978-3-319-47151-8_3},
 id = {8c92303b-a1b2-3f37-8344-b6548255b770},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-28T08:08:24.709Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {© Springer International Publishing AG 2016.Modeling and simulation of polymer formation is an important field of research not only in the material sciences but also in the life sciences due to the prominent role of processes such as actin filament formation and multivalent ligand-receptor interactions. While the advantages of a rule-based description of polymerizations has been successfully demonstrated, no efficient simulation of these mostly stiff processes is currently available, in particular for large system sizes. We present a hybrid stochastic simulation approach, in which the average changes of highly abundant species due to fast reactions are deterministically simulated while for the remaining species with small counts a rule-based simulation is performed. We propose a nesting of rejection steps to arrive at an approach that is efficient and accurate. We test our method on two case studies of polymerization.},
 bibtype = {book},
 author = {Krüger, T. and Wolf, V.},
 doi = {10.1007/978-3-319-47151-8_3}
}

© Springer International Publishing AG 2016.Modeling and simulation of polymer formation is an important field of research not only in the material sciences but also in the life sciences due to the prominent role of processes such as actin filament formation and multivalent ligand-receptor interactions. While the advantages of a rule-based description of polymerizations has been successfully demonstrated, no efficient simulation of these mostly stiff processes is currently available, in particular for large system sizes. We present a hybrid stochastic simulation approach, in which the average changes of highly abundant species due to fast reactions are deterministically simulated while for the remaining species with small counts a rule-based simulation is performed. We propose a nesting of rejection steps to arrive at an approach that is efficient and accurate. We test our method on two case studies of polymerization.

@article{
 title = {The Influence of Hydroxylation on Maintaining CpG Methylation Patterns: A Hidden Markov Model Approach},
 type = {article},
 year = {2016},
 volume = {12},
 websites = {http://journals.plos.org/ploscompbiol/article?id=10.1371/journal.pcbi.1004905},
 id = {07748d39-b52a-3977-ba64-999646a3cb8e},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-28T08:07:34.966Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {© 2016 Giehr et al.DNA methylation and demethylation are opposing processes that when in balance create stable patterns of epigenetic memory. The control of DNA methylation pattern formation by replication dependent and independent demethylation processes has been suggested to be influenced by Tet mediated oxidation of 5mC. Several alternative mechanisms have been proposed suggesting that 5hmC influences either replication dependent maintenance of DNA methylation or replication independent processes of active demethylation. Using high resolution hairpin oxidative bisulfite sequencing data, we precisely determine the amount of 5mC and 5hmC and model the contribution of 5hmC to processes of demethylation in mouse ESCs. We develop an extended hidden Markov model capable of accurately describing the regional contribution of 5hmC to demethylation dynamics. Our analysis shows that 5hmC has a strong impact on replication dependent demethylation, mainly by impairing methylation maintenance.},
 bibtype = {article},
 author = {Giehr, P. and Kyriakopoulos, C. and Ficz, G. and Wolf, V. and Walter, J.},
 doi = {10.1371/journal.pcbi.1004905},
 journal = {PLoS Computational Biology},
 number = {5}
}

© 2016 Giehr et al.DNA methylation and demethylation are opposing processes that when in balance create stable patterns of epigenetic memory. The control of DNA methylation pattern formation by replication dependent and independent demethylation processes has been suggested to be influenced by Tet mediated oxidation of 5mC. Several alternative mechanisms have been proposed suggesting that 5hmC influences either replication dependent maintenance of DNA methylation or replication independent processes of active demethylation. Using high resolution hairpin oxidative bisulfite sequencing data, we precisely determine the amount of 5mC and 5hmC and model the contribution of 5hmC to processes of demethylation in mouse ESCs. We develop an extended hidden Markov model capable of accurately describing the regional contribution of 5hmC to demethylation dynamics. Our analysis shows that 5hmC has a strong impact on replication dependent demethylation, mainly by impairing methylation maintenance.

@article{
 title = {Model Reconstruction for Moment-Based Stochastic Chemical Kinetics},
 type = {article},
 year = {2015},
 pages = {1-19},
 volume = {25},
 websites = {http://dl.acm.org/citation.cfm?id=2699712},
 id = {c12e1fa7-0b06-3366-aaf3-fda084f9db40},
 created = {2016-02-15T08:58:12.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Andreychenko2015},
 private_publication = {false},
 abstract = {Based on the theory of stochastic chemical kinetics, the inherent randomness of biochemical reaction networks can be described by discrete-state continuous-time Markov chains. However, the analysis of such processes is computationally expensive and sophisticated numerical methods are required. Here, we propose an analysis framework in which we integrate a number of moments of the process instead of the state probabilities. This results in a very efficient simulation of the time evolution of the process. To regain the state probabilities from the moment representation, we combine the fast moment-based simulation with a maximum entropy approach for the reconstruction of the underlying probability distribution. We investigate the usefulness of this combined approach in the setting of stochastic chemical kinetics and present numerical results for three reaction networks showing its efficiency and accuracy. Besides a simple dimerization system, we study a bistable switch system and a multiattractor network with complex dynamics.},
 bibtype = {article},
 author = {Andreychenko, Alexander and Mikeev, Linar and Wolf, Verena},
 doi = {10.1145/2699712},
 journal = {ACM Transactions on Modeling and Computer Simulation},
 number = {2}
}

Based on the theory of stochastic chemical kinetics, the inherent randomness of biochemical reaction networks can be described by discrete-state continuous-time Markov chains. However, the analysis of such processes is computationally expensive and sophisticated numerical methods are required. Here, we propose an analysis framework in which we integrate a number of moments of the process instead of the state probabilities. This results in a very efficient simulation of the time evolution of the process. To regain the state probabilities from the moment representation, we combine the fast moment-based simulation with a maximum entropy approach for the reconstruction of the underlying probability distribution. We investigate the usefulness of this combined approach in the setting of stochastic chemical kinetics and present numerical results for three reaction networks showing its efficiency and accuracy. Besides a simple dimerization system, we study a bistable switch system and a multiattractor network with complex dynamics.

@article{
 title = {Reconstruction of multimodal distributions for hybrid moment-based chemical kinetics},
 type = {article},
 year = {2015},
 pages = {156-163},
 volume = {3},
 websites = {http://openurl.ingenta.com/content?genre=article&issn=2330-152X&volume=3&issue=2&spage=156&epage=163},
 publisher = {American Scientific Publishers},
 id = {c6ddc434-b671-3e2b-a61e-e9167e2063b3},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {andreychenko2015reconstruction},
 source_type = {article},
 private_publication = {false},
 abstract = {The stochastic dynamics of biochemical reaction networks can be accurately described by discrete-state Markov processes where each chemical reaction corresponds to a state transition of the process. Due to the largeness problem of the state space, analysis techniques based on an exploration of the state space are often not feasible and the integration of the moments of the underlying probability distribution has become a very popular alternative. In this paper the focus is on a comparison of reconstructed distributions from their moments obtained by two different moment-based analysis methods, the method of moments (MM) and the method of conditional moments (MCM). We use the maximum entropy principle to derive a distribution that fits best to a given sequence of (conditional) moments. For the two gene regulatory networks that we consider we find that the MCM approach is more suitable to describe multimodal distributions and that the reconstruction of marginal distributions is more accurate if conditional distributions are considered.},
 bibtype = {article},
 author = {Andreychenko, Alexander and Mikeev, Linar and Wolf, Verena},
 journal = {Journal of Coupled Systems and Multiscale Dynamics},
 number = {2}
}

The stochastic dynamics of biochemical reaction networks can be accurately described by discrete-state Markov processes where each chemical reaction corresponds to a state transition of the process. Due to the largeness problem of the state space, analysis techniques based on an exploration of the state space are often not feasible and the integration of the moments of the underlying probability distribution has become a very popular alternative. In this paper the focus is on a comparison of reconstructed distributions from their moments obtained by two different moment-based analysis methods, the method of moments (MM) and the method of conditional moments (MCM). We use the maximum entropy principle to derive a distribution that fits best to a given sequence of (conditional) moments. For the two gene regulatory networks that we consider we find that the MCM approach is more suitable to describe multimodal distributions and that the reconstruction of marginal distributions is more accurate if conditional distributions are considered.

@article{
 title = {Model reconstruction for moment-based stochastic chemical kinetics},
 type = {article},
 year = {2015},
 pages = {12},
 volume = {25},
 publisher = {ACM},
 id = {5bde2a9c-28fd-38f6-9a9f-a706cf7c52c5},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {andreychenko2015model},
 source_type = {article},
 private_publication = {false},
 bibtype = {article},
 author = {Andreychenko, Alexander and Mikeev, Linar and Wolf, Verena},
 journal = {ACM Transactions on Modeling and Computer Simulation (TOMACS)},
 number = {2}
}

@inbook{
 type = {inbook},
 year = {2015},
 keywords = {Branching processes,DNA methylation,Epigenomics,Next generation sequencing,Parameter estimation},
 pages = {141-155},
 volume = {9271},
 websites = {http://link.springer.com/chapter/10.1007/978-3-319-26916-0_8},
 publisher = {Springer},
 id = {cf4bcbe7-391e-3044-965e-d5ebf68f44f7},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {bock2015model},
 source_type = {incollection},
 private_publication = {false},
 abstract = {We consider the problem of understanding how DNA methylation fidelity, i.e. the preservation of methylated sites in the genome, varies across the genome and across different cell types. Our approach uses a stochastic model of DNA methylation across generations and trains it using data obtained through next generation sequencing. By training the model locally, i.e. learning its parameters based on observations in a specific genomic region, we can compare how DNA methylation fidelity varies genome-wide. In the paper, we focus on the computational challenges to scale parameter estimation to the whole-genome level, and present two methods to achieve this goal, one based on moment-based approximation and one based on simulation. We extensively tested our methods on synthetic data and on a first batch of experimental data.},
 bibtype = {inbook},
 author = {Bock, C. and Bortolussi, L. and Krüger, T. and Mikeev, L. and Wolf, V.},
 doi = {10.1007/978-3-319-26916-0_8},
 chapter = {Model-based whole-genome analysis of dna methylation fidelity},
 title = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}
}

We consider the problem of understanding how DNA methylation fidelity, i.e. the preservation of methylated sites in the genome, varies across the genome and across different cell types. Our approach uses a stochastic model of DNA methylation across generations and trains it using data obtained through next generation sequencing. By training the model locally, i.e. learning its parameters based on observations in a specific genomic region, we can compare how DNA methylation fidelity varies genome-wide. In the paper, we focus on the computational challenges to scale parameter estimation to the whole-genome level, and present two methods to achieve this goal, one based on moment-based approximation and one based on simulation. We extensively tested our methods on synthetic data and on a first batch of experimental data.

@inproceedings{
 title = {Modeling of Resilience Properties in Oscillatory Biological Systems Using Parametric Time Petri Nets},
 type = {inproceedings},
 year = {2015},
 pages = {239-250},
 websites = {http://link.springer.com/10.1007/978-3-319-23401-4_20},
 publisher = {Springer International Publishing},
 city = {Cham},
 chapter = {Modeling o},
 id = {c38b6d06-f6e3-3c37-aebd-533c0cb7c6c3},
 created = {2016-02-15T09:28:48.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Andreychenko2015},
 source_type = {inbook},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Andreychenko, Alexander and Magnin, Morgan and Inoue, Katsumi},
 editor = {Roux, Olivier and Bourdon, Jérémie},
 doi = {10.1007/978-3-319-23401-4_20},
 booktitle = {Computational Methods in Systems Biology: 13th International Conference, CMSB 2015, Nantes, France, September 16-18, 2015, Proceedings}
}

@inproceedings{
 title = {Rule-based modelling and simulation of drug-administration policies},
 type = {inproceedings},
 year = {2015},
 pages = {53-60},
 websites = {http://delivery.acm.org/10.1145/2880000/2873012/p53-bortolussi.pdf?ip=134.96.243.197&id=2873012&acc=ACTIVE SERVICE&key=2BA2C432AB83DA15%2E751454C00E92148A%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35&CFID=528669532&CFTOKEN=13974390&__acm__=1456997720_ed4dd53fe07},
 institution = {Society for Computer Simulation International},
 id = {1d416eeb-8de8-357a-875e-f879f6f2bf9c},
 created = {2016-02-15T09:28:48.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {bortolussi2015rule},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We consider rule-based models extended with timedependent reaction rates, a suitable formalism to describe the effect of drug administration on biochemical systems. In the paper, we provide a novel and efficient rejection-based simulation algorithm that samples exactly the trajectory space of such models. Furthermore, we investigate a model of drug administration in the context of a plaque-formation process of Alzheimer’s disease, a polymerization process best described by a rule-based model to counteract the intrinsic combinatorial explosion of the underlying reaction network. Furthermore, time-dependent rates are needed to model the effect of drugs. We apply the simulation algorithm to study the efficacy of different drug administration policies.},
 bibtype = {inproceedings},
 author = {Bortolussi, Luca and Krüger, Thilo and Lehr, Thorsten and Wolf, Verena},
 booktitle = {Proceedings of the Symposium on Modeling and Simulation in Medicine}
}

We consider rule-based models extended with timedependent reaction rates, a suitable formalism to describe the effect of drug administration on biochemical systems. In the paper, we provide a novel and efficient rejection-based simulation algorithm that samples exactly the trajectory space of such models. Furthermore, we investigate a model of drug administration in the context of a plaque-formation process of Alzheimer’s disease, a polymerization process best described by a rule-based model to counteract the intrinsic combinatorial explosion of the underlying reaction network. Furthermore, time-dependent rates are needed to model the effect of drugs. We apply the simulation algorithm to study the efficacy of different drug administration policies.

@book{
 title = {Optimal observation time points in stochastic chemical kinetics},
 type = {book},
 year = {2015},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {7699},
 id = {5e5299d3-eba5-300f-8a58-be5aa479dbb1},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {© Springer International Publishing Switzerland 2015.Wet-lab experiments, in which the dynamics within living cells are observed, are usually costly and time consuming. This is particularly true if single-cell measurements are obtained using experimental techniques such as flow-cytometry or fluorescence microscopy. It is therefore important to optimize experiments with respect to the information they provide about the system. In this paper we make a priori predictions of the amount of information that can be obtained from measurements. We focus on the case where the measurements are made to estimate parameters of a stochastic model of the underlying biochemical reactions. We propose a numerical scheme to approximate the Fisher information of future experiments at different observation time points and determine optimal observation time points. To illustrate the usefulness of our approach, we apply our method to two interesting case studies.},
 bibtype = {book},
 author = {Kyriakopoulos, C. and Wolf, V.},
 doi = {10.1007/978-3-319-27656-4_5}
}

© Springer International Publishing Switzerland 2015.Wet-lab experiments, in which the dynamics within living cells are observed, are usually costly and time consuming. This is particularly true if single-cell measurements are obtained using experimental techniques such as flow-cytometry or fluorescence microscopy. It is therefore important to optimize experiments with respect to the information they provide about the system. In this paper we make a priori predictions of the amount of information that can be obtained from measurements. We focus on the case where the measurements are made to estimate parameters of a stochastic model of the underlying biochemical reactions. We propose a numerical scheme to approximate the Fisher information of future experiments at different observation time points and determine optimal observation time points. To illustrate the usefulness of our approach, we apply our method to two interesting case studies.

@inproceedings{
 title = {Optimal Observation Time Points in Stochastic Chemical Kinetics},
 type = {inproceedings},
 year = {2014},
 pages = {83-96},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-319-27656-4_5#page-1},
 publisher = {Springer},
 id = {c874410f-f8c1-3857-8254-e49c5dca15ed},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {kyriakopoulos2014optimal},
 source_type = {incollection},
 private_publication = {false},
 abstract = {Wet-lab experiments, in which the dynamics within living cells are observed, are usually costly and time consuming. This is particularly true if single-cell measurements are obtained using experimental techniques such as flow-cytometry or fluorescence microscopy. It is therefore important to optimize experiments with respect to the information they provide about the system. In this paper we make a priori predictions of the amount of information that can be obtained from measurements. We focus on the case where the measurements are made to estimate parameters of a stochastic model of the underlying biochemical reactions. We propose a numerical scheme to approximate the Fisher information of future experiments at different observation time points and determine optimal observation time points. To illustrate the usefulness of our approach, we apply our method to two interesting case studies.},
 bibtype = {inproceedings},
 author = {Kyriakopoulos, Charalampos and Wolf, Verena},
 booktitle = {Hybrid Systems Biology}
}

Wet-lab experiments, in which the dynamics within living cells are observed, are usually costly and time consuming. This is particularly true if single-cell measurements are obtained using experimental techniques such as flow-cytometry or fluorescence microscopy. It is therefore important to optimize experiments with respect to the information they provide about the system. In this paper we make a priori predictions of the amount of information that can be obtained from measurements. We focus on the case where the measurements are made to estimate parameters of a stochastic model of the underlying biochemical reactions. We propose a numerical scheme to approximate the Fisher information of future experiments at different observation time points and determine optimal observation time points. To illustrate the usefulness of our approach, we apply our method to two interesting case studies.

@inbook{
 type = {inbook},
 year = {2014},
 pages = {1-25},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-662-45489-3_1},
 publisher = {Springer},
 id = {8b909e90-f590-38ae-b57b-e40ba2b58187},
 created = {2016-02-15T09:28:48.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {andreychenko2014analyzing},
 source_type = {incollection},
 private_publication = {false},
 abstract = {An important behavioral pattern that can be witnessed in many systems is periodic re-occurrence. For example, most living organisms that we know are governed by a 24 hours rhythm that determines whether they are awake or not. On a larger scale, also whole population numbers of organisms fluctuate in a cyclic manner as in predator-prey relationships. When treating such systems in a deterministic way, i.e., assuming that stochastic effects are negligible, the analysis is a well-studied topic. But if those effects play an important role, recent publications suggest that at least a part of the system should be modeled stochastically. However, in that case, one quickly realizes that characterizing and defining oscillatory behavior is not a straightforward task, which can be solved once and for all. Moreover, efficiently checking whether a given system oscillates or not and if so determining the amplitude of the fluctuations and the time in-between is intricate. This paper shall give an overview of the existing literature on different modeling formalisms for oscillatory systems, definitions of oscillatory behavior, and the respective analysis methods.},
 bibtype = {inbook},
 author = {Andreychenko, Alexander and Krüger, Thilo and Spieler, David},
 chapter = {Analyzing Oscillatory Behavior with Formal Methods},
 title = {Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems}
}

An important behavioral pattern that can be witnessed in many systems is periodic re-occurrence. For example, most living organisms that we know are governed by a 24 hours rhythm that determines whether they are awake or not. On a larger scale, also whole population numbers of organisms fluctuate in a cyclic manner as in predator-prey relationships. When treating such systems in a deterministic way, i.e., assuming that stochastic effects are negligible, the analysis is a well-studied topic. But if those effects play an important role, recent publications suggest that at least a part of the system should be modeled stochastically. However, in that case, one quickly realizes that characterizing and defining oscillatory behavior is not a straightforward task, which can be solved once and for all. Moreover, efficiently checking whether a given system oscillates or not and if so determining the amplitude of the fluctuations and the time in-between is intricate. This paper shall give an overview of the existing literature on different modeling formalisms for oscillatory systems, definitions of oscillatory behavior, and the respective analysis methods.

@inproceedings{
 title = {Model checking CSL for markov population models},
 type = {inproceedings},
 year = {2014},
 websites = {http://arxiv.org/pdf/1111.4385.pdf},
 publisher = {EPTCS},
 id = {cb180e1f-fa90-33bf-b2d0-1e2185c11756},
 created = {2016-03-03T09:50:01.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {spieler2011model},
 source_type = {article},
 private_publication = {false},
 abstract = {Markov population models (MPMs) are a widely used modelling formalism in the area of computational biology and related areas. The semantics of a MPM is an infinite-state continuous-time Markov chain. In this paper, we use the established continuous stochastic logic (CSL) to express properties of Markov population models. This allows us to express important measures of biological systems, such as probabilistic reachability, survivability, oscillations, switching times between attractor regions, and various others. Because of the infinite state space, available analysis techniques only apply to a very restricted subset of CSL properties. We present a full algorithm for model checking CSL for MPMs, and provide experimental evidence showing that our method is effective.},
 bibtype = {inproceedings},
 author = {Spieler, David and Hahn, Ernst Moritz and Zhang, Lijun},
 booktitle = {QAPL'14}
}

Markov population models (MPMs) are a widely used modelling formalism in the area of computational biology and related areas. The semantics of a MPM is an infinite-state continuous-time Markov chain. In this paper, we use the established continuous stochastic logic (CSL) to express properties of Markov population models. This allows us to express important measures of biological systems, such as probabilistic reachability, survivability, oscillations, switching times between attractor regions, and various others. Because of the infinite state space, available analysis techniques only apply to a very restricted subset of CSL properties. We present a full algorithm for model checking CSL for MPMs, and provide experimental evidence showing that our method is effective.

@inproceedings{
 title = {Numerical Approximation of Rare Event Probabilities in Biochemically Reacting Systems},
 type = {inproceedings},
 year = {2013},
 pages = {5-18},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-642-40708-6_2},
 institution = {Springer},
 id = {acdcb834-039a-36d0-b82e-86b5f64b89b8},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {mikeev2013numerical},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {In stochastic biochemically reacting systems, certain rare events can cause serious consequences, which makes their probabilities important to analyze. We solve the chemical master equation using a four-stage fourth order Runge-Kutta integration scheme in combination with a guided state space exploration and a dynamical state space truncation in order to approximate the unknown probabilities of rare but important events numerically. The guided state space exploration biases the system parameters such that the rare event of interest becomes less rare. For each numerical integration step, the portion of the state space to be truncated is then dynamically obtained using information from the biased model and the numerical integration of the unbiased model is conducted only on the remaining significant part of the state space. The efficiency and the accuracy of our method are studied through a benchmark model that recently received considerable attention in the literature.},
 bibtype = {inproceedings},
 author = {Mikeev, Linar and Sandmann, Werner and Wolf, Verena},
 booktitle = {Computational Methods in Systems Biology}
}

In stochastic biochemically reacting systems, certain rare events can cause serious consequences, which makes their probabilities important to analyze. We solve the chemical master equation using a four-stage fourth order Runge-Kutta integration scheme in combination with a guided state space exploration and a dynamical state space truncation in order to approximate the unknown probabilities of rare but important events numerically. The guided state space exploration biases the system parameters such that the rare event of interest becomes less rare. For each numerical integration step, the portion of the state space to be truncated is then dynamically obtained using information from the biased model and the numerical integration of the unbiased model is conducted only on the remaining significant part of the state space. The efficiency and the accuracy of our method are studied through a benchmark model that recently received considerable attention in the literature.

@inproceedings{
 title = {Approximate transient analysis of queueing networks by quasi product forms},
 type = {inproceedings},
 year = {2013},
 keywords = {to appear},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-642-39408-9_3#page-1},
 publisher = {Springer},
 series = {Lecture Notes of Computer Science},
 id = {c6690674-a2b5-3a63-aefe-68a5b368a6d0},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {AsmtaQPF},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {In this paper we deal with transient analysis of networks of queues. These systems most often have enormous state space and the exact computation of their transient behavior is not possible. We propose to apply an approximate technique based on assumptions on the structure of the transient probabilities. In particular, we assume that the transient probabilities of the model can be decomposed into a quasi product form. This assumption simplifies the dependency structure of the model and leads to a relatively small set of ordinary differential equations (ODE) that can be used to compute an approximation of the transient probabilities. We provide the derivation of this set of ODEs and illustrate the accuracy of the approach on numerical examples.},
 bibtype = {inproceedings},
 author = {Angius, Alessio and Horvath, Andras and Wolf, Verena},
 booktitle = {Proceedings of the 20th International Conference on Analytic and Stochastic Modelling Techniques and Applications (ASMTA'13)}
}

In this paper we deal with transient analysis of networks of queues. These systems most often have enormous state space and the exact computation of their transient behavior is not possible. We propose to apply an approximate technique based on assumptions on the structure of the transient probabilities. In particular, we assume that the transient probabilities of the model can be decomposed into a quasi product form. This assumption simplifies the dependency structure of the model and leads to a relatively small set of ordinary differential equations (ODE) that can be used to compute an approximation of the transient probabilities. We provide the derivation of this set of ODEs and illustrate the accuracy of the approach on numerical examples.

@inproceedings{
 title = {Efficient Steady State Analysis of Multimodal Markov Chains},
 type = {inproceedings},
 year = {2013},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-642-39408-9_27#page-1},
 publisher = {Springer},
 series = {Lecture Notes of Computer Science},
 id = {c4c97752-f04b-33a5-a109-171bd25a7a70},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {AsmtaSS},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We consider the problem of computing the steady state distribution of Markov chains describing cellular processes. Our main contribution is a numerical algorithm that approximates the steady state distribution in the presence of multiple modes. This method tackles two problems that occur during the analysis of systems with multimodal distributions: stiffness preventing fast convergence of iterative methods and largeness of the state space leading to excessive memory requirements and prohibiting direct solutions. We use drift arguments to locate the relevant parts of the state space, that is, parts containing 1 − ε of the steady state probability. In order to separate the widely varying time scales of the model we apply stochastic complementation techniques. The memory requirements of our method are low because we exploit accurate approximations based on inexact matrix vector multiplications. We test the performance of our method on two challenging examples from biology.},
 bibtype = {inproceedings},
 author = {Spieler, David and Wolf, Verena},
 booktitle = {Proceedings of the 20th International Conference on Analytic and Stochastic Modelling Techniques and Applications (ASMTA'13)}
}

We consider the problem of computing the steady state distribution of Markov chains describing cellular processes. Our main contribution is a numerical algorithm that approximates the steady state distribution in the presence of multiple modes. This method tackles two problems that occur during the analysis of systems with multimodal distributions: stiffness preventing fast convergence of iterative methods and largeness of the state space leading to excessive memory requirements and prohibiting direct solutions. We use drift arguments to locate the relevant parts of the state space, that is, parts containing 1 − ε of the steady state probability. In order to separate the widely varying time scales of the model we apply stochastic complementation techniques. The memory requirements of our method are low because we exploit accurate approximations based on inexact matrix vector multiplications. We test the performance of our method on two challenging examples from biology.

@article{
 title = {Method of conditional moments (MCM) for the Chemical Master Equation},
 type = {article},
 year = {2013},
 pages = {687-735},
 volume = {69},
 websites = {http://link.springer.com/article/10.1007%2Fs00285-013-0711-5#/page-1},
 id = {8546a88d-b85c-3157-b392-ebf53beaa06d},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Hasenauer2013},
 source_type = {article},
 private_publication = {false},
 abstract = {The time-evolution of continuous-time discrete-state biochemical processes is governed by the Chemical Master Equation (CME), which describes the probability of the molecular counts of each chemical species. As the corresponding number of discrete states is, for most processes, large, a direct numerical simulation of the CME is in general infeasible. In this paper we introduce the method of conditional moments (MCM), a novel approximation method for the solution of the CME. The MCM employs a discrete stochastic description for low-copy number species and a moment-based description for medium/high-copy number species. The moments of the medium/high-copy number species are conditioned on the state of the low abundance species, which allows us to capture complex correlation structures arising, e.g., for multi-attractor and oscillatory systems. We prove that the MCM provides a generalization of previous approximations of the CME based on hybrid modeling and moment-based methods. Furthermore, it improves upon these existing methods, as we illustrate using a model for the dynamics of stochastic single-gene expression. This application example shows that due to the more general structure, the MCM allows for the approximation of multi-modal distributions.},
 bibtype = {article},
 author = {Hasenauer, J and Wolf, V and Kazeroonian, A and Theis, F J},
 doi = {10.1007/s00285-013-0711-5},
 journal = {Journal of Mathematical Biology},
 number = {3}
}

The time-evolution of continuous-time discrete-state biochemical processes is governed by the Chemical Master Equation (CME), which describes the probability of the molecular counts of each chemical species. As the corresponding number of discrete states is, for most processes, large, a direct numerical simulation of the CME is in general infeasible. In this paper we introduce the method of conditional moments (MCM), a novel approximation method for the solution of the CME. The MCM employs a discrete stochastic description for low-copy number species and a moment-based description for medium/high-copy number species. The moments of the medium/high-copy number species are conditioned on the state of the low abundance species, which allows us to capture complex correlation structures arising, e.g., for multi-attractor and oscillatory systems. We prove that the MCM provides a generalization of previous approximations of the CME based on hybrid modeling and moment-based methods. Furthermore, it improves upon these existing methods, as we illustrate using a model for the dynamics of stochastic single-gene expression. This application example shows that due to the more general structure, the MCM allows for the approximation of multi-modal distributions.

@inbook{
 type = {inbook},
 year = {2013},
 pages = {106-122},
 websites = {http://link.springer.com/chapter/10.1007/978-3-642-40196-1_8#page-1},
 publisher = {Springer},
 id = {f07ee825-e966-3fbd-807c-fcb2a76102a0},
 created = {2016-03-03T09:50:01.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {spieler2013characterizing},
 source_type = {incollection},
 private_publication = {false},
 abstract = {In systems biology, an interesting problem is to analyze and characterize the oscillatory and periodic behavior of a chemical reaction system. Traditionally, those systems have been treated deterministically and continuously via ordinary differential equations. In case of high molecule counts with respect to the volume this treatment is justified. But otherwise, stochastic fluctuations can have a high influence on the characteristics of a system as has been shown in recent publications. In this paper we develop an efficient numerical approach for analyzing the oscillatory and periodic character of user-defined observations on Markov population models (MPMs). MPMs are a special kind of continuous-time Markov chains that allow for a discrete representation of unbounded population counts for several population types and transformations between populations. Examples are chemical species and the reactions between them.},
 bibtype = {inbook},
 author = {Spieler, David},
 chapter = {Characterizing oscillatory and noisy periodic behavior in markov population models},
 title = {Quantitative Evaluation of Systems}
}

In systems biology, an interesting problem is to analyze and characterize the oscillatory and periodic behavior of a chemical reaction system. Traditionally, those systems have been treated deterministically and continuously via ordinary differential equations. In case of high molecule counts with respect to the volume this treatment is justified. But otherwise, stochastic fluctuations can have a high influence on the characteristics of a system as has been shown in recent publications. In this paper we develop an efficient numerical approach for analyzing the oscillatory and periodic character of user-defined observations on Markov population models (MPMs). MPMs are a special kind of continuous-time Markov chains that allow for a discrete representation of unbounded population counts for several population types and transformations between populations. Examples are chemical species and the reactions between them.

@book{
 title = {Efficient steady state analysis of multimodal Markov chains},
 type = {book},
 year = {2013},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {7984 LNCS},
 id = {180a5e9f-8947-38d2-b837-b51e73078bb2},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We consider the problem of computing the steady state distribution of Markov chains describing cellular processes. Our main contribution is a numerical algorithm that approximates the steady state distribution in the presence of multiple modes. This method tackles two problems that occur during the analysis of systems with multimodal distributions: stiffness preventing fast convergence of iterative methods and largeness of the state space leading to excessive memory requirements and prohibiting direct solutions. We use drift arguments to locate the relevant parts of the state space, that is, parts containing 1 - ε of the steady state probability. In order to separate the widely varying time scales of the model we apply stochastic complementation techniques. The memory requirements of our method are low because we exploit accurate approximations based on inexact matrix vector multiplications. We test the performance of our method on two challenging examples from biology. © 2013 Springer-Verlag.},
 bibtype = {book},
 author = {Spieler, D. and Wolf, V.},
 doi = {10.1007/978-3-642-39408-9_27}
}

We consider the problem of computing the steady state distribution of Markov chains describing cellular processes. Our main contribution is a numerical algorithm that approximates the steady state distribution in the presence of multiple modes. This method tackles two problems that occur during the analysis of systems with multimodal distributions: stiffness preventing fast convergence of iterative methods and largeness of the state space leading to excessive memory requirements and prohibiting direct solutions. We use drift arguments to locate the relevant parts of the state space, that is, parts containing 1 - ε of the steady state probability. In order to separate the widely varying time scales of the model we apply stochastic complementation techniques. The memory requirements of our method are low because we exploit accurate approximations based on inexact matrix vector multiplications. We test the performance of our method on two challenging examples from biology. © 2013 Springer-Verlag.

@article{
 title = {On-the-fly verification and optimization of DTA-properties for large Markov chains},
 type = {article},
 year = {2013},
 keywords = {[Continuous-time Markov chains, Deterministic time},
 volume = {43},
 id = {85c6c212-8683-3ff8-9a2e-0f1162032fde},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies. © 2012 Springer Science+Business Media, LLC.},
 bibtype = {article},
 author = {Mikeev, L. and Neuhäußer, M.R. and Spieler, D. and Wolf, V.},
 doi = {10.1007/s10703-012-0165-1},
 journal = {Formal Methods in System Design},
 number = {2}
}

We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies. © 2012 Springer Science+Business Media, LLC.

@book{
 title = {Numerical approximation of rare event probabilities in biochemically reacting systems},
 type = {book},
 year = {2013},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 keywords = {[Biochemically reacting systems, Chemical master e},
 volume = {8130 LNBI},
 id = {ff4edda8-5857-36c2-85a3-1a74b1875515},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {In stochastic biochemically reacting systems, certain rare events can cause serious consequences, which makes their probabilities important to analyze. We solve the chemical master equation using a four-stage fourth order Runge-Kutta integration scheme in combination with a guided state space exploration and a dynamical state space truncation in order to approximate the unknown probabilities of rare but important events numerically. The guided state space exploration biases the system parameters such that the rare event of interest becomes less rare. For each numerical integration step, the portion of the state space to be truncated is then dynamically obtained using information from the biased model and the numerical integration of the unbiased model is conducted only on the remaining significant part of the state space. The efficiency and the accuracy of our method are studied through a benchmark model that recently received considerable attention in the literature. © Springer-Verlag 2013.},
 bibtype = {book},
 author = {Mikeev, L. and Sandmann, W. and Wolf, V.},
 doi = {10.1007/978-3-642-40708-6_2}
}

In stochastic biochemically reacting systems, certain rare events can cause serious consequences, which makes their probabilities important to analyze. We solve the chemical master equation using a four-stage fourth order Runge-Kutta integration scheme in combination with a guided state space exploration and a dynamical state space truncation in order to approximate the unknown probabilities of rare but important events numerically. The guided state space exploration biases the system parameters such that the rare event of interest becomes less rare. For each numerical integration step, the portion of the state space to be truncated is then dynamically obtained using information from the biased model and the numerical integration of the unbiased model is conducted only on the remaining significant part of the state space. The efficiency and the accuracy of our method are studied through a benchmark model that recently received considerable attention in the literature. © Springer-Verlag 2013.

@article{
 title = {In vivo control of CpG and non-CpG DNA methylation by DNA methyltransferases},
 type = {article},
 year = {2012},
 volume = {8},
 websites = {http://www.plosgenetics.org/article/info%3Adoi%2F10.1371%2Fjournal.pgen.1002750},
 id = {6008ea05-ffdc-3941-b408-2efc86d7aefc},
 created = {2016-02-15T08:58:12.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {The enzymatic control of the setting and maintenance of symmetric and non-symmetric DNA methylation patterns in a particular genome context is not well understood. Here, we describe a comprehensive analysis of DNA methylation patterns generated by high resolution sequencing of hairpin-bisulfite amplicons of selected single copy genes and repetitive elements (LINE1, B1, IAP-LTR-retrotransposons, and major satellites). The analysis unambiguously identifies a substantial amount of regional incomplete methylation maintenance, i.e. hemimethylated CpG positions, with variant degrees among cell types. Moreover, non-CpG cytosine methylation is confined to ESCs and exclusively catalysed by Dnmt3a and Dnmt3b. This sequence position-, cell type-, and region-dependent non-CpG methylation is strongly linked to neighboring CpG methylation and requires the presence of Dnmt3L. The generation of a comprehensive data set of 146,000 CpG dyads was used to apply and develop parameter estimated hidden Markov models (HMM) to calculate the relative contribution of DNA methyltransferases (Dnmts) for de novo and maintenance DNA methylation. The comparative modelling included wild-type ESCs and mutant ESCs deficient for Dnmt1, Dnmt3a, Dnmt3b, or Dnmt3a/3b, respectively. The HMM analysis identifies a considerable de novo methylation activity for Dnmt1 at certain repetitive elements and single copy sequences. Dnmt3a and Dnmt3b contribute de novo function. However, both enzymes are also essential to maintain symmetrical CpG methylation at distinct repetitive and single copy sequences in ESCs.},
 bibtype = {article},
 author = {Arand, Julia and Spieler, David and Karius, Tommy and Branco, Miguel R. and Meilinger, Daniela and Meissner, Alexander and Jenuwein, Thomas and Xu, Guoliang and Leonhardt, Heinrich and Wolf, Verena and Walter, Jörn},
 journal = {PLoS Genetics},
 number = {6}
}

The enzymatic control of the setting and maintenance of symmetric and non-symmetric DNA methylation patterns in a particular genome context is not well understood. Here, we describe a comprehensive analysis of DNA methylation patterns generated by high resolution sequencing of hairpin-bisulfite amplicons of selected single copy genes and repetitive elements (LINE1, B1, IAP-LTR-retrotransposons, and major satellites). The analysis unambiguously identifies a substantial amount of regional incomplete methylation maintenance, i.e. hemimethylated CpG positions, with variant degrees among cell types. Moreover, non-CpG cytosine methylation is confined to ESCs and exclusively catalysed by Dnmt3a and Dnmt3b. This sequence position-, cell type-, and region-dependent non-CpG methylation is strongly linked to neighboring CpG methylation and requires the presence of Dnmt3L. The generation of a comprehensive data set of 146,000 CpG dyads was used to apply and develop parameter estimated hidden Markov models (HMM) to calculate the relative contribution of DNA methyltransferases (Dnmts) for de novo and maintenance DNA methylation. The comparative modelling included wild-type ESCs and mutant ESCs deficient for Dnmt1, Dnmt3a, Dnmt3b, or Dnmt3a/3b, respectively. The HMM analysis identifies a considerable de novo methylation activity for Dnmt1 at certain repetitive elements and single copy sequences. Dnmt3a and Dnmt3b contribute de novo function. However, both enzymes are also essential to maintain symmetrical CpG methylation at distinct repetitive and single copy sequences in ESCs.

@article{
 title = {Approximate maximum likelihood estimation for stochastic chemical kinetics},
 type = {article},
 year = {2012},
 volume = {9},
 websites = {http://bsb.eurasipjournals.com/content/2012/1/9/abstract},
 id = {c64e55c0-e130-3104-8fd3-8b01ad84943b},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {MLEJournal},
 source_type = {article},
 private_publication = {false},
 abstract = {Recent experimental imaging techniques are able to tag and count molecular populations in a living cell. From these data mathematical models are inferred and calibrated. If small populations are present, discrete-state stochastic models are widely-used to describe the discreteness and randomness of molecular interactions. Based on time-series data of the molecular populations, the corresponding stochastic reaction rate constants can be estimated. This procedure is computationally very challenging, since the underlying stochastic process has to be solved for different parameters in order to obtain optimal estimates. Here, we focus on the maximum likelihood method and estimate rate constants, initial populations and parameters representing measurement errors.},
 bibtype = {article},
 author = {Andreychenko, Aleksandr and Mikeev, Linar and Spieler, David and Wolf, Verena},
 journal = {EURASIP Journal on Bioinformatics and Systems Biology}
}

Recent experimental imaging techniques are able to tag and count molecular populations in a living cell. From these data mathematical models are inferred and calibrated. If small populations are present, discrete-state stochastic models are widely-used to describe the discreteness and randomness of molecular interactions. Based on time-series data of the molecular populations, the corresponding stochastic reaction rate constants can be estimated. This procedure is computationally very challenging, since the underlying stochastic process has to be solved for different parameters in order to obtain optimal estimates. Here, we focus on the maximum likelihood method and estimate rate constants, initial populations and parameters representing measurement errors.

@article{
 title = {On-the-fly Verification and Optimization of DTA-properties for Large Markov Chains.},
 type = {article},
 year = {2012},
 pages = {1-25},
 websites = {http://link.springer.com/article/10.1007%2Fs10703-012-0165-1},
 id = {d403b8b9-1887-3d75-9114-c5d9687b7c5d},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {dtapaper},
 source_type = {article},
 private_publication = {false},
 abstract = {We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies.},
 bibtype = {article},
 author = {Mikeev, Linar and Neuhäußer, Martin and Spieler, David and Wolf, Verena},
 journal = {Formal Methods in System Design}
}

We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies.

@article{
 title = {Three-Valued Abstraction for Probabilistic Systems.},
 type = {article},
 year = {2012},
 pages = {356-389},
 volume = {81},
 websites = {http://www.sciencedirect.com/science/article/pii/S1567832612000239},
 id = {d39cfdd9-123b-304d-995b-cccdf6e7ed3b},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {KaKlLeWo_12:CV},
 source_type = {article},
 private_publication = {false},
 abstract = {This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs.},
 bibtype = {article},
 author = {Katoen, J.-P. and Klink, D and Leucker, M and Wolf, V},
 journal = {Journal on Logic and Algebraic Programming},
 number = {4}
}

This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs.

@inproceedings{
 title = {Parameter Estimation for Stochastic Hybrid Models of Biochemical Reaction Networks},
 type = {inproceedings},
 year = {2012},
 websites = {http://dl.acm.org/citation.cfm?id=2185657},
 series = {ACM International Conference Proceeding Series},
 id = {a67c57a5-3d1f-3421-a10c-a822895831c8},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {hscc12},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {The dynamics of biochemical reaction networks can be accurately described by stochastic hybrid models, where we assume that large chemical populations evolve deterministically and continuously over time while small populations change through random discrete reactions. We propose an algorithm for estimating the parameters of a given biochemical reaction network based on a stochastic hybrid model. We assume that noisy time series measurements of the chemical populations are available and follow a maximum likelihood approach to calibrate the parameters. We numerically approximate the likelihood and its derivatives for concrete values of the parameters and show that, based on this approximation, the maximization of the likelihood can be done efficiently. We substantiate the usefulness of our approach by applying it to several case studies from systems biology.},
 bibtype = {inproceedings},
 author = {Mikeev, Linar and Wolf, Verena},
 booktitle = {Proceedings of the 15th International Conference on Hybrid Systems: Computation and Control (HSCC'12)}
}

The dynamics of biochemical reaction networks can be accurately described by stochastic hybrid models, where we assume that large chemical populations evolve deterministically and continuously over time while small populations change through random discrete reactions. We propose an algorithm for estimating the parameters of a given biochemical reaction network based on a stochastic hybrid model. We assume that noisy time series measurements of the chemical populations are available and follow a maximum likelihood approach to calibrate the parameters. We numerically approximate the likelihood and its derivatives for concrete values of the parameters and show that, based on this approximation, the maximization of the likelihood can be done efficiently. We substantiate the usefulness of our approach by applying it to several case studies from systems biology.

@inproceedings{
 title = {Parameter estimation for stochastic hybrid models of biochemical reaction networks},
 type = {inproceedings},
 year = {2012},
 keywords = {[Biochemical reactions, Parameter identification,},
 id = {36bc46d5-f3ac-37d0-8543-7c1b37f42dc4},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {The dynamics of biochemical reaction networks can be accurately described by stochastic hybrid models, where we assume that large chemical populations evolve deterministically and continuously over time while small populations change through random discrete reactions. We propose an algorithm for estimating the parameters of a given biochemical reaction network based on a stochastic hybrid model. We assume that noisy time series measurements of the chemical populations are available and follow a maximum likelihood approach to calibrate the parameters. We numerically approximate the likelihood and its derivatives for concrete values of the parameters and show that, based on this approximation, the maximization of the likelihood can be done efficiently. We substantiate the usefulness of our approach by applying it to several case studies from systems biology. Copyright 2012 ACM.},
 bibtype = {inproceedings},
 author = {Mikeev, L. and Wolf, V.},
 doi = {10.1145/2185632.2185657},
 booktitle = {HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control}
}

The dynamics of biochemical reaction networks can be accurately described by stochastic hybrid models, where we assume that large chemical populations evolve deterministically and continuously over time while small populations change through random discrete reactions. We propose an algorithm for estimating the parameters of a given biochemical reaction network based on a stochastic hybrid model. We assume that noisy time series measurements of the chemical populations are available and follow a maximum likelihood approach to calibrate the parameters. We numerically approximate the likelihood and its derivatives for concrete values of the parameters and show that, based on this approximation, the maximization of the likelihood can be done efficiently. We substantiate the usefulness of our approach by applying it to several case studies from systems biology. Copyright 2012 ACM.

@article{
 title = {Three-valued abstraction for probabilistic systems},
 type = {article},
 year = {2012},
 volume = {81},
 id = {eba1888c-f7dc-3ecf-8674-1548423fe610},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs. © 2012 Elsevier Inc. All rights reserved.},
 bibtype = {article},
 author = {Katoen, J.-P. and Klink, D. and Leucker, M. and Wolf, V.},
 doi = {10.1016/j.jlap.2012.03.007},
 journal = {Journal of Logic and Algebraic Programming},
 number = {4}
}

This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs. © 2012 Elsevier Inc. All rights reserved.

@book{
 title = {Quasi product form approximation for markov models of reaction networks},
 type = {book},
 year = {2012},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {7625 LNBI},
 id = {dc335fa1-37e2-3751-a2f8-80c90cec8842},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {In cell processes, such as gene regulation or cell differentiation, stochasticity often plays a crucial role. Quantitative analysis of stochastic models of the underlying chemical reaction network can be obstructed by the size of the state space which grows exponentially with the number of considered species. In a recent paper [1] we showed that the space complexity of the analysis can be drastically decreased by assuming that the transient probabilities of the model are in product form. This assumption, however, leads to approximations that are satisfactory only for a limited range of models. In this paper we relax the product form assumption by introducing the quasi product form assumption. This leads to an algorithm whose memory complexity is still reasonably low and provides a good approximation of the transient probabilities for a wide range of models. We discuss the characteristics of this algorithm and illustrate its application on several reaction networks. © 2012 Springer-Verlag.},
 bibtype = {book},
 author = {Angius, A. and Horváth, A. and Wolf, V.},
 doi = {10.1007/978-3-642-35524-0_2}
}

In cell processes, such as gene regulation or cell differentiation, stochasticity often plays a crucial role. Quantitative analysis of stochastic models of the underlying chemical reaction network can be obstructed by the size of the state space which grows exponentially with the number of considered species. In a recent paper [1] we showed that the space complexity of the analysis can be drastically decreased by assuming that the transient probabilities of the model are in product form. This assumption, however, leads to approximations that are satisfactory only for a limited range of models. In this paper we relax the product form assumption by introducing the quasi product form assumption. This leads to an algorithm whose memory complexity is still reasonably low and provides a good approximation of the transient probabilities for a wide range of models. We discuss the characteristics of this algorithm and illustrate its application on several reaction networks. © 2012 Springer-Verlag.

@article{
 title = {Infinite Level-Dependent QBDs and Matrix Analytic Solutions for Stochastic Chemical Kinetics},
 type = {article},
 year = {2011},
 volume = {43},
 websites = {http://projecteuclid.org/euclid.aap/1324045696},
 id = {c015eb1b-1f53-38cb-be66-aabb8fffa271},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Advances},
 source_type = {article},
 private_publication = {false},
 abstract = {Systems of stochastic chemical kinetics are modeled as infinite level-dependent quasi-birth-and-death (LDQBD) processes. For these systems, in contrast to many other applications, levels have an increasing number of states as the level number increases and the probability mass may reside arbitrarily far away from lower levels. Ideas from Lyapunov theory are combined with existing matrix-analytic formulations to obtain accurate approximations to the stationary probability distribution when the infinite LDQBD process is ergodic. Results of numerical experiments on a set of problems are provided.},
 bibtype = {article},
 author = {Dayar, T and Sandmann, W and Spieler, D and Wolf, V},
 journal = {Advances in Applied Probability},
 number = {4}
}

Systems of stochastic chemical kinetics are modeled as infinite level-dependent quasi-birth-and-death (LDQBD) processes. For these systems, in contrast to many other applications, levels have an increasing number of states as the level number increases and the probability mass may reside arbitrarily far away from lower levels. Ideas from Lyapunov theory are combined with existing matrix-analytic formulations to obtain accurate approximations to the stationary probability distribution when the infinite LDQBD process is ergodic. Results of numerical experiments on a set of problems are provided.

@article{
 title = {Approximation of Event Probabilities in Noisy Cellular Processes},
 type = {article},
 year = {2011},
 pages = {2128-2141},
 volume = {412},
 publisher = {Elsevier},
 id = {046c20d6-4d98-3979-9edf-a8492a868fa0},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {TCSapprox},
 source_type = {article},
 private_publication = {false},
 bibtype = {article},
 author = {Didier, Frédéric and Henzinger, Thomas A and Mateescu, Maria and Wolf, Verena},
 journal = {Journal of Theoretical Computer Science},
 number = {21}
}

@inproceedings{
 title = {On-the-fly Uniformization of Time-Inhomogeneous Infinite Markov Population Models},
 type = {inproceedings},
 year = {2011},
 websites = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?QAPL2011.1.pdf},
 series = {Electronic Proceedings in Theoretical Computer Science},
 id = {ca7e6a3f-16e7-3a49-9659-e381807f3e14},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {qapl11},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {This paper presents an on-the-fly uniformization technique for the analysis of time-inhomogeneous Markov population models. This technique is applicable to models with infinite state spaces and unbounded rates, which are, for instance, encountered in the realm of biochemical reaction networks. To deal with the infinite state space, we dynamically maintain a finite subset of the states where most of the probability mass is located. This approach yields an under-approximation of the original, infinite system. We present experimental results to show the applicability of our technique.},
 bibtype = {inproceedings},
 author = {Andreychenko, Aleksandr and Crouzen, Pepijn and Wolf, Verena},
 booktitle = {Proceedings of the 9th International Workshop on Quantitative Aspects of Programming Languages (QAPL'11)}
}

This paper presents an on-the-fly uniformization technique for the analysis of time-inhomogeneous Markov population models. This technique is applicable to models with infinite state spaces and unbounded rates, which are, for instance, encountered in the realm of biochemical reaction networks. To deal with the infinite state space, we dynamically maintain a finite subset of the states where most of the probability mass is located. This approach yields an under-approximation of the original, infinite system. We present experimental results to show the applicability of our technique.

@article{
 title = {Formalisms for Specifying Markovian Population Models},
 type = {article},
 year = {2011},
 volume = {22},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-642-04420-5_2},
 publisher = {World Scientific Publishing},
 id = {dccd2249-10d7-3b54-8fbf-e3ccf80b0cb6},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {TSpaperJournal},
 source_type = {article},
 private_publication = {false},
 abstract = {We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages —matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models— all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model.},
 bibtype = {article},
 author = {Henzinger, Thomas A and Jobstmann, Barbara and Wolf, Verena},
 journal = {Journal of Foundations of Computer Science},
 number = {4}
}

We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages —matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models— all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model.

@inproceedings{
 title = {Efficient Calculation of Rare Event Probabilities in Markovian Queueing Networks},
 type = {inproceedings},
 year = {2011},
 websites = {http://dl.acm.org/citation.cfm?id=2151710},
 series = {ACM International Conference Proceeding Series},
 id = {d4b9e4a7-cfce-391a-97e5-8874eed7550c},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {valuetools11},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We address the computation of rare event probabilities in Markovian queueing networks with huge or possibly even infinite state spaces. For this purpose, we incorporate ideas from importance sampling simulations into a non-simulative numerical method that approximates transient probabilities based on a dynamical truncation of the state space. A change of measure technique is applied in order to accomplish a guided state space exploration. Numerical results for three different example networks demonstrate the efficiency and accuracy of our method.},
 bibtype = {inproceedings},
 author = {Mikeev, Linar and Sandmann, Werner and Wolf, Verena},
 booktitle = {Proceedings of the 5th International ICST Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'11)}
}

We address the computation of rare event probabilities in Markovian queueing networks with huge or possibly even infinite state spaces. For this purpose, we incorporate ideas from importance sampling simulations into a non-simulative numerical method that approximates transient probabilities based on a dynamical truncation of the state space. A change of measure technique is applied in order to accomplish a guided state space exploration. Numerical results for three different example networks demonstrate the efficiency and accuracy of our method.

@inproceedings{
 title = {Parameter Identification for Markov Models of Biochemical Reactions},
 type = {inproceedings},
 year = {2011},
 pages = {83-98},
 volume = {6806},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-642-22110-1_8},
 publisher = {Springer},
 series = {Lecture Notes of Computer Science},
 id = {de401bd4-5f4f-380d-aaa1-90bbc95b0a09},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {CAV11},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We propose a numerical technique for parameter inference in Markov models of biological processes. Based on time-series data of a process we estimate the kinetic rate constants by maximizing the likelihood of the data. The computation of the likelihood relies on a dynamic abstraction of the discrete state space of the Markov model which successfully mitigates the problem of state space largeness. We compare two variants of our method to state-of-the-art, recently published methods and demonstrate their usefulness and efficiency on several case studies from systems biology.},
 bibtype = {inproceedings},
 author = {Andreychenko, Aleksandr and Mikeev, Linar and Spieler, David and Wolf, Verena},
 booktitle = {Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11)}
}

We propose a numerical technique for parameter inference in Markov models of biological processes. Based on time-series data of a process we estimate the kinetic rate constants by maximizing the likelihood of the data. The computation of the likelihood relies on a dynamic abstraction of the discrete state space of the Markov model which successfully mitigates the problem of state space largeness. We compare two variants of our method to state-of-the-art, recently published methods and demonstrate their usefulness and efficiency on several case studies from systems biology.

@article{
 title = {Bounding the Equilibrium Distribution of Markov Population Models.},
 type = {article},
 year = {2011},
 pages = {931-946},
 volume = {18},
 websites = {http://onlinelibrary.wiley.com/doi/10.1002/nla.795/abstract},
 id = {3244e72c-8791-343f-b3a6-9a8b9d032759},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {NLAA},
 source_type = {article},
 private_publication = {false},
 abstract = {We propose a bounding technique for the equilibrium probability distribution of continuous-time Markov chains with population structure and infinite state space. We use Lyapunov functions to determine a finite set of states that contains most of the equilibrium probability mass. Then we apply a refinement scheme based on stochastic complementation to derive lower and upper bounds on the equilibrium probability for each state within that set. To show the usefulness of our approach, we present experimental results for several examples from biology.},
 bibtype = {article},
 author = {Dayar, T and Hermanns, H and Spieler, D and Wolf, V},
 journal = {Numerical Linear Algebra with Applications},
 number = {6}
}

We propose a bounding technique for the equilibrium probability distribution of continuous-time Markov chains with population structure and infinite state space. We use Lyapunov functions to determine a finite set of states that contains most of the equilibrium probability mass. Then we apply a refinement scheme based on stochastic complementation to derive lower and upper bounds on the equilibrium probability for each state within that set. To show the usefulness of our approach, we present experimental results for several examples from biology.

@inproceedings{
 title = {SHAVE -- Stochastic Hybrid Analysis of Markov Population Models},
 type = {inproceedings},
 year = {2011},
 websites = {http://dl.acm.org/citation.cfm?id=1967746&dl=ACM&coll=DL&CFID=528669532&CFTOKEN=13974390},
 series = {ACM International Conference Proceeding Series},
 id = {9f4fc243-44b0-38c1-9b04-1177dddef983},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {hscc11},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We present a tool called SHAVE that approximates the transient distribution of a continuous-time Markov population process by combining moment-based and state-based representations of probability distributions. As an intermediate step, SHAVE constructs a stochastic hybrid model from the original process which is then solved numerically.},
 bibtype = {inproceedings},
 author = {Lapin, Maksim and Mikeev, Linar and Wolf, Verena},
 booktitle = {Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC'11)}
}

We present a tool called SHAVE that approximates the transient distribution of a continuous-time Markov population process by combining moment-based and state-based representations of probability distributions. As an intermediate step, SHAVE constructs a stochastic hybrid model from the original process which is then solved numerically.

@article{
 title = {Infinite level-dependent QBD processes and matrix-analytic solutions for stochastic chemical kinetics},
 type = {article},
 year = {2011},
 keywords = {[Level-dependent quasi-birth-and-death process, Ly},
 volume = {43},
 id = {77c57591-d97e-3fbb-88e4-bd971a39f69e},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Systems of stochastic chemical kinetics are modeled as infinite level-dependent quasibirth-and-death (LDQBD) processes. For these systems, in contrast to many other applications, levels have an increasing number of states as the level number increases and the probability mass may reside arbitrarily far away from lower levels. Ideas from Lyapunov theory are combined with existing matrix-analytic formulations to obtain accurate approximations to the stationary probability distribution when the infinite LDQBD process is ergodic. Results of numerical experiments on a set of problems are provided. © Applied Probability Trust 2011.},
 bibtype = {article},
 author = {Dayar, T. and Sandmann, W. and Spieler, D. and Wolf, V.},
 doi = {10.1239/aap/1324045696},
 journal = {Advances in Applied Probability},
 number = {4}
}

Systems of stochastic chemical kinetics are modeled as infinite level-dependent quasibirth-and-death (LDQBD) processes. For these systems, in contrast to many other applications, levels have an increasing number of states as the level number increases and the probability mass may reside arbitrarily far away from lower levels. Ideas from Lyapunov theory are combined with existing matrix-analytic formulations to obtain accurate approximations to the stationary probability distribution when the infinite LDQBD process is ergodic. Results of numerical experiments on a set of problems are provided. © Applied Probability Trust 2011.

@inproceedings{
 title = {SHAVE - Stochastic hybrid analysis of Markov population models},
 type = {inproceedings},
 year = {2011},
 keywords = {[Markov processes, Tool, Transient analysis]},
 id = {f86c42f9-a0b7-337b-abf0-baebdaa73827},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We present a tool called SHAVE that approximates the transient distribution of a continuous-time Markov population process by combining moment-based and state-based representations of probability distributions. As an intermediate step, SHAVE constructs a stochastic hybrid model from the original process which is then solved numerically. Copyright 2011 ACM.},
 bibtype = {inproceedings},
 author = {Lapin, M. and Mikeev, L. and Wolf, V.},
 doi = {10.1145/1967701.1967746},
 booktitle = {HSCC'11 - Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control}
}

We present a tool called SHAVE that approximates the transient distribution of a continuous-time Markov population process by combining moment-based and state-based representations of probability distributions. As an intermediate step, SHAVE constructs a stochastic hybrid model from the original process which is then solved numerically. Copyright 2011 ACM.

@inproceedings{
 title = {Efficient calculation of rare event probabilities in Markovian queueing networks},
 type = {inproceedings},
 year = {2011},
 keywords = {[Importance sampling, Markov chains, Queueing netw},
 id = {0a49545c-638d-30d8-9db0-e4178483beb0},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We address the computation of rare event probabilities in Markovian queueing networks with huge or possibly even infinite state spaces. For this purpose, we incorporate ideas from importance sampling simulations into a non-simulative numerical method that approximates transient probabilities based on a dynamical truncation of the state space. A change of measure technique is applied in order to accomplish a guided state space exploration. Numerical results for three different example networks demonstrate the efficiency and accuracy of our method. Copyright © 2011 ICST.},
 bibtype = {inproceedings},
 author = {Mikeev, L. and Sandmann, W. and Wolf, V.},
 doi = {10.4108/icst.valuetools.2011.245597},
 booktitle = {VALUETOOLS 2011 - 5th International ICST Conference on Performance Evaluation Methodologies and Tools}
}

We address the computation of rare event probabilities in Markovian queueing networks with huge or possibly even infinite state spaces. For this purpose, we incorporate ideas from importance sampling simulations into a non-simulative numerical method that approximates transient probabilities based on a dynamical truncation of the state space. A change of measure technique is applied in order to accomplish a guided state space exploration. Numerical results for three different example networks demonstrate the efficiency and accuracy of our method. Copyright © 2011 ICST.

@article{
 title = {Approximation of event probabilities in noisy cellular processes},
 type = {article},
 year = {2011},
 keywords = {[Chemical master equation, Gillespie simulation, I},
 volume = {412},
 id = {dc5819d4-b581-388f-b60c-f6be3f8d1ad4},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required. © 2011 Elsevier B.V. All rights reserved.},
 bibtype = {article},
 author = {Didier, F. and Henzinger, T.A. and Mateescu, M. and Wolf, V.},
 doi = {10.1016/j.tcs.2010.10.022},
 journal = {Theoretical Computer Science},
 number = {21}
}

Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required. © 2011 Elsevier B.V. All rights reserved.

@book{
 title = {Parameter identification for Markov models of biochemical reactions},
 type = {book},
 year = {2011},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {6806 LNCS},
 id = {9abc68a3-b901-391a-8e8f-8fa8b3cb7073},
 created = {2017-12-21T13:50:26.265Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.265Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We propose a numerical technique for parameter inference in Markov models of biological processes. Based on time-series data of a process we estimate the kinetic rate constants by maximizing the likelihood of the data. The computation of the likelihood relies on a dynamic abstraction of the discrete state space of the Markov model which successfully mitigates the problem of state space largeness. We compare two variants of our method to state-of-the-art, recently published methods and demonstrate their usefulness and efficiency on several case studies from systems biology. © 2011 Springer-Verlag.},
 bibtype = {book},
 author = {Andreychenko, A. and Mikeev, L. and Spieler, D. and Wolf, V.},
 doi = {10.1007/978-3-642-22110-1_8}
}

We propose a numerical technique for parameter inference in Markov models of biological processes. Based on time-series data of a process we estimate the kinetic rate constants by maximizing the likelihood of the data. The computation of the likelihood relies on a dynamic abstraction of the discrete state space of the Markov model which successfully mitigates the problem of state space largeness. We compare two variants of our method to state-of-the-art, recently published methods and demonstrate their usefulness and efficiency on several case studies from systems biology. © 2011 Springer-Verlag.

@article{
 title = {Formalisms for specifying Markovian population models},
 type = {article},
 year = {2011},
 volume = {22},
 id = {ec9d0ecd-898c-371f-a418-e6108be5de38},
 created = {2017-12-21T13:50:26.908Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.908Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {In this survey, we compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. All these languages - matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models - describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, and ease of use. Moreover, they provide different support for checking the well-formedness of a model and for analyzing a model. © 2011 World Scientific Publishing Company.},
 bibtype = {article},
 author = {Henzinger, T. and Jobstmann, B. and Wolf, V.},
 doi = {10.1142/S0129054111008441},
 journal = {International Journal of Foundations of Computer Science},
 number = {4}
}

In this survey, we compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. All these languages - matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models - describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, and ease of use. Moreover, they provide different support for checking the well-formedness of a model and for analyzing a model. © 2011 World Scientific Publishing Company.

@inproceedings{
 title = {On the Numerical Analysis of Stochastic Lotka-Volterra Models},
 type = {inproceedings},
 year = {2010},
 websites = {http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=5680059&url=http%3A%2F%2Fieeexplore.ieee.org%2Fiel5%2F5676244%2F5679615%2F05680059.pdf%3Farnumber%3D5680059},
 publisher = {IMCSIT},
 id = {7aed6a46-cf97-32ef-ac5a-73cfaa728239},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {CANA},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {The stochastic Lotka-Volterra model is an infinite Markov population model that has applications in various life science domains. Its analysis is challenging since, besides an infinite state space with unbounded rates, it shows strongly fluctuating dynamics and becomes unstable in the long-run. Traditional numerical methods are therefore not appropriate to solve the system. Here, we suggest adaptations and combinations of traditional methods that yield fast and accurate solutions for certain parameter ranges of the stochastic Lotka-Volterra model. We substantiate our theoretical investigations with a comparison based on experimental results.},
 bibtype = {inproceedings},
 author = {Dayar, Tugrul and Mikeev, Linar and Wolf, Verena},
 booktitle = {Proceedings of the Workshop on Computer Aspects of Numerical Algorithms (CANA'10)}
}

The stochastic Lotka-Volterra model is an infinite Markov population model that has applications in various life science domains. Its analysis is challenging since, besides an infinite state space with unbounded rates, it shows strongly fluctuating dynamics and becomes unstable in the long-run. Traditional numerical methods are therefore not appropriate to solve the system. Here, we suggest adaptations and combinations of traditional methods that yield fast and accurate solutions for certain parameter ranges of the stochastic Lotka-Volterra model. We substantiate our theoretical investigations with a comparison based on experimental results.

@article{
 title = {Solving the Chemical Master Equation Using Sliding Windows},
 type = {article},
 year = {2010},
 volume = {4},
 websites = {http://bmcsystbiol.biomedcentral.com/articles/10.1186/1752-0509-4-42},
 publisher = {BioMed Central},
 id = {14ae38b4-78eb-30e7-b8b2-9dfdd1081c74},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {sliding},
 source_type = {article},
 private_publication = {false},
 abstract = {The chemical master equation (CME) is a system of ordinary differential equations that describes the evolution of a network of chemical reactions as a stochastic process. Its solution yields the probability density vector of the system at each point in time. Solving the CME numerically is in many cases computationally expensive or even infeasible as the number of reachable states can be very large or infinite. We introduce the sliding window method, which computes an approximate solution of the CME by performing a sequence of local analysis steps. In each step, only a manageable subset of states is considered, representing a "window" into the state space. In subsequent steps, the window follows the direction in which the probability mass moves, until the time period of interest has elapsed. We construct the window based on a deterministic approximation of the future behavior of the system by estimating upper and lower bounds on the populations of the chemical species.},
 bibtype = {article},
 author = {Wolf, Verena and Goel, Rushil and Mateescu, Maria and Henzinger, Thomas A},
 journal = {BMC Systems Biology Journal},
 number = {42}
}

The chemical master equation (CME) is a system of ordinary differential equations that describes the evolution of a network of chemical reactions as a stochastic process. Its solution yields the probability density vector of the system at each point in time. Solving the CME numerically is in many cases computationally expensive or even infeasible as the number of reachable states can be very large or infinite. We introduce the sliding window method, which computes an approximate solution of the CME by performing a sequence of local analysis steps. In each step, only a manageable subset of states is considered, representing a "window" into the state space. In subsequent steps, the window follows the direction in which the probability mass moves, until the time period of interest has elapsed. We construct the window based on a deterministic approximation of the future behavior of the system by estimating upper and lower bounds on the populations of the chemical species.

@inproceedings{
 title = {SABRE: A Tool for Stochastic Analysis of Biochemical Reaction Networks},
 type = {inproceedings},
 year = {2010},
 pages = {193-194},
 websites = {https://www.computer.org/csdl/proceedings/qest/2010/4188/00/4188a193.pdf},
 publisher = {IEEE Computer Society},
 id = {12216ac7-e878-3000-bc2e-1d9461b726c8},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Sabre},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {The importance of stochasticity within biological systems has been shown repeatedly during the last years and has raised the need for efficient stochastic tools. We present SABRE, a tool for stochastic analysis of biochemical reaction networks. SABRE implements fast adaptive uniformization, a direct numerical approximation algorithm for computing transient solutions of biochemical reaction networks. In addition to the stochastic analysis, SABRE may also conduct deterministic analysis.},
 bibtype = {inproceedings},
 author = {Didier, Frederic and Henzinger, Thomas A and Mateescu, Maria and Wolf, Verena},
 booktitle = {Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST'10)}
}

The importance of stochasticity within biological systems has been shown repeatedly during the last years and has raised the need for efficient stochastic tools. We present SABRE, a tool for stochastic analysis of biochemical reaction networks. SABRE implements fast adaptive uniformization, a direct numerical approximation algorithm for computing transient solutions of biochemical reaction networks. In addition to the stochastic analysis, SABRE may also conduct deterministic analysis.

@inproceedings{
 title = {Hybrid Numerical Solution of the Chemical Master Equation},
 type = {inproceedings},
 year = {2010},
 pages = {55-65},
 websites = {http://dl.acm.org/citation.cfm?id=1839772},
 series = {ACM International Conference Proceeding Series},
 id = {0f72c681-3354-33c7-858d-d7d095b91540},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {hybrid},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We present a numerical approximation technique for the analysis of continuous-time Markov chains that describe networks of biochemical reactions and play an important role in the stochastic modeling of biological systems. Our approach is based on the construction of a stochastic hybrid model in which certain discrete random variables of the original Markov chain are approximated by continuous deterministic variables. We compute the solution of the stochastic hybrid model using a numerical algorithm that discretizes time and in each step performs a mutual update of the transient probability distribution of the discrete stochastic variables and the values of the continuous deterministic variables. We implemented the algorithm and we demonstrate its usefulness and efficiency on several case studies from systems biology.},
 bibtype = {inproceedings},
 author = {Henzinger, Thomas A and Mateescu, Maria and Mikeev, Linar and Wolf, Verena},
 booktitle = {Proceedings of the 8th International Conference on Computational Methods in Systems Biology (CMSB '10)}
}

We present a numerical approximation technique for the analysis of continuous-time Markov chains that describe networks of biochemical reactions and play an important role in the stochastic modeling of biological systems. Our approach is based on the construction of a stochastic hybrid model in which certain discrete random variables of the original Markov chain are approximated by continuous deterministic variables. We compute the solution of the stochastic hybrid model using a numerical algorithm that discretizes time and in each step performs a mutual update of the transient probability distribution of the discrete stochastic variables and the values of the continuous deterministic variables. We implemented the algorithm and we demonstrate its usefulness and efficiency on several case studies from systems biology.

@article{
 title = {Fast adaptive uniformisation of the chemical master equation},
 type = {article},
 year = {2010},
 volume = {4},
 id = {556e0fa0-023e-34cf-bc59-431f4dcd1335},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Within systems biology there is an increasing interest in the stochastic behaviour of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equationwhich represents a continuous-time Markov chain (CTMC). The uniformisation technique is an efficient method to compute probability distributions of a CTMC if the number of states is manageable. Howeverthe size of a CTMC that represents a biochemical reaction network is usually far beyond what is feasible. In this studythe authors present an on-the-fly variant of uniformisationwhere they improve the original algorithm at the cost of a small approximation error. By means of several examplesthe authors show that their approach is particularly well-suited for biochemical reaction networks. © 2010 © The Institution of Engineering and Technology.},
 bibtype = {article},
 author = {Mateescu, M. and Wolf, V. and Didier, F. and Henzinger, T.A.},
 doi = {10.1049/iet-syb.2010.0005},
 journal = {IET Systems Biology},
 number = {6}
}

Within systems biology there is an increasing interest in the stochastic behaviour of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equationwhich represents a continuous-time Markov chain (CTMC). The uniformisation technique is an efficient method to compute probability distributions of a CTMC if the number of states is manageable. Howeverthe size of a CTMC that represents a biochemical reaction network is usually far beyond what is feasible. In this studythe authors present an on-the-fly variant of uniformisationwhere they improve the original algorithm at the cost of a small approximation error. By means of several examplesthe authors show that their approach is particularly well-suited for biochemical reaction networks. © 2010 © The Institution of Engineering and Technology.

@inproceedings{
 title = {SABRE: A tool for stochastic analysis of biochemical reaction networks},
 type = {inproceedings},
 year = {2010},
 id = {7effc7ab-8ba2-3329-9e4c-cc1412e20248},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {The importance of stochasticity within biological systems has been shown repeatedly during the last years and has raised the need for efficient stochastic tools. We present SABRE, a tool for stochastic analysis of biochemical reaction networks. SABRE implements fast adaptive uniformization, a direct numerical approximation algorithm for computing transient solutions of biochemical reaction networks. In addition to the stochastic analysis, SABRE may also conduct deterministic analysis. © 2010 IEEE.},
 bibtype = {inproceedings},
 author = {Didier, F. and Henzinger, T.A. and Mateescu, M. and Wolf, V.},
 doi = {10.1109/QEST.2010.33},
 booktitle = {Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010}
}

The importance of stochasticity within biological systems has been shown repeatedly during the last years and has raised the need for efficient stochastic tools. We present SABRE, a tool for stochastic analysis of biochemical reaction networks. SABRE implements fast adaptive uniformization, a direct numerical approximation algorithm for computing transient solutions of biochemical reaction networks. In addition to the stochastic analysis, SABRE may also conduct deterministic analysis. © 2010 IEEE.

@inproceedings{
 title = {Hybrid numerical solution of the chemical master equation},
 type = {inproceedings},
 year = {2010},
 keywords = {[Biochemical reaction network, Chemical master equ},
 id = {1f409d92-c85f-306e-90bd-fa92b97f1285},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We present a numerical approximation technique for the analysis of continuous-time Markov chains that describe networks of biochemical reactions and play an important role in the stochastic modeling of biological systems. Our approach is based on the construction of a stochastic hybrid model in which certain discrete random variables of the original Markov chain are approximated by continuous deterministic variables. We compute the solution of the stochastic hybrid model using a numerical algorithm that discretizes time and in each step performs a mutual update of the transient probability distribution of the discrete stochastic variables and the values of the continuous deterministic variables. We implemented the algorithm and we demonstrate its usefulness and effciency on several case studies from systems biology. Copyright 2010 ACM.},
 bibtype = {inproceedings},
 author = {Henzinger, T.A. and Mateescu, M. and Mikeev, L. and Wolf, V.},
 doi = {10.1145/1839764.1839772},
 booktitle = {CMSB 2010 - Proceedings of the 8th International Conference on Computational Methods in Systems Biology}
}

We present a numerical approximation technique for the analysis of continuous-time Markov chains that describe networks of biochemical reactions and play an important role in the stochastic modeling of biological systems. Our approach is based on the construction of a stochastic hybrid model in which certain discrete random variables of the original Markov chain are approximated by continuous deterministic variables. We compute the solution of the stochastic hybrid model using a numerical algorithm that discretizes time and in each step performs a mutual update of the transient probability distribution of the discrete stochastic variables and the values of the continuous deterministic variables. We implemented the algorithm and we demonstrate its usefulness and effciency on several case studies from systems biology. Copyright 2010 ACM.

@article{
 title = {Solving the chemical master equation using sliding windows},
 type = {article},
 year = {2010},
 volume = {4},
 id = {a32d0544-eeb3-3157-a034-1605b8a3faac},
 created = {2017-12-21T13:50:26.520Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.520Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Background: The chemical master equation (CME) is a system of ordinary differential equations that describes the evolution of a network of chemical reactions as a stochastic process. Its solution yields the probability density vector of the system at each point in time. Solving the CME numerically is in many cases computationally expensive or even infeasible as the number of reachable states can be very large or infinite. We introduce the sliding window method, which computes an approximate solution of the CME by performing a sequence of local analysis steps. In each step, only a manageable subset of states is considered, representing a "window" into the state space. In subsequent steps, the window follows the direction in which the probability mass moves, until the time period of interest has elapsed. We construct the window based on a deterministic approximation of the future behavior of the system by estimating upper and lower bounds on the populations of the chemical species.Results: In order to show the effectiveness of our approach, we apply it to several examples previously described in the literature. The experimental results show that the proposed method speeds up the analysis considerably, compared to a global analysis, while still providing high accuracy.Conclusions: The sliding window method is a novel approach to address the performance problems of numerical algorithms for the solution of the chemical master equation. The method efficiently approximates the probability distributions at the time points of interest for a variety of chemically reacting systems, including systems for which no upper bound on the population sizes of the chemical species is known a priori. © 2010 Wolf et al; licensee BioMed Central Ltd.},
 bibtype = {article},
 author = {Wolf, V. and Goel, R. and Mateescu, M. and Henzinger, T.A.},
 doi = {10.1186/1752-0509-4-42},
 journal = {BMC Systems Biology}
}

Background: The chemical master equation (CME) is a system of ordinary differential equations that describes the evolution of a network of chemical reactions as a stochastic process. Its solution yields the probability density vector of the system at each point in time. Solving the CME numerically is in many cases computationally expensive or even infeasible as the number of reachable states can be very large or infinite. We introduce the sliding window method, which computes an approximate solution of the CME by performing a sequence of local analysis steps. In each step, only a manageable subset of states is considered, representing a "window" into the state space. In subsequent steps, the window follows the direction in which the probability mass moves, until the time period of interest has elapsed. We construct the window based on a deterministic approximation of the future behavior of the system by estimating upper and lower bounds on the populations of the chemical species.Results: In order to show the effectiveness of our approach, we apply it to several examples previously described in the literature. The experimental results show that the proposed method speeds up the analysis considerably, compared to a global analysis, while still providing high accuracy.Conclusions: The sliding window method is a novel approach to address the performance problems of numerical algorithms for the solution of the chemical master equation. The method efficiently approximates the probability distributions at the time points of interest for a variety of chemically reacting systems, including systems for which no upper bound on the population sizes of the chemical species is known a priori. © 2010 Wolf et al; licensee BioMed Central Ltd.

@inproceedings{
 title = {Formalisms for Specifying Markovian Population Models},
 type = {inproceedings},
 year = {2009},
 volume = {5797},
 websites = {http://dl.acm.org/citation.cfm?id=1617521},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {e78d7f4d-85e0-3849-abd4-012800586311},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {TSpaper},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages --matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models-- all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model.},
 bibtype = {inproceedings},
 author = {Henzinger, Thomas A and Jobstmann, Barbara and Wolf, Verena},
 booktitle = {Proceedings of the 3rd International Workshop on Reachability Problems (RP'09)}
}

We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages --matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models-- all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model.

@inproceedings{
 title = {Fast Adaptive Uniformization of the Chemical Master Equation},
 type = {inproceedings},
 year = {2009},
 pages = {118-127},
 websites = {http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=5298685&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D5298685},
 publisher = {IEEE Computer Society},
 id = {0d28741a-4771-3363-a097-73d158fd8a74},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {HIBI09},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {Within systems biology there is an increasing interest in the stochastic behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous-time Markov chain (CTMC). Standard Uniformization (SU) is an efficient method for the transient analysis of CTMCs. For systems with very different time scales, such as biochemical reaction networks, SU is computationally expensive. In these cases, a variant of SU, called adaptive uniformization (AU), is known to reduce the large number of iterations needed by SU. The additional difficulty of AU is that it requires the solution of a birth process. In this paper we present an on-the-fly variant of AU, where we improve the original algorithm for AU at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks.},
 bibtype = {inproceedings},
 author = {Didier, Frédéric and Henzinger, Thomas A and Mateescu, Maria and Wolf, Verena},
 booktitle = {Proceedings of the High Performance Computational Systems Biology Workshop (HIBI'09)}
}

Within systems biology there is an increasing interest in the stochastic behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous-time Markov chain (CTMC). Standard Uniformization (SU) is an efficient method for the transient analysis of CTMCs. For systems with very different time scales, such as biochemical reaction networks, SU is computationally expensive. In these cases, a variant of SU, called adaptive uniformization (AU), is known to reduce the large number of iterations needed by SU. The additional difficulty of AU is that it requires the solution of a birth process. In this paper we present an on-the-fly variant of AU, where we improve the original algorithm for AU at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks.

@inproceedings{
 title = {Approximation of Event Probabilities in Noisy Cellular Processes},
 type = {inproceedings},
 year = {2009},
 pages = {173-183},
 volume = {5688},
 websites = {http://www.sciencedirect.com/science/article/pii/S0304397510005840},
 publisher = {Springer},
 series = {Lecture Notes in Bioinformatics},
 id = {2ab31427-4381-3475-a257-5191d17d9006},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {CMSB09},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.},
 bibtype = {inproceedings},
 author = {Didier, Frédéric and Henzinger, Thomas A and Mateescu, Maria and Wolf, Verena},
 booktitle = {Proceedings of the 7th International Conference on Computational Methods in Systems Biology (CMSB'09)}
}

Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.

@inproceedings{
 title = {Sliding Window Abstraction for Infinite Markov Chains},
 type = {inproceedings},
 year = {2009},
 pages = {337-352},
 volume = {5643},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-642-02658-4_27},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {f0e85fff-d267-3539-b85b-63b87ee57814},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {slidingCAV},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology.},
 bibtype = {inproceedings},
 author = {Henzinger, T and Mateescu, M and Wolf, V},
 booktitle = {Proceedings of the 21st International Conference on Computer Aided Verification (CAV'09)}
}

We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology.

@book{
 title = {Approximation of event probabilities in noisy cellular processes},
 type = {book},
 year = {2009},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {5688 LNBI},
 id = {51e8fe54-09b8-3c26-85a4-cd0ba82a3ea1},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete -state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required. © 2009 Springer Berlin Heidelberg.},
 bibtype = {book},
 author = {Didier, F. and Henzinger, T.A. and Mateescu, M. and Wolf, V.},
 doi = {10.1007/978-3-642-03845-7_12}
}

Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete -state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required. © 2009 Springer Berlin Heidelberg.

@inproceedings{
 title = {Fast adaptive uniformization of the chemical master equation},
 type = {inproceedings},
 year = {2009},
 keywords = {[Biochemical reactions, Chemical master equation,},
 id = {eed70c1e-db1c-318f-a881-d3ab5af96a5e},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Within systems biology there is an increasing interest in the stochastic behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous-time Markov chain (CTMC). Standard Uniformization (SU) is an efficient method for the transient analysis of CTMCs. For systems with very different time scales, such as biochemical reaction networks, SU is computationally expensive. In these cases, a variant of SU, called adaptive uniformization (AU), is known to reduce the large number of iterations needed by SU. The additional difficulty of AU is that it requires the solution of a birth process. In this paper we present an on-the-fly variant of AU, where we improve the original algorithm for AU at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks. © 2009 IEEE.},
 bibtype = {inproceedings},
 author = {Didier, F. and Henzinger, T.A. and Mateescu, M. and Wolf, V.},
 doi = {10.1109/HiBi.2009.23},
 booktitle = {HiBi09 - 2009 International Workshop on High Performance Computational Systems Biology}
}

Within systems biology there is an increasing interest in the stochastic behavior of biochemical reaction networks. An appropriate stochastic description is provided by the chemical master equation, which represents a continuous-time Markov chain (CTMC). Standard Uniformization (SU) is an efficient method for the transient analysis of CTMCs. For systems with very different time scales, such as biochemical reaction networks, SU is computationally expensive. In these cases, a variant of SU, called adaptive uniformization (AU), is known to reduce the large number of iterations needed by SU. The additional difficulty of AU is that it requires the solution of a birth process. In this paper we present an on-the-fly variant of AU, where we improve the original algorithm for AU at the cost of a small approximation error. By means of several examples, we show that our approach is particularly well-suited for biochemical reaction networks. © 2009 IEEE.

@book{
 title = {Sliding window abstraction for infinite markov chains},
 type = {book},
 year = {2009},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {5643 LNCS},
 id = {a43bc289-8bc1-3892-a69f-fbc40eea22dd},
 created = {2017-12-21T13:50:26.326Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.326Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology. © 2009 Springer Berlin Heidelberg.},
 bibtype = {book},
 author = {Henzinger, T.A. and Mateescu, M. and Wolf, V.},
 doi = {10.1007/978-3-642-02658-4_27}
}

We present an on-the-fly abstraction technique for infinite-state continuous -time Markov chains. We consider Markov chains that are specified by a finite set of transition classes. Such models naturally represent biochemical reactions and therefore play an important role in the stochastic modeling of biological systems. We approximate the transient probability distributions at various time instances by solving a sequence of dynamically constructed abstract models, each depending on the previous one. Each abstract model is a finite Markov chain that represents the behavior of the original, infinite chain during a specific time interval. Our approach provides complete information about probability distributions, not just about individual parameters like the mean. The error of each abstraction can be computed, and the precision of the abstraction refined when desired. We implemented the algorithm and demonstrate its usefulness and efficiency on several case studies from systems biology. © 2009 Springer Berlin Heidelberg.

@book{
 title = {Formalisms for specifying Markovian population models},
 type = {book},
 year = {2009},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {5797 LNCS},
 id = {04c60d6e-f06d-3c26-b4b2-dd2bde45ce7f},
 created = {2017-12-21T13:50:26.573Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.573Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages -matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models- all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model. © 2009 Springer Berlin Heidelberg.},
 bibtype = {book},
 author = {Henzinger, T.A. and Jobstmann, B. and Wolf, V.},
 doi = {10.1007/978-3-642-04420-5_2}
}

We compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. These languages -matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models- all describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, ease of use, and the support they provide for checking the well-formedness of a model and for analyzing a model. © 2009 Springer Berlin Heidelberg.

@inproceedings{
 title = {Abstraction for Stochastic Systems by Erlang`s Method of Stages},
 type = {inproceedings},
 year = {2008},
 pages = {279-294},
 volume = {5201},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-540-85361-9_24#page-1},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {ccc739f2-1a14-3d5b-86b9-c3a6ca02f4c7},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {KKLW08},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {This paper proposes a novel abstraction technique based on Erlang’s method of stages for continuous-time Markov chains (CTMCs). As abstract models Erlang-k interval processes are proposed where state residence times are governed by Poisson processes and transition probabilities are specified by intervals. We provide a three-valued semantics of CSL (Continuous Stochastic Logic) for Erlang-k interval processes, and show that both affirmative and negative verification results are preserved by our abstraction. The feasibility of our technique is demonstrated by a quantitative analysis of an enzyme-catalyzed substrate conversion, a well-known case study from biochemistry.},
 bibtype = {inproceedings},
 author = {Katoen, J.-P. and Klink, D and Leucker, M and Wolf, V},
 booktitle = {Proceedings of the 19th International Conference on Concurrency Theory (CONCUR'08)}
}

This paper proposes a novel abstraction technique based on Erlang’s method of stages for continuous-time Markov chains (CTMCs). As abstract models Erlang-k interval processes are proposed where state residence times are governed by Poisson processes and transition probabilities are specified by intervals. We provide a three-valued semantics of CSL (Continuous Stochastic Logic) for Erlang-k interval processes, and show that both affirmative and negative verification results are preserved by our abstraction. The feasibility of our technique is demonstrated by a quantitative analysis of an enzyme-catalyzed substrate conversion, a well-known case study from biochemistry.

@misc{
 title = {Equivalences on Phase Type Processes},
 type = {misc},
 year = {2008},
 institution = {University of Mannheim},
 id = {75c0d8d4-faff-3a15-9fd0-89f34bc6e158},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {thesisWolf},
 source_type = {other},
 notes = {Dissertation},
 private_publication = {false},
 bibtype = {misc},
 author = {Wolf, V}
}

@inproceedings{
 title = {Computational Probability for Systems Biology},
 type = {inproceedings},
 year = {2008},
 pages = {33-47},
 volume = {5054},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-540-68413-8_3},
 publisher = {Springer},
 series = {Lecture Notes in Bioinformatics},
 id = {ceaf5ce9-fbd7-3ca4-bfa9-403f0fdf4ce5},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {SW08},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {Stochastic models of biological networks properly take the randomness of molecular dynamics in living cells into account. Numerical solution approaches inspired by computational methods from applied probability can efficiently yield accurate results and have significant advantages compared to stochastic simulation. Examples for the success of non-simulative numerical analysis techniques in systems biology confirm the enormous potential.},
 bibtype = {inproceedings},
 author = {Sandmann, W and Wolf, V},
 booktitle = {Proceedings of the International Workshop on Formal Methods in Systems Biology (FMSB'08)}
}

Stochastic models of biological networks properly take the randomness of molecular dynamics in living cells into account. Numerical solution approaches inspired by computational methods from applied probability can efficiently yield accurate results and have significant advantages compared to stochastic simulation. Examples for the success of non-simulative numerical analysis techniques in systems biology confirm the enormous potential.

@article{
 title = {Modelling of Biochemical Reactions by Stochastic Automata Networks},
 type = {article},
 year = {2007},
 keywords = {Biochemical Reactions,Markov Chain,Stochastic Automata Networks},
 pages = {197-208},
 volume = {171},
 websites = {http://www.sciencedirect.com/science/article/pii/S1571066107002952},
 id = {56e79e03-43e1-3a43-a5cb-0e5de963f771},
 created = {2016-02-15T08:58:11.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {This paper presents a stochastic modelling framework based on stochastic automata networks (SANs) for the analysis of complex biochemical reaction networks. Our approach takes into account the discrete character of quantities of components (i.e. the individual populations of the involved chemical species) and the inherent probabilistic nature of microscopic molecular collisions. Moreover, as for process calculi that have recently been applied to systems in biology, the SAN approach has the advantage of a modular design process being adequate for abstraction purposes. The associated composition operator leads to an elegant and compact representation of the underlying continuous-time Markov chain in form of a Kronecker product. SANs have been extensively used in performance analysis of computer systems and a large variety of numerical and simulative analysis algorithms exist. We illustrate that describing a biochemical reaction network by means of a SAN offers promising opportunities to get insight into the quantitative behaviour of systems in biology while taking advantage of the benefits of a compositional modelling approach. ?? 2007 Elsevier B.V. All rights reserved.},
 bibtype = {article},
 author = {Wolf, Verena},
 journal = {Electronic Notes in Theoretical Computer Science},
 number = {2 SPEC. ISS.}
}

This paper presents a stochastic modelling framework based on stochastic automata networks (SANs) for the analysis of complex biochemical reaction networks. Our approach takes into account the discrete character of quantities of components (i.e. the individual populations of the involved chemical species) and the inherent probabilistic nature of microscopic molecular collisions. Moreover, as for process calculi that have recently been applied to systems in biology, the SAN approach has the advantage of a modular design process being adequate for abstraction purposes. The associated composition operator leads to an elegant and compact representation of the underlying continuous-time Markov chain in form of a Kronecker product. SANs have been extensively used in performance analysis of computer systems and a large variety of numerical and simulative analysis algorithms exist. We illustrate that describing a biochemical reaction network by means of a SAN offers promising opportunities to get insight into the quantitative behaviour of systems in biology while taking advantage of the benefits of a compositional modelling approach. ?? 2007 Elsevier B.V. All rights reserved.

@inproceedings{
 title = {Three-Valued Abstraction for Continuous-Time Markov Chains},
 type = {inproceedings},
 year = {2007},
 pages = {316-329},
 volume = {4590},
 websites = {http://link.springer.com/chapter/10.1007%2F978-3-540-73368-3_37},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {09179be2-5c44-348f-98d5-ac7f69739f03},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {KKLW07},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {This paper proposes a novel abstraction technique for continuous-time Markov chains (CTMCs). Our technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key idea is to apply abstraction on uniform CTMCs that are readily obtained from general CTMCs, and to abstract transition probabilities by intervals. It is shown that this provides a conservative abstraction for both true and false for a three-valued semantics of the branching-time logic CSL (Continuous Stochastic Logic). Experiments on an infinite-state CTMC indicate the feasibility of our abstraction technique.},
 bibtype = {inproceedings},
 author = {Katoen, J.-P. and Klink, D and Leucker, M and Wolf, V},
 booktitle = {Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)}
}

This paper proposes a novel abstraction technique for continuous-time Markov chains (CTMCs). Our technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key idea is to apply abstraction on uniform CTMCs that are readily obtained from general CTMCs, and to abstract transition probabilities by intervals. It is shown that this provides a conservative abstraction for both true and false for a three-valued semantics of the branching-time logic CSL (Continuous Stochastic Logic). Experiments on an infinite-state CTMC indicate the feasibility of our abstraction technique.

@inproceedings{
 title = {Interaction Models for Biochemical Reactions},
 type = {inproceedings},
 year = {2007},
 pages = {480-486},
 publisher = {CSREA Press},
 id = {dd26de27-668d-3e86-91e6-7a730625a9b6},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {biocomp},
 source_type = {inproceedings},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Majster-Cederbaum, Mila E and Semmelrock, Nils and Wolf, Verena},
 booktitle = {Proceedings of the International Conference on Bioinformatics and Computational Biology (BIOCOMP'07)}
}

@book{
 title = {Three-valued abstraction for continuous-time markov chains},
 type = {book},
 year = {2007},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {4590 LNCS},
 id = {501ea18e-3507-388d-93a9-d320dad59c86},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {This paper proposes a novel abstraction technique for continuous-time Markov chains (CTMCs). Our technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key idea is to apply abstraction on uniform CTMCs that are readily obtained from general CTMCs, and to abstract transition probabilities by intervals. It is shown that this provides a conservative abstraction for both true and false for a three-valued semantics of the branching-time logic CSL (Continuous Stochastic Logic). Experiments on an infinite-state CTMC indicate the feasibility of our abstraction technique. © Springer-Verlag Berlin Heidelberg 2007.},
 bibtype = {book},
 author = {Katoen, J.-P. and Klink, D. and Leucker, M. and Wolf, V.}
}

This paper proposes a novel abstraction technique for continuous-time Markov chains (CTMCs). Our technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key idea is to apply abstraction on uniform CTMCs that are readily obtained from general CTMCs, and to abstract transition probabilities by intervals. It is shown that this provides a conservative abstraction for both true and false for a three-valued semantics of the branching-time logic CSL (Continuous Stochastic Logic). Experiments on an infinite-state CTMC indicate the feasibility of our abstraction technique. © Springer-Verlag Berlin Heidelberg 2007.

@inproceedings{
 title = {A Numerical Aggregation Algorithm for the Enzyme-Catalyzed Substrate Conversion},
 type = {inproceedings},
 year = {2006},
 pages = {298-311},
 volume = {4210},
 websites = {http://www.springerlink.com/index/121221u810741l81.pdf},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {d36fd5fa-5236-3a13-9303-1d7ace15b872},
 created = {2016-02-15T08:58:11.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {Computational models of biochemical systems are usually very large, and moreover, if reaction frequencies of different reaction types differ in orders of magnitude, models possess the mathematical property of stiffness, which renders system analysis difficult and often even impossible with traditional methods. Recently, an accelerated stochastic simulation technique based on a system partitioning, the slow-scale stochastic simulation algorithm, has been applied to the enzyme-catalyzed substrate conversion to circumvent the inefficiency of standard stochastic simulation in the presence of stiffness. We propose a numerical algorithm based on a similar partitioning but without resorting to simulation. The algorithm exploits the connection to continuous-time Markov chains and decomposes the overall problem to significantly smaller subproblems that become tractable. Numerical results show enormous efficiency improvements relative to accelerated stochastic simulation. Keywords: Biochemical Reactions, Stochastic Model, Markov Chain, Aggregation.},
 bibtype = {inproceedings},
 author = {Busch, Hauke and Sandmann, Werner and Wolf, Verena},
 editor = {Priami, Corrado},
 booktitle = {Computational Methods in Systems Biology}
}

Computational models of biochemical systems are usually very large, and moreover, if reaction frequencies of different reaction types differ in orders of magnitude, models possess the mathematical property of stiffness, which renders system analysis difficult and often even impossible with traditional methods. Recently, an accelerated stochastic simulation technique based on a system partitioning, the slow-scale stochastic simulation algorithm, has been applied to the enzyme-catalyzed substrate conversion to circumvent the inefficiency of standard stochastic simulation in the presence of stiffness. We propose a numerical algorithm based on a similar partitioning but without resorting to simulation. The algorithm exploits the connection to continuous-time Markov chains and decomposes the overall problem to significantly smaller subproblems that become tractable. Numerical results show enormous efficiency improvements relative to accelerated stochastic simulation. Keywords: Biochemical Reactions, Stochastic Model, Markov Chain, Aggregation.

@article{
 title = {Trace Semantics for Stochastic Systems with Nondeterminism},
 type = {article},
 year = {2006},
 keywords = {Button Pushing Experiment,Linear-time Semantics,Markov Chains,Nondeterminism,Trace Equivalence},
 pages = {187-204},
 volume = {164},
 id = {f9a64420-0fc2-3b7f-8d46-c1b5e40572bf},
 created = {2016-02-15T08:58:12.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {This paper discusses trace semantics of interactive Markov chains (IMCs) that are a generalisation of continuous-time Markov chains. In IMCs besides probabilistic alternatives there may be a nondeterministic choice between several action-labelled transitions in a state. We analyse several variants of trace equivalences that arise from the different ways one has to resolve nondeterministic branching. Button pushing testing scenarios are used to motivate each abstraction level induced by the trace semantics and associated equivalences are sorted according to their distinguishing power. ?? 2006 Elsevier B.V. All rights reserved.},
 bibtype = {article},
 author = {Wolf, Verena and Baier, Christel and Majster-Cederbaum, Mila},
 journal = {Electronic Notes in Theoretical Computer Science},
 number = {3 SPEC. ISS.}
}

This paper discusses trace semantics of interactive Markov chains (IMCs) that are a generalisation of continuous-time Markov chains. In IMCs besides probabilistic alternatives there may be a nondeterministic choice between several action-labelled transitions in a state. We analyse several variants of trace equivalences that arise from the different ways one has to resolve nondeterministic branching. Button pushing testing scenarios are used to motivate each abstraction level induced by the trace semantics and associated equivalences are sorted according to their distinguishing power. ?? 2006 Elsevier B.V. All rights reserved.

@inproceedings{
 title = {Stochastic Reasoning About Channel-based Component Connectors},
 type = {inproceedings},
 year = {2006},
 pages = {1-15},
 volume = {4038},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {3025c39f-a446-36d6-a51f-f9fe44441c5d},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {BW06},
 source_type = {inproceedings},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Baier, C and Wolf, V},
 booktitle = {Proceedings of the 8th International Conference on Coordination Models and Languages (COORDINATION'06)}
}

@inproceedings{
 title = {Don't know in probabilistic systems},
 type = {inproceedings},
 year = {2006},
 pages = {71-88},
 volume = {3925},
 websites = {http://link.springer.com/chapter/10.1007%2F11691617_5},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {5e54b353-87b3-3252-ba62-2c083e96ed8c},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {FLW06},
 source_type = {inproceedings},
 private_publication = {false},
 abstract = {In this paper the abstraction-refinement paradigm based on 3-valued logics is extended to the setting of probabilistic systems. We define a notion of abstraction for Markov chains. To be able to relate the behavior of abstract and concrete systems, we equip the notion of abstraction with the concept of simulation. Furthermore, we present model checking for abstract probabilistic systems (abstract Markov chains) with respect to specifications in probabilistic temporal logics, interpreted over a 3-valued domain. More specifically, we introduce a 3-valued version of probabilistic computation-tree logic (PCTL) and give a model checking algorithm w.r.t. abstract Markov chains.},
 bibtype = {inproceedings},
 author = {Fecher, H and Leucker, M and Wolf, V},
 booktitle = {Proceedings of 13th International SPIN Workshop on Model Checking of Software (SPIN'06)}
}

In this paper the abstraction-refinement paradigm based on 3-valued logics is extended to the setting of probabilistic systems. We define a notion of abstraction for Markov chains. To be able to relate the behavior of abstract and concrete systems, we equip the notion of abstraction with the concept of simulation. Furthermore, we present model checking for abstract probabilistic systems (abstract Markov chains) with respect to specifications in probabilistic temporal logics, interpreted over a 3-valued domain. More specifically, we introduce a 3-valued version of probabilistic computation-tree logic (PCTL) and give a model checking algorithm w.r.t. abstract Markov chains.

@inproceedings{
 title = {Bisimulation and Simulation Relations for Markov Chains},
 type = {inproceedings},
 year = {2006},
 pages = {73-78},
 volume = {162},
 publisher = {Elsevier},
 series = {Electronic Notes in Theoretical Computer Science},
 id = {7b3af4ac-d64a-3aac-b4c7-9d369c1ca00c},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {BHKW06},
 source_type = {inproceedings},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Baier, Christel and Hermanns, Holger and Katoen, Joost-Pieter and Wolf, Verena},
 booktitle = {Proceedings of the Workshop Essays on Algebraic Process Calculi (ACP'06)}
}

@book{
 title = {Stochastic reasoning about channel-based component connectors},
 type = {book},
 year = {2006},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {4038 LNCS},
 id = {0876bd37-e24e-3919-9f62-e4cc0425ad57},
 created = {2017-01-02T09:34:03.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Constraint automata have been used as an operational model for component connectors that coordinate the cooperation and communication of the components by means of a network of channels. In this paper, we introduce a variant of constraint automata (called continuous-time constraint automata) that allows us to specify time-dependent stochastic assumptions about the channel connections or the component interfaces, such as the arrival rates of communication requests, the average delay of enabled I/O-operations at the channel ends or the stochastic duration of internal computations. This yields the basis for a performance analysis of channel-based coordination mechanisms. We focus on compositional reasoning and discuss several bisimulation relations on continuous-time constraint automata. For this, we adapt notions of strong and weak bisimulation that have been introduced for similar stochastic models and introduce a new notion of weak bisimulation which abstracts away from invisible non-stochastic computations as well as the internal stochastic evolution. © Springer-Verlag Berlin Heidelberg 2006.},
 bibtype = {book},
 author = {Baier, C. and Wolf, V.}
}

Constraint automata have been used as an operational model for component connectors that coordinate the cooperation and communication of the components by means of a network of channels. In this paper, we introduce a variant of constraint automata (called continuous-time constraint automata) that allows us to specify time-dependent stochastic assumptions about the channel connections or the component interfaces, such as the arrival rates of communication requests, the average delay of enabled I/O-operations at the channel ends or the stochastic duration of internal computations. This yields the basis for a performance analysis of channel-based coordination mechanisms. We focus on compositional reasoning and discuss several bisimulation relations on continuous-time constraint automata. For this, we adapt notions of strong and weak bisimulation that have been introduced for similar stochastic models and introduce a new notion of weak bisimulation which abstracts away from invisible non-stochastic computations as well as the internal stochastic evolution. © Springer-Verlag Berlin Heidelberg 2006.

@book{
 title = {A numerical aggregation algorithm for the enzyme-catalyzed substrate conversion},
 type = {book},
 year = {2006},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 keywords = {[Aggregation, Biochemical reactions, Markov chain,},
 volume = {4210 LNBI},
 id = {dd2626e5-2087-35ab-ac81-c422e3f89b75},
 created = {2017-01-02T09:34:04.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {Computational models of biochemical systems are usually very large, and moreover, if reaction frequencies of different reaction types differ in orders of magnitude, models possess the mathematical property of stiffness, which renders system analysis difficult and often even impossible with traditional methods. Recently, an accelerated stochastic simulation technique based on a system partitioning, the slow-scale stochastic simulation algorithm, has been applied to the enzyme-catalyzed substrate conversion to circumvent the inefficiency of standard stochastic simulation in the presence of stiffness. We propose a numerical algorithm based on a similar partitioning but without resorting to simulation. The algorithm exploits the connection to continuous-time Markov chains and decomposes the overall problem to significantly smaller sub-problems that become tractable. Numerical results show enormous efficiency improvements relative to accelerated stochastic simulation. © Springer-Verlag Berlin Heidelberg 2006.},
 bibtype = {book},
 author = {Busch, H. and Sandmann, W. and Wolf, V.}
}

Computational models of biochemical systems are usually very large, and moreover, if reaction frequencies of different reaction types differ in orders of magnitude, models possess the mathematical property of stiffness, which renders system analysis difficult and often even impossible with traditional methods. Recently, an accelerated stochastic simulation technique based on a system partitioning, the slow-scale stochastic simulation algorithm, has been applied to the enzyme-catalyzed substrate conversion to circumvent the inefficiency of standard stochastic simulation in the presence of stiffness. We propose a numerical algorithm based on a similar partitioning but without resorting to simulation. The algorithm exploits the connection to continuous-time Markov chains and decomposes the overall problem to significantly smaller sub-problems that become tractable. Numerical results show enormous efficiency improvements relative to accelerated stochastic simulation. © Springer-Verlag Berlin Heidelberg 2006.

@article{
 title = {Trace Machines for Observing Continuous-Time Markov Chains},
 type = {article},
 year = {2006},
 keywords = {Markov chain,button pushing experiment,linear-time semantics,trace equivalence,trace machine},
 volume = {153},
 id = {15fe5983-c973-300d-8d62-e465bc559b13},
 created = {2017-12-21T13:50:26.456Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.456Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {In this paper, we study several linear-time equivalences (Markovian trace equivalence, failure and ready trace equivalence) for continuous-time Markov chains that refer to the probabilities for timed execution paths. Our focus is on testing scenarios by means of push-button experiments with appropriate trace machines and a discussion of the connections between the equivalences. For Markovian trace equivalence, we provide alternative characterizations, including one that abstracts away from the time instances where actions are observed, but just reports on the average sojourn times in the states. This result is used for a reduction of the question whether two finite-state continuous-time Markov chains are Markovian trace equivalent to the probabilistic trace equivalence problem for discrete-time Markov chains (and the latter is known to be solvable in polynomial time). © 2006 Elsevier B.V. All rights reserved.},
 bibtype = {article},
 author = {Wolf, V. and Baier, C. and Majster-Cederbaum, M.},
 doi = {10.1016/j.entcs.2005.10.042},
 journal = {Electronic Notes in Theoretical Computer Science},
 number = {2 SPEC. ISS.}
}

In this paper, we study several linear-time equivalences (Markovian trace equivalence, failure and ready trace equivalence) for continuous-time Markov chains that refer to the probabilities for timed execution paths. Our focus is on testing scenarios by means of push-button experiments with appropriate trace machines and a discussion of the connections between the equivalences. For Markovian trace equivalence, we provide alternative characterizations, including one that abstracts away from the time instances where actions are observed, but just reports on the average sojourn times in the states. This result is used for a reduction of the question whether two finite-state continuous-time Markov chains are Markovian trace equivalent to the probabilistic trace equivalence problem for discrete-time Markov chains (and the latter is known to be solvable in polynomial time). © 2006 Elsevier B.V. All rights reserved.

@article{
 title = {Testing theory for probabilistic systems},
 type = {article},
 year = {2005},
 keywords = {Algorithms,Automata theory,Polynomial time,Probabilistic bisimulation,Probabilistic logics,Probabilistic systems,Problem solving,Software testing,Testing theory},
 pages = {233-275},
 volume = {3472 LNCS},
 websites = {http://www.scopus.com/inward/record.url?eid=2-s2.0-36849044726&partnerID=40&md5=b9cb99864d2adcf9d4d092a715a269b2},
 id = {cb486db4-1972-3c4f-b3df-c3d73b330caa},
 created = {2016-02-15T08:58:11.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 private_publication = {false},
 abstract = {We have given an extensive survey of the testing theory for probabilistic systems and presented the definitions of different preorders in a uniform style to ease the task of establishing relationships between them. Moreover we saw that in most cases the relations are closely connected with the classical testing relation of De Nicola and Hennessy (see Figure 9.14, page 265) and we discussed characterizations to better reflect the nature of the relations (see Figure 9.15, page 270). Table 9.1 summarizes the main contents of this chapter. Computational issues: Most authors do not not address computational issues, but from the summary table we can see that some of the relations are decidable. First, consider the characterization by extended traces. If the process is finite, we can determine the (finite) set of extended traces with a non-zero probability and compute the probability of each extended trace with the inductive definitions of section 9.11.1. Christoff presents algorithms for verification of his testing relations in [CC91]. Furthermore, we have a characterization by probabilistic bisimulation that can be computed in polynomial time and space by a partitioning technique [HT92]. To the best of our knowledge, for all other relations no algorithms computing them exist. Open problems: • We have only pointed out the most obvious connections between the different preorders presented here. Clarifying which relations are incomparable and which are finer/coarser than others would be helpful to obtain a more complete picture on probabilistic testing relations. For example, the relationship between the following pairs of relations has not been considered yet: (⊆CL, ⊆CL), (⊆CL, ⊆JY), (⊆CHwte, ⊆BC) and the ⊆LS with any of the "compositional testing relations". • Many relations are not computable because infinite sets of test processes have to be applied, so an interesting problem would be finding the set of "essential" test processes that decide whether two processes are related or not. A good starting point would be defining the "informativeness" of a test process with regard to the tested process. Of course, test processes should be as compact as possible avoiding unnecessary computations. © Springer-Verlag Berlin Heidelberg 2005.},
 bibtype = {article},
 author = {Wolf, V},
 journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}
}

We have given an extensive survey of the testing theory for probabilistic systems and presented the definitions of different preorders in a uniform style to ease the task of establishing relationships between them. Moreover we saw that in most cases the relations are closely connected with the classical testing relation of De Nicola and Hennessy (see Figure 9.14, page 265) and we discussed characterizations to better reflect the nature of the relations (see Figure 9.15, page 270). Table 9.1 summarizes the main contents of this chapter. Computational issues: Most authors do not not address computational issues, but from the summary table we can see that some of the relations are decidable. First, consider the characterization by extended traces. If the process is finite, we can determine the (finite) set of extended traces with a non-zero probability and compute the probability of each extended trace with the inductive definitions of section 9.11.1. Christoff presents algorithms for verification of his testing relations in [CC91]. Furthermore, we have a characterization by probabilistic bisimulation that can be computed in polynomial time and space by a partitioning technique [HT92]. To the best of our knowledge, for all other relations no algorithms computing them exist. Open problems: • We have only pointed out the most obvious connections between the different preorders presented here. Clarifying which relations are incomparable and which are finer/coarser than others would be helpful to obtain a more complete picture on probabilistic testing relations. For example, the relationship between the following pairs of relations has not been considered yet: (⊆CL, ⊆CL), (⊆CL, ⊆JY), (⊆CHwte, ⊆BC) and the ⊆LS with any of the "compositional testing relations". • Many relations are not computable because infinite sets of test processes have to be applied, so an interesting problem would be finding the set of "essential" test processes that decide whether two processes are related or not. A good starting point would be defining the "informativeness" of a test process with regard to the tested process. Of course, test processes should be as compact as possible avoiding unnecessary computations. © Springer-Verlag Berlin Heidelberg 2005.

@article{
 title = {Comparative branching-time semantics for Markov chains},
 type = {article},
 year = {2005},
 pages = {149-214},
 volume = {200},
 websites = {http://www.sciencedirect.com/science/article/pii/S0890540105000441},
 publisher = {Elsevier},
 id = {b52099dd-a8ff-36b2-8677-2fa31b1bcb9d},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {BKHW05},
 source_type = {article},
 private_publication = {false},
 abstract = {This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship.},
 bibtype = {article},
 author = {Baier, C and Katoen, J.-P. and Hermanns, H and Wolf, V},
 journal = {Information and Computation}
}

This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship.

@inproceedings{
 title = {Trace machines for observing continuous-time Markov chains},
 type = {inproceedings},
 year = {2004},
 pages = {259-277},
 volume = {153},
 publisher = {Elsevier},
 series = {Electronic Notes in Theoretical Computer Science},
 id = {ca284220-539d-3681-9d85-e0ce93d7b701},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {WBM06},
 source_type = {inproceedings},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Wolf, V and Baier, C and Majster-Cederbaum, M},
 booktitle = {Proceedings of the International Workshop on Quantitative Aspects of Programming Languages (QAPL'04)}
}

@misc{
 title = {Bisimulation und Simulation für Markovmodelle},
 type = {misc},
 year = {2003},
 institution = {University of Bonn},
 id = {b8af1fac-237f-3eb4-9b1d-07df9812147f},
 created = {2016-02-15T08:58:38.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {DiplomWolf},
 source_type = {other},
 notes = {Diploma thesis},
 private_publication = {false},
 bibtype = {misc},
 author = {Wolf, V}
}

@inproceedings{
 title = {Comparative Branching Time Semantics for Markov Chains},
 type = {inproceedings},
 year = {2003},
 pages = {492-508},
 volume = {2761},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 id = {09f9d30e-c665-3be1-8194-d2b9712d3bfe},
 created = {2016-02-15T08:58:39.000Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-03-22T13:51:34.979Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {BKHW03},
 source_type = {inproceedings},
 private_publication = {false},
 bibtype = {inproceedings},
 author = {Baier, C and Katoen, J.-P. and Hermanns, H and Wolf, V},
 booktitle = {Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03)}
}

@book{
 title = {Comparative branching-time semantics for Markov chains (extended abstract)},
 type = {book},
 year = {2003},
 source = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
 volume = {2761},
 id = {37133f37-2c84-3b70-ab32-118413b61ccd},
 created = {2017-12-21T13:50:26.393Z},
 file_attached = {false},
 profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
 last_modified = {2017-12-21T13:50:26.393Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {false},
 hidden = {false},
 private_publication = {false},
 abstract = {This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterised in terms of the temporal logics PCTL and CSL. Apart from presenting various existing branching-time relations in a uniform manner, our contributions are: (i) weak simulation for DTMCs is defined, (ii) weak bisimulation equivalence is shown to coincide with weak simulation equivalence, (iii) logical characterisation of weak (bi)simulations are provided, and (iv) a classification of branching-time relations is presented, elucidating the semantics of DTMCs, CTMCs and their interrelation. © Springer-Verlag Berlin Heidelberg 2003.},
 bibtype = {book},
 author = {Baier, C. and Hermanns, H. and Katoen, J.-P. and Wolf, V.}
}

This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterised in terms of the temporal logics PCTL and CSL. Apart from presenting various existing branching-time relations in a uniform manner, our contributions are: (i) weak simulation for DTMCs is defined, (ii) weak bisimulation equivalence is shown to coincide with weak simulation equivalence, (iii) logical characterisation of weak (bi)simulations are provided, and (iv) a classification of branching-time relations is presented, elucidating the semantics of DTMCs, CTMCs and their interrelation. © Springer-Verlag Berlin Heidelberg 2003.