---
_id: '7147'
abstract:
- lang: eng
  text: "The expression of a gene is characterised by its transcription factors and
    the function processing them. If the transcription factors are not affected by
    gene products, the regulating function is often represented as a combinational
    logic circuit, where the outputs (product) are determined by current input values
    (transcription factors) only, and are hence independent on their relative arrival
    times. However, the simultaneous arrival of transcription factors (TFs) in genetic
    circuits is a strong assumption, given that the processes of transcription and
    translation of a gene into a protein introduce intrinsic time delays and that
    there is no global synchronisation among the arrival times of different molecular
    species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally
    implementable genetic circuit with two inputs and a single output, such that,
    in presence of small delays in input arrival, the circuit exhibits qualitatively
    distinct observable phenotypes. In particular, these phenotypes are long lived
    transients: they all converge to a single value, but so slowly, that they seem
    stable for an extended time period, longer than typical experiment duration. We
    used rule-based language to prototype our circuit, and we implemented a search
    for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe
    behaviour of our prototype circuit has wide implications. First, it suggests that
    GRNs can exploit event timing to create phenotypes. Second, it opens the possibility
    that GRNs are using event timing to react to stimuli and memorise events, without
    explicit feedback in regulation. From the modelling perspective, our prototype
    circuit demonstrates the critical importance of analysing the transient dynamics
    at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Calin C
  full_name: Guet, Calin C
  id: 47F8433E-F248-11E8-B48F-1D18A9856A87
  last_name: Guet
  orcid: 0000-0001-6220-2052
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Claudia
  full_name: Igler, Claudia
  id: 46613666-F248-11E8-B48F-1D18A9856A87
  last_name: Igler
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
- first_name: Ali
  full_name: Sezgin, Ali
  id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
  last_name: Sezgin
citation:
  ama: 'Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene
    regulation. In: <i>17th International Conference on Computational Methods in Systems
    Biology</i>. Vol 11773. Springer Nature; 2019:155-187. doi:<a href="https://doi.org/10.1007/978-3-030-31304-3_9">10.1007/978-3-030-31304-3_9</a>'
  apa: 'Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., &#38; Sezgin, A. (2019).
    Transient memory in gene regulation. In <i>17th International Conference on Computational
    Methods in Systems Biology</i> (Vol. 11773, pp. 155–187). Trieste, Italy: Springer
    Nature. <a href="https://doi.org/10.1007/978-3-030-31304-3_9">https://doi.org/10.1007/978-3-030-31304-3_9</a>'
  chicago: Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali
    Sezgin. “Transient Memory in Gene Regulation.” In <i>17th International Conference
    on Computational Methods in Systems Biology</i>, 11773:155–87. Springer Nature,
    2019. <a href="https://doi.org/10.1007/978-3-030-31304-3_9">https://doi.org/10.1007/978-3-030-31304-3_9</a>.
  ieee: C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient
    memory in gene regulation,” in <i>17th International Conference on Computational
    Methods in Systems Biology</i>, Trieste, Italy, 2019, vol. 11773, pp. 155–187.
  ista: 'Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory
    in gene regulation. 17th International Conference on Computational Methods in
    Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773,
    155–187.'
  mla: Guet, Calin C., et al. “Transient Memory in Gene Regulation.” <i>17th International
    Conference on Computational Methods in Systems Biology</i>, vol. 11773, Springer
    Nature, 2019, pp. 155–87, doi:<a href="https://doi.org/10.1007/978-3-030-31304-3_9">10.1007/978-3-030-31304-3_9</a>.
  short: C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International
    Conference on Computational Methods in Systems Biology, Springer Nature, 2019,
    pp. 155–187.
conference:
  end_date: 2019-09-20
  location: Trieste, Italy
  name: 'CMSB: Computational Methods in Systems Biology'
  start_date: 2019-09-18
date_created: 2019-12-04T16:07:50Z
date_published: 2019-09-17T00:00:00Z
date_updated: 2023-09-06T11:18:08Z
day: '17'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-030-31304-3_9
external_id:
  isi:
  - '000557875100009'
intvolume: '     11773'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 155-187
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 251EE76E-B435-11E9-9278-68D0E5697425
  grant_number: '24573'
  name: Design principles underlying genetic switch architecture
publication: 17th International Conference on Computational Methods in Systems Biology
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783030313036'
  - '9783030313043'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Transient memory in gene regulation
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11773
year: '2019'
...
---
_id: '471'
abstract:
- lang: eng
  text: 'We present a new algorithm for the statistical model checking of Markov chains
    with respect to unbounded temporal properties, including full linear temporal
    logic. The main idea is that we monitor each simulation run on the fly, in order
    to detect quickly if a bottom strongly connected component is entered with high
    probability, in which case the simulation run can be terminated early. As a result,
    our simulation runs are often much shorter than required by termination bounds
    that are computed a priori for a desired level of confidence on a large state
    space. In comparison to previous algorithms for statistical model checking our
    method is not only faster in many cases but also requires less information about
    the system, namely, only the minimum transition probability that occurs in the
    Markov chain. In addition, our method can be generalised to unbounded quantitative
    properties such as mean-payoff bounds. '
article_number: '12'
author:
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
    for unbounded temporal properties. <i>ACM Transactions on Computational Logic
    (TOCL)</i>. 2017;18(2). doi:<a href="https://doi.org/10.1145/3060139">10.1145/3060139</a>
  apa: Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster
    statistical model checking for unbounded temporal properties. <i>ACM Transactions
    on Computational Logic (TOCL)</i>. ACM. <a href="https://doi.org/10.1145/3060139">https://doi.org/10.1145/3060139</a>
  chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
    “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM
    Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href="https://doi.org/10.1145/3060139">https://doi.org/10.1145/3060139</a>.
  ieee: P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
    model checking for unbounded temporal properties,” <i>ACM Transactions on Computational
    Logic (TOCL)</i>, vol. 18, no. 2. ACM, 2017.
  ista: Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model
    checking for unbounded temporal properties. ACM Transactions on Computational
    Logic (TOCL). 18(2), 12.
  mla: Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal
    Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no.
    2, 12, ACM, 2017, doi:<a href="https://doi.org/10.1145/3060139">10.1145/3060139</a>.
  short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational
    Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:39Z
