Approximating attractors of Boolean networks by iterative CTL model checking
This paper introduces the notion of approximating asynchronous attractors of Boolean networks by minimal trap spaces. We define three criteria for determining the quality of an approximation: faithfulness which requires that the oscillating variables of all attractors in a trapspace correspond to th...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Frontiers Media S.A.
2015-09-01
|
Series: | Frontiers in Bioengineering and Biotechnology |
Subjects: | |
Online Access: | http://journal.frontiersin.org/Journal/10.3389/fbioe.2015.00130/full |
id |
doaj-832e0c542337478689c9d33b6bd741d3 |
---|---|
record_format |
Article |
spelling |
doaj-832e0c542337478689c9d33b6bd741d32020-11-25T01:15:34ZengFrontiers Media S.A.Frontiers in Bioengineering and Biotechnology2296-41852015-09-01310.3389/fbioe.2015.00130142935Approximating attractors of Boolean networks by iterative CTL model checkingHannes eKlarner0Heike eSiebert1Freie Universität BerlinFreie Universität BerlinThis paper introduces the notion of approximating asynchronous attractors of Boolean networks by minimal trap spaces. We define three criteria for determining the quality of an approximation: faithfulness which requires that the oscillating variables of all attractors in a trapspace correspond to their dimensions, univocality which requires that there is a unique attractor in each trap space and completeness which requires that there are no attractors outside of a given set of trap spaces. Each is a reachability property for which we give equivalent model checking queries. Whereas faithfulness and univocality can be decided by model checking the corresponding subnetworks, the naive query for completeness must be evaluated on the full state space. Our main result is an alternative approach which is based on the iterative refinement of an initially poor approximation. The algorithm detects so-called autonomous sets in the interaction graph, variables that contain all their regulators, and considers their intersection and extension in order to perform model checking on the smallest possible state spaces. A benchmark, in which we apply the algorithm to 18 published Boolean networks, is given. In each case, the minimal trap spaces are faithful, univocal and complete which suggests that they are in general good approximations for the asymptotics of Boolean networks.http://journal.frontiersin.org/Journal/10.3389/fbioe.2015.00130/fullattractorsgene regulationBoolean networksAsynchronous dynamicsCTL model checkingsignal transudction |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Hannes eKlarner Heike eSiebert |
spellingShingle |
Hannes eKlarner Heike eSiebert Approximating attractors of Boolean networks by iterative CTL model checking Frontiers in Bioengineering and Biotechnology attractors gene regulation Boolean networks Asynchronous dynamics CTL model checking signal transudction |
author_facet |
Hannes eKlarner Heike eSiebert |
author_sort |
Hannes eKlarner |
title |
Approximating attractors of Boolean networks by iterative CTL model checking |
title_short |
Approximating attractors of Boolean networks by iterative CTL model checking |
title_full |
Approximating attractors of Boolean networks by iterative CTL model checking |
title_fullStr |
Approximating attractors of Boolean networks by iterative CTL model checking |
title_full_unstemmed |
Approximating attractors of Boolean networks by iterative CTL model checking |
title_sort |
approximating attractors of boolean networks by iterative ctl model checking |
publisher |
Frontiers Media S.A. |
series |
Frontiers in Bioengineering and Biotechnology |
issn |
2296-4185 |
publishDate |
2015-09-01 |
description |
This paper introduces the notion of approximating asynchronous attractors of Boolean networks by minimal trap spaces. We define three criteria for determining the quality of an approximation: faithfulness which requires that the oscillating variables of all attractors in a trapspace correspond to their dimensions, univocality which requires that there is a unique attractor in each trap space and completeness which requires that there are no attractors outside of a given set of trap spaces. Each is a reachability property for which we give equivalent model checking queries. Whereas faithfulness and univocality can be decided by model checking the corresponding subnetworks, the naive query for completeness must be evaluated on the full state space. Our main result is an alternative approach which is based on the iterative refinement of an initially poor approximation. The algorithm detects so-called autonomous sets in the interaction graph, variables that contain all their regulators, and considers their intersection and extension in order to perform model checking on the smallest possible state spaces. A benchmark, in which we apply the algorithm to 18 published Boolean networks, is given. In each case, the minimal trap spaces are faithful, univocal and complete which suggests that they are in general good approximations for the asymptotics of Boolean networks. |
topic |
attractors gene regulation Boolean networks Asynchronous dynamics CTL model checking signal transudction |
url |
http://journal.frontiersin.org/Journal/10.3389/fbioe.2015.00130/full |
work_keys_str_mv |
AT hanneseklarner approximatingattractorsofbooleannetworksbyiterativectlmodelchecking AT heikeesiebert approximatingattractorsofbooleannetworksbyiterativectlmodelchecking |
_version_ |
1725152452160782336 |