> Besides important theoretical applications in studying properties of trap spaces, the connection enables us to propose an alternative approach to compute minimal trap spaces, and hence complex attractors, of a general Boolean network. It replaces the need for prime implicants by a completely different technique, namely the enumeration of maximal siphons in the Petri net encoding of the original model. We then demonstrate its efficiency and compare it to the state-of-the-art methods on a large collection of real-world and randomly generated models.
The most common use of Boolean models is simulating biological systems, i.e. genes and proteins interacting with each other. Trap spaces are the steady states of the model. So, if you start the model in a random state then you're guaranteed to see the model in one of the trap space states after a long enough amount of simulation time. That's interesting because it tells us the most likely behavior of the biological system. Suppose we're modeling cancer cells. They have a trap space that corresponds to activation of lots of genes that cause hyperactive growth. We'd like to know how to disrupt that system so that the trap space with hyperactive growth genes goes away, causing the cancer to stop growing.
Yep, they’re just next state equations with boolean states. It is indeed very general. The interesting bit is that they typically have lots of feedback loops, which leads to behavior that’s really difficult to predict.
Fascinating, then were model checkers successful at all for finding interesting properties and behaviors?
IIRC Petri Nets are strictly more powerful than register-transfer/Boolean state machines, intuitive reason being the Petri net tokens are a dynamic set of unbounded, concurrent counters (whereas a state machine has a fixed set of state variables equivalent to a single counter). I wonder if this paper explains this distinction as it argues one reduces to the other.