date_published: 2017-05-01T00:00:00Z
date_updated: 2023-02-21T16:48:11Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3060139
ec_funded: 1
intvolume: '        18'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1504.05739
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
  issn:
  - '15293785'
publication_status: published
publisher: ACM
publist_id: '7349'
quality_controlled: '1'
related_material:
  record:
  - id: '1234'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '1351'
abstract:
- lang: eng
  text: The behaviour of gene regulatory networks (GRNs) is typically analysed using
    simulation-based statistical testing-like methods. In this paper, we demonstrate
    that we can replace this approach by a formal verification-like method that gives
    higher assurance and scalability. We focus on Wagner’s weighted GRN model with
    varying weights, which is used in evolutionary biology. In the model, weight parameters
    represent the gene interaction strength that may change due to genetic mutations.
    For a property of interest, we synthesise the constraints over the parameter space
    that represent the set of GRNs satisfying the property. We experimentally show
    that our parameter synthesis procedure computes the mutational robustness of GRNs—an
    important problem of interest in evolutionary biology—more efficiently than the
    classical simulation method. We specify the property in linear temporal logic.
    We employ symbolic bounded model checking and SMT solving to compute the space
    of GRNs that satisfy the property, which amounts to synthesizing a set of linear
    constraints on the weights.
article_processing_charge: No
author:
- first_name: Mirco
  full_name: Giacobbe, Mirco
  id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
  last_name: Giacobbe
  orcid: 0000-0001-8180-0904
- first_name: Calin C
  full_name: Guet, Calin C
  id: 47F8433E-F248-11E8-B48F-1D18A9856A87
  last_name: Guet
  orcid: 0000-0001-6220-2052
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Tiago
  full_name: Paixao, Tiago
  id: 2C5658E6-F248-11E8-B48F-1D18A9856A87
  last_name: Paixao
  orcid: 0000-0003-2361-3953
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking
    the evolution of gene regulatory networks. <i>Acta Informatica</i>. 2017;54(8):765-787.
    doi:<a href="https://doi.org/10.1007/s00236-016-0278-x">10.1007/s00236-016-0278-x</a>
  apa: Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38; Petrov,
    T. (2017). Model checking the evolution of gene regulatory networks. <i>Acta Informatica</i>.
    Springer. <a href="https://doi.org/10.1007/s00236-016-0278-x">https://doi.org/10.1007/s00236-016-0278-x</a>
  chicago: Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago
    Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.”
    <i>Acta Informatica</i>. Springer, 2017. <a href="https://doi.org/10.1007/s00236-016-0278-x">https://doi.org/10.1007/s00236-016-0278-x</a>.
  ieee: M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov,
    “Model checking the evolution of gene regulatory networks,” <i>Acta Informatica</i>,
    vol. 54, no. 8. Springer, pp. 765–787, 2017.
  ista: Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model
    checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.
  mla: Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.”
    <i>Acta Informatica</i>, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:<a href="https://doi.org/10.1007/s00236-016-0278-x">10.1007/s00236-016-0278-x</a>.
  short: M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta
    Informatica 54 (2017) 765–787.
date_created: 2018-12-11T11:51:32Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2025-05-28T11:57:04Z
day: '01'
ddc:
- '006'
- '576'
department:
- _id: ToHe
- _id: CaGu
- _id: NiBa
doi: 10.1007/s00236-016-0278-x
ec_funded: 1
external_id:
  isi:
  - '000414343200003'
file:
- access_level: open_access
  checksum: 4e661d9135d7f8c342e8e258dee76f3e
  content_type: application/pdf
  creator: dernst
  date_created: 2019-01-17T15:57:29Z
  date_updated: 2020-07-14T12:44:46Z
  file_id: '5841'
  file_name: 2017_ActaInformatica_Giacobbe.pdf
  file_size: 755241
  relation: main_file
file_date_updated: 2020-07-14T12:44:46Z
has_accepted_license: '1'
intvolume: '        54'
isi: 1
issue: '8'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '12'
oa: 1
oa_version: Published Version
page: 765 - 787
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25B1EC9E-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '618091'
  name: Speed of Adaptation in Population Genetics and Evolutionary Computation
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _id: 25B07788-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '250152'
  name: Limits to selection in biology and in evolutionary computation
publication: Acta Informatica
publication_identifier:
  issn:
  - '00015903'
publication_status: published
publisher: Springer
publist_id: '5898'
pubrep_id: '649'
quality_controlled: '1'
related_material:
  record:
  - id: '1835'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Model checking the evolution of gene regulatory networks
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 54
year: '2017'
...
---
_id: '1093'
abstract:
- lang: eng
  text: '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. '
acknowledgement: "This research was funded in part by the European Research Council
  (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF)
  under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award),
  by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced
  Postdoc. Mobility Fellowship – grant number P300P2_161067."
alternative_title:
- LIPIcs
article_number: '20'
author:
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov
    chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a
    href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.20">10.4230/LIPIcs.CONCUR.2016.20</a>'
  apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Linear
    distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency
    Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
    <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.20">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>'
  chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
    “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2016. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.20">https://doi.org/10.4230/LIPIcs.CONCUR.2016.20</a>.
  ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances
    between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City;
    Canada, 2016, vol. 59.'
  ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between
    Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.'
  mla: Daca, Przemyslaw, et al. <i>Linear Distances between Markov Chains</i>. Vol.
    59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.20">10.4230/LIPIcs.CONCUR.2016.20</a>.
  short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl -
    Leibniz-Zentrum für Informatik, 2016.
