Informatik und Informationswissenschafthttp://kops.uni-konstanz.de:80/handle/123456789/362018-04-24T02:37:04Z2018-04-24T02:37:04ZLinear Distances between Markov ChainsDaca, PrzemyslawHenzinger, Thomas A.Kretínský, JanPetrov, Tatjanapop516560Desharnais, JoséeJagadeesan, Radha123456789/421392018-04-24T01:14:47Z2016Linear Distances between Markov Chains
Daca, Przemyslaw; Henzinger, Thomas A.; Kretínský, Jan; Petrov, Tatjana
We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results.
2016Daca, PrzemyslawHenzinger, Thomas A.Kretínský, JanPetrov, Tatjana004We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results.Schloss Dagstuhl, Leibniz-Zentrum für Informatik GmbHDesharnais, JoséeJagadeesan, RadhaINPROCEEDINGSeng10.4230/LIPIcs.CONCUR.2016.20LIPIcs : Leibniz International Proceedings in Informatics59978-3-95977-017-01868-896927th International Conference on Concurrency Theory : CONCUR'162018-04-23T15:20:37+02:00123456789/3627th International Conference on Concurrency Theory : CONCUR'16 / Desharnais, Josée; Jagadeesan, Radha (Hrsg.). - Saarbrücken/Wadern : Schloss Dagstuhl, Leibniz-Zentrum für Informatik GmbH, 2016. - (LIPIcs : Leibniz International Proceedings in Informatics ; 59). - 20. - ISSN 1868-8969. - ISBN 978-3-95977-017-0Québec City, Canada2016-08-23Saarbrücken/Wadern27th International Conference on Concurrency Theory : CONCUR 20162016-08-262018-04-23T13:20:37ZEfficient Reduction of Kappa Models by Static Inspection of the Rule-SetBeica, AndreeaGuet, Calin C.Petrov, Tatjanapop516560Abate, AlessandroSafranek, David123456789/421382018-04-24T01:14:40Z2016-01-10Efficient Reduction of Kappa Models by Static Inspection of the Rule-Set
Beica, Andreea; Guet, Calin C.; Petrov, Tatjana
When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations.<br />Our algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude.
2016-01-10Beica, AndreeaGuet, Calin C.Petrov, Tatjana004When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations.<br />Our algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude.SpringerAbate, AlessandroSafranek, DavidINPROCEEDINGSeng10.1007/978-3-319-26916-0_10Lecture Notes in Bioinformatics9271978-3-319-26915-30302-97431611-3349173191Hybrid Systems Biology : Fourth International Workshop2018-04-23T14:53:10+02:00123456789/36Hybrid Systems Biology : Fourth International Workshop / Abate, Alessandro; Safranek, David (Hrsg.). - Cham : Springer, 2016. - (Lecture Notes in Bioinformatics ; 9271). - S. 173-191. - ISSN 0302-9743. - eISSN 1611-3349. - ISBN 978-3-319-26915-3Madrid, Spain2015-09-04Cham4th International Workshop on Hybrid Systems Biology : HSB 20152015-09-052018-04-23T12:53:10ZLumpability abstractions of rule-based systemsFeret, JeromeHenzinger, ThomasKoeppl, HeinzPetrov, Tatjanapop516560123456789/421372018-04-24T01:14:35Z2012-05Lumpability abstractions of rule-based systems
Feret, Jerome; Henzinger, Thomas; Koeppl, Heinz; Petrov, Tatjana
The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the combinatorial complexity by quotienting the reachable set of molecular species into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently, we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper, we prove that this quotienting yields a sufficient condition for weak lumpability (that is to say that the quotient system is still Markovian for a given set of initial distributions) and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system (which means that the conditional probability of being in a given state in the original system knowing that we are in its equivalence class is an invariant of the system). We illustrate the framework on a case study of the epidermal growth factor (EGF)/insulin receptor crosstalk.
2012-05Feret, JeromeHenzinger, ThomasKoeppl, HeinzPetrov, Tatjana004The induction of a signaling pathway is characterized by transient complex formation and mutual posttranslational modification of proteins. To faithfully capture this combinatorial process in a mathematical model is an important challenge in systems biology. Exploiting the limited context on which most binding and modification events are conditioned, attempts have been made to reduce the combinatorial complexity by quotienting the reachable set of molecular species into species aggregates while preserving the deterministic semantics of the thermodynamic limit. Recently, we proposed a quotienting that also preserves the stochastic semantics and that is complete in the sense that the semantics of individual species can be recovered from the aggregate semantics. In this paper, we prove that this quotienting yields a sufficient condition for weak lumpability (that is to say that the quotient system is still Markovian for a given set of initial distributions) and that it gives rise to a backward Markov bisimulation between the original and aggregated transition system (which means that the conditional probability of being in a given state in the original system knowing that we are in its equivalence class is an invariant of the system). We illustrate the framework on a case study of the epidermal growth factor (EGF)/insulin receptor crosstalk.JOURNAL_ARTICLEeng10.1016/j.tcs.2011.12.0590304-39751879-2294137164431Theoretical Computer Science2018-04-23T13:50:12+02:00123456789/36Theoretical Computer Science ; 431 (2012). - S. 137-164. - ISSN 0304-3975. - eISSN 1879-22942018-04-23T11:50:12ZStochastic Semantics of Signaling as a Composition of Agent-view AutomataKoeppl, HeinzPetrov, Tatjanapop516560123456789/421362018-04-24T01:14:32Z2011-05Stochastic Semantics of Signaling as a Composition of Agent-view Automata
Koeppl, Heinz; Petrov, Tatjana
In this paper we present a formalism based on stochastic automata to describe the stochastic dynamics of signal transduction networks that are specified by rule-sets. Our formalism gives a modular description of the underlying stochastic process, in the sense that it is a composition of smaller units, agent-views. The view of an agent is an automaton that identifies all local modification changes of that agent (internal state modifications, binding and unbinding), but also those of interacting agents, which are tested within the same rule. We show how to represent the generator matrix of the underlying Markov process of the whole rule-set as Kronecker sums of the rate matrices belonging to individual view-automata. In the absence of birth the automata are finite, since the number of different contexts in which one agent can appear in a rule-set is finite. We illustrate the framework by an example that is related to cellular signaling events.
2011-05Koeppl, HeinzPetrov, Tatjana004In this paper we present a formalism based on stochastic automata to describe the stochastic dynamics of signal transduction networks that are specified by rule-sets. Our formalism gives a modular description of the underlying stochastic process, in the sense that it is a composition of smaller units, agent-views. The view of an agent is an automaton that identifies all local modification changes of that agent (internal state modifications, binding and unbinding), but also those of interacting agents, which are tested within the same rule. We show how to represent the generator matrix of the underlying Markov process of the whole rule-set as Kronecker sums of the rate matrices belonging to individual view-automata. In the absence of birth the automata are finite, since the number of different contexts in which one agent can appear in a rule-set is finite. We illustrate the framework by an example that is related to cellular signaling events.JOURNAL_ARTICLEeng10.1016/j.entcs.2011.04.0021571-0661317272Electronic Notes in Theoretical Computer Science2018-04-23T13:45:32+02:00123456789/36Electronic Notes in Theoretical Computer Science ; 272 (2011). - S. 3-17. - ISSN 1571-06612018-04-23T11:45:32Z