---
_id: '719'
abstract:
- lang: eng
  text: 'The ubiquity of computation in modern machines and devices imposes a need
    to assert the correctness of their behavior. Especially in the case of safety-critical
    systems, their designers need to take measures that enforce their safe operation.
    Formal methods has emerged as a research field that addresses this challenge:
    by rigorously proving that all system executions adhere to their specifications,
    the correctness of an implementation under concern can be assured. To achieve
    this goal, a plethora of techniques are nowadays available, all of which are optimized
    for different system types and application domains.'
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Rüdiger
  full_name: Ehlers, Rüdiger
  last_name: Ehlers
citation:
  ama: 'Chatterjee K, Ehlers R. Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>.
    2017;54(6):543-544. doi:<a href="https://doi.org/10.1007/s00236-017-0299-0">10.1007/s00236-017-0299-0</a>'
  apa: 'Chatterjee, K., &#38; Ehlers, R. (2017). Special issue: Synthesis and SYNT
    2014. <i>Acta Informatica</i>. Springer. <a href="https://doi.org/10.1007/s00236-017-0299-0">https://doi.org/10.1007/s00236-017-0299-0</a>'
  chicago: 'Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis
    and SYNT 2014.” <i>Acta Informatica</i>. Springer, 2017. <a href="https://doi.org/10.1007/s00236-017-0299-0">https://doi.org/10.1007/s00236-017-0299-0</a>.'
  ieee: 'K. Chatterjee and R. Ehlers, “Special issue: Synthesis and SYNT 2014,” <i>Acta
    Informatica</i>, vol. 54, no. 6. Springer, pp. 543–544, 2017.'
  ista: 'Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta
    Informatica. 54(6), 543–544.'
  mla: 'Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and
    SYNT 2014.” <i>Acta Informatica</i>, vol. 54, no. 6, Springer, 2017, pp. 543–44,
    doi:<a href="https://doi.org/10.1007/s00236-017-0299-0">10.1007/s00236-017-0299-0</a>.'
  short: K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.
date_created: 2018-12-11T11:48:07Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2021-01-12T08:12:18Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s00236-017-0299-0
intvolume: '        54'
issue: '6'
language:
- iso: eng
month: '09'
oa_version: None
page: 543 - 544
publication: Acta Informatica
publication_identifier:
  issn:
  - '00015903'
publication_status: published
publisher: Springer
publist_id: '6961'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Special issue: Synthesis and SYNT 2014'
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 54
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
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'
...