conference:
  end_date: 2016-08-26
  location: Quebec City; Canada
  name: 'CONCUR: Concurrency Theory'
  start_date: 2016-08-23
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
- _id: CaGu
doi: 10.4230/LIPIcs.CONCUR.2016.20
ec_funded: 1
file:
- access_level: open_access
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:39Z
  date_updated: 2018-12-12T10:11:39Z
  file_id: '4895'
  file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf
  file_size: 501827
  relation: main_file
file_date_updated: 2018-12-12T10:11:39Z
has_accepted_license: '1'
intvolume: '        59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6283'
pubrep_id: '794'
quality_controlled: '1'
related_material:
  record:
  - id: '1155'
    relation: dissertation_contains
    status: public
scopus_import: 1
status: public
title: Linear distances between Markov chains
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1524'
abstract:
- lang: eng
  text: "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.\r\nOur 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."
acknowledgement: This research was supported by the People Programme (Marie Curie
  Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under
  REA grant agreement no. 291734, and the SNSF Early Postdoc.Mobility Fellowship,
  the grant number P2EZP2_148797.
alternative_title:
- LNCS
author:
- first_name: Andreea
  full_name: Beica, Andreea
  last_name: Beica
- first_name: Calin C
  full_name: Guet, Calin C
  id: 47F8433E-F248-11E8-B48F-1D18A9856A87
  last_name: Guet
  orcid: 0000-0001-6220-2052
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: 'Beica A, Guet CC, Petrov T. Efficient reduction of kappa models by static
    inspection of the rule-set. In: Vol 9271. Springer; 2016:173-191. doi:<a href="https://doi.org/10.1007/978-3-319-26916-0_10">10.1007/978-3-319-26916-0_10</a>'
  apa: 'Beica, A., Guet, C. C., &#38; Petrov, T. (2016). Efficient reduction of kappa
    models by static inspection of the rule-set (Vol. 9271, pp. 173–191). Presented
    at the HSB: Hybrid Systems Biology, Madrid, Spain: Springer. <a href="https://doi.org/10.1007/978-3-319-26916-0_10">https://doi.org/10.1007/978-3-319-26916-0_10</a>'
  chicago: Beica, Andreea, Calin C Guet, and Tatjana Petrov. “Efficient Reduction
    of Kappa Models by Static Inspection of the Rule-Set,” 9271:173–91. Springer,
    2016. <a href="https://doi.org/10.1007/978-3-319-26916-0_10">https://doi.org/10.1007/978-3-319-26916-0_10</a>.
  ieee: 'A. Beica, C. C. Guet, and T. Petrov, “Efficient reduction of kappa models
    by static inspection of the rule-set,” presented at the HSB: Hybrid Systems Biology,
    Madrid, Spain, 2016, vol. 9271, pp. 173–191.'
  ista: 'Beica A, Guet CC, Petrov T. 2016. Efficient reduction of kappa models by
    static inspection of the rule-set. HSB: Hybrid Systems Biology, LNCS, vol. 9271,
    173–191.'
  mla: Beica, Andreea, et al. <i>Efficient Reduction of Kappa Models by Static Inspection
    of the Rule-Set</i>. Vol. 9271, Springer, 2016, pp. 173–91, doi:<a href="https://doi.org/10.1007/978-3-319-26916-0_10">10.1007/978-3-319-26916-0_10</a>.
  short: A. Beica, C.C. Guet, T. Petrov, in:, Springer, 2016, pp. 173–191.
conference:
  end_date: 2015-09-05
  location: Madrid, Spain
  name: 'HSB: Hybrid Systems Biology'
  start_date: 2015-09-04
date_created: 2018-12-11T11:52:31Z
date_published: 2016-01-10T00:00:00Z
date_updated: 2021-01-12T06:51:22Z
day: '10'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/978-3-319-26916-0_10
ec_funded: 1
intvolume: '      9271'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1501.00440
month: '01'
oa: 1
oa_version: Preprint
page: 173 - 191
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5649'
quality_controlled: '1'
scopus_import: 1
status: public
title: Efficient reduction of kappa models by static inspection of the rule-set
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9271
year: '2016'
...
---
_id: '1234'
abstract:
- lang: eng
  text: We present a new algorithm for the statistical model checking of Markov chains
    with respect to unbounded temporal properties, including full linear temporal
    logic. The main idea is that we monitor each simulation run on the fly, in order
    to detect quickly if a bottom strongly connected component is entered with high
    probability, in which case the simulation run can be terminated early. As a result,
    our simulation runs are often much shorter than required by termination bounds
    that are computed a priori for a desired level of confidence on a large state
    space. In comparison to previous algorithms for statistical model checking our
    method is not only faster in many cases but also requires less information about
    the system, namely, only the minimum transition probability that occurs in the
    Markov chain. In addition, our method can be generalised to unbounded quantitative
    properties such as mean-payoff bounds.
acknowledgement: "This research was funded in part by the European Research Council
  (ERC) under\r\ngrant  agreement  267989  (QUAREM),  the  Austrian  Science  Fund
  \ (FWF)  under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
  the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh
  Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility
  Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation
  under grant agreement P202/12/G061."
alternative_title:
- LNCS
author:
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
    for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:<a
    href="https://doi.org/10.1007/978-3-662-49674-9_7">10.1007/978-3-662-49674-9_7</a>'
  apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Faster
    statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129).
    Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
    of Systems, Eindhoven, The Netherlands: Springer. <a href="https://doi.org/10.1007/978-3-662-49674-9_7">https://doi.org/10.1007/978-3-662-49674-9_7</a>'
  chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
    “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29.
    Springer, 2016. <a href="https://doi.org/10.1007/978-3-662-49674-9_7">https://doi.org/10.1007/978-3-662-49674-9_7</a>.
  ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
    model checking for unbounded temporal properties,” presented at the TACAS: Tools
    and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands,
    2016, vol. 9636, pp. 112–129.'
  ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model
    checking for unbounded temporal properties. TACAS: Tools and Algorithms for the
    Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.'
  mla: Daca, Przemyslaw, et al. <i>Faster Statistical Model Checking for Unbounded
    Temporal Properties</i>. Vol. 9636, Springer, 2016, pp. 112–29, doi:<a href="https://doi.org/10.1007/978-3-662-49674-9_7">10.1007/978-3-662-49674-9_7</a>.
  short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp.
    112–129.
