# Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks

arXiv: https://arxiv.org/abs/2305.02442 · HTML: https://mlsanity.com/paper/2305.02442/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 40 references that are in the map.
- First posted on arXiv 3 May 2023.

## Builds on (most cited first, 4 of 4)

- [Multi-shot ASP solving with clingo](https://mlsanity.com/paper/1705.09811/) (2017)
- [DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL](https://mlsanity.com/paper/1702.08256/) (2017)
- [Synthesis of Boolean Networks from Biological Dynamical Constraints using Answer-Set Programming](https://mlsanity.com/paper/1909.04309/) (2019)
- [Marker and source-marker reprogramming of Most Permissive Boolean networks and ensembles with BoNesis](https://mlsanity.com/paper/2207.13307/) (2022)

## Abstract (arXiv)

Minimal trap spaces (MTSs) capture subspaces in which the Boolean dynamics is trapped, whatever the update mode. They correspond to the attractors of the most permissive mode. Due to their versatility, the computation of MTSs has recently gained traction, essentially by focusing on their enumeration. In this paper, we address the logical reasoning on universal properties of MTSs in the scope of two problems: the reprogramming of Boolean networks for identifying the permanent freeze of Boolean variables that enforce a given property on all the MTSs, and the synthesis of Boolean networks from universal properties on their MTSs. Both problems reduce to solving the satisfiability of quantified propositional logic formula with 3 levels of quantifiers (existsforallexists). In this paper, we introduce a Counter-Example Guided Refinement Abstraction (CEGAR) to efficiently solve these problems by coupling the resolution of two simpler formulas. We provide a prototype relying on Answer-Set Programming for each formula and show its tractability on a wide range of Boolean models of biological networks.