| Popis: |
The attractors of Boolean networks and their basins have been shown to be highly relevant for model validation and predictive modelling, e.g., in systems biology. Yet there are currently very few tools available that are able to compute and visualise not only attractors but also their basins. In the realm of asynchronous, non-deterministic modeling not only is the repertoire of software even more limited, but also the formal notions for basins of attraction are often lacking. In this setting, the difficulty both for theory and computation arises from the fact that states may be ele- ments of several distinct basins. In this paper we address this topic by partitioning the state space into sets that are committed to the same attractors. These commitment sets can easily be generalised to sets that are equivalent w.r.t. the long-term behaviours of pre-selected nodes which leads us to the notions of markers and phenotypes which we illustrate in a case study on bladder tumorigenesis. For every concept we propose equivalent CTL model checking queries and an extension of the state of the art model checking software NuSMV is made available that is capa- ble of computing the respective sets. All notions are fully integrated as three new modules in our Python package PyBoolNet, including functions for visualising the basins, commitment sets and phenotypes as quotient graphs and pie charts. |