conference:
  end_date: 2016-04-08
  location: Eindhoven, The Netherlands
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2016-04-02
date_created: 2018-12-11T11:50:51Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1007/978-3-662-49674-9_7
ec_funded: 1
intvolume: '      9636'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1504.05739
month: '01'
oa: 1
oa_version: Preprint
page: 112 - 129
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '6099'
quality_controlled: '1'
related_material:
  record:
  - id: '471'
    relation: later_version
    status: public
  - id: '1155'
    relation: dissertation_contains
    status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9636
year: '2016'
...
---
_id: '1835'
abstract:
- lang: eng
  text: The behaviour of gene regulatory networks (GRNs) is typically analysed using
    simulation-based statistical testing-like methods. In this paper, we demonstrate
    that we can replace this approach by a formal verification-like method that gives
    higher assurance and scalability. We focus on Wagner’s weighted GRN model with
    varying weights, which is used in evolutionary biology. In the model, weight parameters
    represent the gene interaction strength that may change due to genetic mutations.
    For a property of interest, we synthesise the constraints over the parameter space
    that represent the set of GRNs satisfying the property. We experimentally show
    that our parameter synthesis procedure computes the mutational robustness of GRNs
    –an important problem of interest in evolutionary biology– more efficiently than
    the classical simulation method. We specify the property in linear temporal logics.
    We employ symbolic bounded model checking and SMT solving to compute the space
    of GRNs that satisfy the property, which amounts to synthesizing a set of linear
    constraints on the weights.
acknowledgement: "SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2
  148797.\r\n"
alternative_title:
- LNCS
author:
- first_name: Mirco
  full_name: Giacobbe, Mirco
  id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
  last_name: Giacobbe
  orcid: 0000-0001-8180-0904
- first_name: Calin C
  full_name: Guet, Calin C
  id: 47F8433E-F248-11E8-B48F-1D18A9856A87
  last_name: Guet
  orcid: 0000-0001-6220-2052
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Tiago
  full_name: Paixao, Tiago
  id: 2C5658E6-F248-11E8-B48F-1D18A9856A87
  last_name: Paixao
  orcid: 0000-0003-2361-3953
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking
    gene regulatory networks. 2015;9035:469-483. doi:<a href="https://doi.org/10.1007/978-3-662-46681-0_47">10.1007/978-3-662-46681-0_47</a>
  apa: 'Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., &#38;
    Petrov, T. (2015). Model checking gene regulatory networks. Presented at the TACAS:
    Tools and Algorithms for the Construction and Analysis of Systems, London, United
    Kingdom: Springer. <a href="https://doi.org/10.1007/978-3-662-46681-0_47">https://doi.org/10.1007/978-3-662-46681-0_47</a>'
  chicago: Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago
    Paixao, and Tatjana Petrov. “Model Checking Gene Regulatory Networks.” Lecture
    Notes in Computer Science. Springer, 2015. <a href="https://doi.org/10.1007/978-3-662-46681-0_47">https://doi.org/10.1007/978-3-662-46681-0_47</a>.
  ieee: M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov,
    “Model checking gene regulatory networks,” vol. 9035. Springer, pp. 469–483, 2015.
  ista: Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2015. Model
    checking gene regulatory networks. 9035, 469–483.
  mla: Giacobbe, Mirco, et al. <i>Model Checking Gene Regulatory Networks</i>. Vol.
    9035, Springer, 2015, pp. 469–83, doi:<a href="https://doi.org/10.1007/978-3-662-46681-0_47">10.1007/978-3-662-46681-0_47</a>.
  short: M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035
    (2015) 469–483.
conference:
  end_date: 2015-04-18
  location: London, United Kingdom
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2015-04-11
date_created: 2018-12-11T11:54:16Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2025-05-28T11:57:04Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
- _id: NiBa
doi: 10.1007/978-3-662-46681-0_47
ec_funded: 1
intvolume: '      9035'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1410.7704
month: '04'
oa: 1
oa_version: Preprint
page: 469 - 483
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25B1EC9E-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '618091'
  name: Speed of Adaptation in Population Genetics and Evolutionary Computation
- _id: 25B07788-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '250152'
  name: Limits to selection in biology and in evolutionary computation
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5267'
quality_controlled: '1'
related_material:
  record:
  - id: '1351'
    relation: later_version
    status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Model checking gene regulatory networks
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9035
year: '2015'
...
---
_id: '1840'
abstract:
- lang: eng
  text: In this paper, we present a method for reducing a regular, discrete-time Markov
    chain (DTMC) to another DTMC with a given, typically much smaller number of states.
    The cost of reduction is defined as the Kullback-Leibler divergence rate between
    a projection of the original process through a partition function and a DTMC on
    the correspondingly partitioned state space. Finding the reduced model with minimal
    cost is computationally expensive, as it requires an exhaustive search among all
    state space partitions, and an exact evaluation of the reduction cost for each
    candidate partition. Our approach deals with the latter problem by minimizing
    an upper bound on the reduction cost instead of minimizing the exact cost. The
    proposed upper bound is easy to compute and it is tight if the original chain
    is lumpable with respect to the partition. Then, we express the problem in the
    form of information bottleneck optimization, and propose using the agglomerative
    information bottleneck algorithm for searching a suboptimal partition greedily,
    rather than exhaustively. The theory is illustrated with examples and one application
    scenario in the context of modeling bio-molecular interactions.
acknowledgement: "This work was supported by the Austrian Research Association under
  Project 06/12684, by the Swiss National Science Foundation (SNSF) under Grant PP00P2
  128503/1, by the SystemsX.ch (the Swiss Inititative for Systems Biology), and by
  a SNSF Early Postdoc.Mobility Fellowship grant P2EZP2_148797.\r\n"
author:
- first_name: Bernhard
  full_name: Geiger, Bernhard
  last_name: Geiger
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
- first_name: Gernot
  full_name: Kubin, Gernot
  last_name: Kubin
- first_name: Heinz
  full_name: Koeppl, Heinz
  last_name: Koeppl
citation:
  ama: Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation
    via information bottleneck. <i>IEEE Transactions on Automatic Control</i>. 2015;60(4):1010-1022.
    doi:<a href="https://doi.org/10.1109/TAC.2014.2364971">10.1109/TAC.2014.2364971</a>
  apa: Geiger, B., Petrov, T., Kubin, G., &#38; Koeppl, H. (2015). Optimal Kullback-Leibler
    aggregation via information bottleneck. <i>IEEE Transactions on Automatic Control</i>.
    IEEE. <a href="https://doi.org/10.1109/TAC.2014.2364971">https://doi.org/10.1109/TAC.2014.2364971</a>
  chicago: Geiger, Bernhard, Tatjana Petrov, Gernot Kubin, and Heinz Koeppl. “Optimal
    Kullback-Leibler Aggregation via Information Bottleneck.” <i>IEEE Transactions
    on Automatic Control</i>. IEEE, 2015. <a href="https://doi.org/10.1109/TAC.2014.2364971">https://doi.org/10.1109/TAC.2014.2364971</a>.
  ieee: B. Geiger, T. Petrov, G. Kubin, and H. Koeppl, “Optimal Kullback-Leibler aggregation
    via information bottleneck,” <i>IEEE Transactions on Automatic Control</i>, vol.
    60, no. 4. IEEE, pp. 1010–1022, 2015.
  ista: Geiger B, Petrov T, Kubin G, Koeppl H. 2015. Optimal Kullback-Leibler aggregation
    via information bottleneck. IEEE Transactions on Automatic Control. 60(4), 1010–1022.
  mla: Geiger, Bernhard, et al. “Optimal Kullback-Leibler Aggregation via Information
    Bottleneck.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 4, IEEE,
    2015, pp. 1010–22, doi:<a href="https://doi.org/10.1109/TAC.2014.2364971">10.1109/TAC.2014.2364971</a>.
  short: B. Geiger, T. Petrov, G. Kubin, H. Koeppl, IEEE Transactions on Automatic
    Control 60 (2015) 1010–1022.
date_created: 2018-12-11T11:54:18Z
date_published: 2015-04-01T00:00:00Z
date_updated: 2021-01-12T06:53:33Z
day: '01'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1109/TAC.2014.2364971
intvolume: '        60'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1304.6603
month: '04'
oa: 1
oa_version: Preprint
page: 1010 - 1022
publication: IEEE Transactions on Automatic Control
publication_identifier:
  issn:
  - 0018-9286
publication_status: published
publisher: IEEE
publist_id: '5262'
quality_controlled: '1'
scopus_import: 1
status: public
title: Optimal Kullback-Leibler aggregation via information bottleneck
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 60
year: '2015'
...
---
_id: '1913'
abstract:
- lang: eng
  text: 'Deposits of phosphorylated tau protein and convergence of pathology in the
    hippocampus are the hallmarks of neurodegenerative tauopathies. Thus we aimed
    to evaluate whether regional and cellular vulnerability patterns in the hippocampus
    distinguish tauopathies or are influenced by their concomitant presence. Methods:
    We created a heat map of phospho-tau (AT8) immunoreactivity patterns in 24 hippocampal
    subregions/layers in individuals with Alzheimer''s disease (AD)-related neurofibrillary
    degeneration (n = 40), Pick''s disease (n = 8), progressive supranuclear palsy
    (n = 7), corticobasal degeneration (n = 6), argyrophilic grain disease (AGD, n
    = 18), globular glial tauopathy (n = 5), and tau-astrogliopathy of the elderly
    (n = 10). AT8 immunoreactivity patterns were compared by mathematical analysis.
    Results: Our study reveals disease-specific hot spots and regional selective vulnerability
    for these disorders. The pattern of hippocampal AD-related tau pathology is strongly
    influenced by concomitant AGD. Mathematical analysis reveals that hippocampal
    involvement in primary tauopathies is distinguishable from early-stage AD-related
    neurofibrillary degeneration. Conclusion: Our data demonstrate disease-specific
    AT8 immunoreactivity patterns and hot spots in the hippocampus even in tauopathies,
    which primarily do not affect the hippocampus. These hot spots can be shifted
    to other regions by the co-occurrence of tauopathies like AGD. Our observations
    support the notion that globular glial tauopathies and tau-astrogliopathy of the
    elderly are distinct entities.'
acknowledgement: This study was supported by the European Commission’s 7th Framework
  Programme under GA No. 278486, ‘DEVELAGE’.
article_processing_charge: No
article_type: original
author:
- first_name: Ivan
  full_name: Milenković, Ivan
  last_name: Milenković
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
- first_name: Gábor
  full_name: Kovács, Gábor
  last_name: Kovács
citation:
  ama: Milenković I, Petrov T, Kovács G. Patterns of hippocampal tau pathology differentiate
    neurodegenerative dementias. <i>Dementia and Geriatric Cognitive Disorders</i>.
    2014;38(5-6):375-388. doi:<a href="https://doi.org/10.1159/000365548">10.1159/000365548</a>
  apa: Milenković, I., Petrov, T., &#38; Kovács, G. (2014). Patterns of hippocampal
    tau pathology differentiate neurodegenerative dementias. <i>Dementia and Geriatric
    Cognitive Disorders</i>. Karger Publishers. <a href="https://doi.org/10.1159/000365548">https://doi.org/10.1159/000365548</a>
  chicago: Milenković, Ivan, Tatjana Petrov, and Gábor Kovács. “Patterns of Hippocampal
    Tau Pathology Differentiate Neurodegenerative Dementias.” <i>Dementia and Geriatric
    Cognitive Disorders</i>. Karger Publishers, 2014. <a href="https://doi.org/10.1159/000365548">https://doi.org/10.1159/000365548</a>.
  ieee: I. Milenković, T. Petrov, and G. Kovács, “Patterns of hippocampal tau pathology
    differentiate neurodegenerative dementias,” <i>Dementia and Geriatric Cognitive
    Disorders</i>, vol. 38, no. 5–6. Karger Publishers, pp. 375–388, 2014.
  ista: Milenković I, Petrov T, Kovács G. 2014. Patterns of hippocampal tau pathology
    differentiate neurodegenerative dementias. Dementia and Geriatric Cognitive Disorders.
    38(5–6), 375–388.
  mla: Milenković, Ivan, et al. “Patterns of Hippocampal Tau Pathology Differentiate
    Neurodegenerative Dementias.” <i>Dementia and Geriatric Cognitive Disorders</i>,
    vol. 38, no. 5–6, Karger Publishers, 2014, pp. 375–88, doi:<a href="https://doi.org/10.1159/000365548">10.1159/000365548</a>.
  short: I. Milenković, T. Petrov, G. Kovács, Dementia and Geriatric Cognitive Disorders
    38 (2014) 375–388.
date_created: 2018-12-11T11:54:41Z
date_published: 2014-11-07T00:00:00Z
date_updated: 2023-10-17T10:21:17Z
day: '07'
department:
- _id: CaGu
doi: 10.1159/000365548
external_id:
  pmid:
  - '25195847'
intvolume: '        38'
issue: 5-6
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://kops.uni-konstanz.de/bitstream/123456789/42127/1/Milenkovic_2-17ivylo2up0798.pdf
month: '11'
oa: 1
oa_version: Published Version
page: 375 - 388
pmid: 1
publication: Dementia and Geriatric Cognitive Disorders
publication_identifier:
  issn:
  - 1420-8008
publication_status: published
publisher: Karger Publishers
publist_id: '5181'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Patterns of hippocampal tau pathology differentiate neurodegenerative dementias
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 38
year: '2014'
...
---
_id: '2056'
abstract:
- lang: eng
  text: 'We consider a continuous-time Markov chain (CTMC) whose state space is partitioned
    into aggregates, and each aggregate is assigned a probability measure. A sufficient
    condition for defining a CTMC over the aggregates is presented as a variant of
    weak lumpability, which also characterizes that the measure over the original
    process can be recovered from that of the aggregated one. We show how the applicability
    of de-aggregation depends on the initial distribution. The application section
    is devoted to illustrate how the developed theory aids in reducing CTMC models
    of biochemical systems particularly in connection to protein-protein interactions.
    We assume that the model is written by a biologist in form of site-graph-rewrite
    rules. Site-graph-rewrite rules compactly express that, often, only a local context
    of a protein (instead of a full molecular species) needs to be in a certain configuration
    in order to trigger a reaction event. This observation leads to suitable aggregate
    Markov chains with smaller state spaces, thereby providing sufficient reduction
    in computational complexity. This is further exemplified in two case studies:
    simple unbounded polymerization and early EGFR/insulin crosstalk.'
acknowledgement: T. Petrov is supported by SystemsX.ch—the Swiss Inititative for Systems
  Biology.
author:
- first_name: Arnab
  full_name: Ganguly, Arnab
  last_name: Ganguly
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
- first_name: Heinz
  full_name: Koeppl, Heinz
  last_name: Koeppl
citation:
  ama: Ganguly A, Petrov T, Koeppl H. Markov chain aggregation and its applications
    to combinatorial reaction networks. <i>Journal of Mathematical Biology</i>. 2014;69(3):767-797.
    doi:<a href="https://doi.org/10.1007/s00285-013-0738-7">10.1007/s00285-013-0738-7</a>
  apa: Ganguly, A., Petrov, T., &#38; Koeppl, H. (2014). Markov chain aggregation
    and its applications to combinatorial reaction networks. <i>Journal of Mathematical
    Biology</i>. Springer. <a href="https://doi.org/10.1007/s00285-013-0738-7">https://doi.org/10.1007/s00285-013-0738-7</a>
  chicago: Ganguly, Arnab, Tatjana Petrov, and Heinz Koeppl. “Markov Chain Aggregation
    and Its Applications to Combinatorial Reaction Networks.” <i>Journal of Mathematical
    Biology</i>. Springer, 2014. <a href="https://doi.org/10.1007/s00285-013-0738-7">https://doi.org/10.1007/s00285-013-0738-7</a>.
  ieee: A. Ganguly, T. Petrov, and H. Koeppl, “Markov chain aggregation and its applications
    to combinatorial reaction networks,” <i>Journal of Mathematical Biology</i>, vol.
    69, no. 3. Springer, pp. 767–797, 2014.
  ista: Ganguly A, Petrov T, Koeppl H. 2014. Markov chain aggregation and its applications
    to combinatorial reaction networks. Journal of Mathematical Biology. 69(3), 767–797.
  mla: Ganguly, Arnab, et al. “Markov Chain Aggregation and Its Applications to Combinatorial
    Reaction Networks.” <i>Journal of Mathematical Biology</i>, vol. 69, no. 3, Springer,
    2014, pp. 767–97, doi:<a href="https://doi.org/10.1007/s00285-013-0738-7">10.1007/s00285-013-0738-7</a>.
  short: A. Ganguly, T. Petrov, H. Koeppl, Journal of Mathematical Biology 69 (2014)
    767–797.
date_created: 2018-12-11T11:55:28Z
date_published: 2014-11-20T00:00:00Z
date_updated: 2021-01-12T06:55:01Z
day: '20'
department:
- _id: CaGu
- _id: ToHe
doi: 10.1007/s00285-013-0738-7
intvolume: '        69'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1303.4532
month: '11'
oa: 1
oa_version: Submitted Version
page: 767 - 797
publication: Journal of Mathematical Biology
publication_status: published
publisher: Springer
publist_id: '4990'
quality_controlled: '1'
scopus_import: 1
status: public
title: Markov chain aggregation and its applications to combinatorial reaction networks
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 69
year: '2014'
...
---
_id: '3168'
abstract:
- lang: eng
  text: 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.
acknowledgement: "We would like to thank the anonymous reviewers for their comments
  on the different versions of the paper. We would also like to thank Ferdinanda Camporesi
  for her careful reading and the useful insights that she gave us about the paper.\r\nJérôme
  Feret’s contribution was partially supported by the AbstractCell ANR-Chair of Excellence.
  Heinz Koeppl’s research is supported by the Swiss National Science Foundation, grant
  no. 200020-117975/1. Tatjana Petrov’s research is supported by SystemsX.ch (the
  Swiss Initiative in Systems Biology)."
author:
- first_name: Jérôme
  full_name: Feret, Jérôme
  last_name: Feret
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Heinz
  full_name: Koeppl, Heinz
  last_name: Koeppl
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: Feret J, Henzinger TA, Koeppl H, Petrov T. Lumpability abstractions of rule
    based systems. <i>Theoretical Computer Science</i>. 2012;431:137-164. doi:<a href="https://doi.org/10.1016/j.tcs.2011.12.059">10.1016/j.tcs.2011.12.059</a>
  apa: Feret, J., Henzinger, T. A., Koeppl, H., &#38; Petrov, T. (2012). Lumpability
    abstractions of rule based systems. <i>Theoretical Computer Science</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.tcs.2011.12.059">https://doi.org/10.1016/j.tcs.2011.12.059</a>
  chicago: Feret, Jérôme, Thomas A Henzinger, Heinz Koeppl, and Tatjana Petrov. “Lumpability
    Abstractions of Rule Based Systems.” <i>Theoretical Computer Science</i>. Elsevier,
    2012. <a href="https://doi.org/10.1016/j.tcs.2011.12.059">https://doi.org/10.1016/j.tcs.2011.12.059</a>.
  ieee: J. Feret, T. A. Henzinger, H. Koeppl, and T. Petrov, “Lumpability abstractions
    of rule based systems,” <i>Theoretical Computer Science</i>, vol. 431. Elsevier,
    pp. 137–164, 2012.
  ista: Feret J, Henzinger TA, Koeppl H, Petrov T. 2012. Lumpability abstractions
    of rule based systems. Theoretical Computer Science. 431, 137–164.
  mla: Feret, Jérôme, et al. “Lumpability Abstractions of Rule Based Systems.” <i>Theoretical
    Computer Science</i>, vol. 431, Elsevier, 2012, pp. 137–64, doi:<a href="https://doi.org/10.1016/j.tcs.2011.12.059">10.1016/j.tcs.2011.12.059</a>.
  short: J. Feret, T.A. Henzinger, H. Koeppl, T. Petrov, Theoretical Computer Science
    431 (2012) 137–164.
date_created: 2018-12-11T12:01:47Z
date_published: 2012-05-04T00:00:00Z
date_updated: 2023-02-23T11:39:40Z
day: '04'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2011.12.059
intvolume: '       431'
language:
- iso: eng
month: '05'
oa_version: None
page: 137 - 164
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '3515'
pubrep_id: '73'
quality_controlled: '1'
related_material:
  record:
  - id: '3719'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Lumpability abstractions of rule based systems
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 431
year: '2012'
...
---
_id: '3719'
abstract:
- lang: eng
  text: 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 math- ematical 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 com- binatorial
    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 and that it gives rise to a
    backward Markov bisimulation between the original and aggregated transition system.
    We illustrate the framework on a case study of the EGF/insulin receptor crosstalk.
acknowledgement: Jérôme Feret’s contribution was partially supported by the ABSTRACTCELL
  ANR-Chair of Excellence. Heinz Koeppl acknowledges the support from the Swiss National
  Science Foundation, grant no. 200020-117975/1. Tatjana Petrov acknowledges the support
  from SystemsX.ch, the Swiss Initiative in Systems Biology.
alternative_title:
- EPTCS
arxiv: 1
author:
- first_name: Jérôme
  full_name: Feret, Jérôme
  last_name: Feret
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Heinz
  full_name: Koeppl, Heinz
  last_name: Koeppl
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: 'Feret J, Henzinger TA, Koeppl H, Petrov T. Lumpability abstractions of rule-based
    systems. In: Vol 40. Open Publishing Association; 2010:142-161.'
  apa: 'Feret, J., Henzinger, T. A., Koeppl, H., &#38; Petrov, T. (2010). Lumpability
    abstractions of rule-based systems (Vol. 40, pp. 142–161). Presented at the MECBIC:
    Membrane Computing and Biologically Inspired Process Calculi, Jena, Germany: Open
    Publishing Association.'
  chicago: Feret, Jérôme, Thomas A Henzinger, Heinz Koeppl, and Tatjana Petrov. “Lumpability
    Abstractions of Rule-Based Systems,” 40:142–61. Open Publishing Association, 2010.
  ieee: 'J. Feret, T. A. Henzinger, H. Koeppl, and T. Petrov, “Lumpability abstractions
    of rule-based systems,” presented at the MECBIC: Membrane Computing and Biologically
    Inspired Process Calculi, Jena, Germany, 2010, vol. 40, pp. 142–161.'
  ista: 'Feret J, Henzinger TA, Koeppl H, Petrov T. 2010. Lumpability abstractions
    of rule-based systems. MECBIC: Membrane Computing and Biologically Inspired Process
    Calculi, EPTCS, vol. 40, 142–161.'
  mla: Feret, Jérôme, et al. <i>Lumpability Abstractions of Rule-Based Systems</i>.
    Vol. 40, Open Publishing Association, 2010, pp. 142–61.
  short: J. Feret, T.A. Henzinger, H. Koeppl, T. Petrov, in:, Open Publishing Association,
    2010, pp. 142–161.
conference:
  end_date: 2010-08-23
  location: Jena, Germany
  name: 'MECBIC: Membrane Computing and Biologically Inspired Process Calculi'
  start_date: 2010-08-23
date_created: 2018-12-11T12:04:47Z
date_published: 2010-10-30T00:00:00Z
date_updated: 2023-02-23T11:15:19Z
day: '30'
ddc:
- '570'
department:
- _id: ToHe
- _id: CaGu
external_id:
  arxiv:
  - '1011.0496'
file:
- access_level: open_access
  checksum: eaaba991a86fff37606b0eb5196878e8
  content_type: application/pdf
  creator: kschuh
  date_created: 2019-01-31T12:09:09Z
  date_updated: 2020-07-14T12:46:14Z
  file_id: '5904'
  file_name: Lumpability_abstractions_of_rule-based_systems.pdf
  file_size: 907155
  relation: main_file
file_date_updated: 2020-07-14T12:46:14Z
has_accepted_license: '1'
intvolume: '        40'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 142-161
publication_status: published
publisher: Open Publishing Association
publist_id: '2511'
quality_controlled: '1'
related_material:
  record:
  - id: '3168'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Lumpability abstractions of rule-based systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 40
year: '2010'
...
---
_id: '4533'
abstract:
- lang: eng
  text: Interface theories have been proposed to support incremental design and independent
    implementability. Incremental design means that the compatibility checking of
    interfaces can proceed for partial system descriptions, without knowing the interfaces
    of all components. Independent implementability means that compatible interfaces
    can be refined separately, maintaining compatibility. We show that these interface
    theories provide no formal support for component reuse, meaning that the same
    component cannot be used to implement several different interfaces in a design.
    We add a new operation to interface theories in order to support such reuse. For
    example, different interfaces for the same component may refer to different aspects
    such as functionality, timing, and power consumption. We give both stateless and
    stateful examples for interface theories with component reuse. To illustrate component
    reuse in interface-based design, we show how the stateful theory provides a natural
    framework for specifying and refining PCI bus clients.
author:
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
- first_name: Tatjana
  full_name: Tatjana Petrov
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: 'Doyen L, Henzinger TA, Jobstmann B, Petrov T. Interface theories with component
    reuse. In: ACM; 2008:79-88. doi:<a href="https://doi.org/10.1145/1450058.1450070">10.1145/1450058.1450070</a>'
  apa: 'Doyen, L., Henzinger, T. A., Jobstmann, B., &#38; Petrov, T. (2008). Interface
    theories with component reuse (pp. 79–88). Presented at the EMSOFT: Embedded Software
    , ACM. <a href="https://doi.org/10.1145/1450058.1450070">https://doi.org/10.1145/1450058.1450070</a>'
  chicago: Doyen, Laurent, Thomas A Henzinger, Barbara Jobstmann, and Tatjana Petrov.
    “Interface Theories with Component Reuse,” 79–88. ACM, 2008. <a href="https://doi.org/10.1145/1450058.1450070">https://doi.org/10.1145/1450058.1450070</a>.
  ieee: 'L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov, “Interface theories
    with component reuse,” presented at the EMSOFT: Embedded Software , 2008, pp.
    79–88.'
  ista: 'Doyen L, Henzinger TA, Jobstmann B, Petrov T. 2008. Interface theories with
    component reuse. EMSOFT: Embedded Software , 79–88.'
  mla: Doyen, Laurent, et al. <i>Interface Theories with Component Reuse</i>. ACM,
    2008, pp. 79–88, doi:<a href="https://doi.org/10.1145/1450058.1450070">10.1145/1450058.1450070</a>.
  short: L. Doyen, T.A. Henzinger, B. Jobstmann, T. Petrov, in:, ACM, 2008, pp. 79–88.
conference:
  name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:21Z
date_published: 2008-10-01T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '01'
doi: 10.1145/1450058.1450070
extern: 1
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/interface_theories_with_component_reuse.pdf
month: '10'
page: 79 - 88
publication_status: published
publisher: ACM
publist_id: '193'
quality_controlled: 0
status: public
title: Interface theories with component reuse
type: conference
year: '2008'
...