[bglazer]

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.

[calf]

Wait so these Boolean models are just Boolean next-state functions of finite state machines? That seems very general then.

[bglazer]

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.

[calf]

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.

[bglazer]

Yep, model checkers are one of the more powerful tools for working with Boolean models. You might find some of the work from Jasmine Fisher's lab interesting, especially when she was at Microsoft Research.

My take on model checking for Boolean networks is that they're too rigid and too difficult to program to answer the really interesting biological questions. My understanding is that they're great for exactly proving exact correctness, but can't tell you if your model is close but not exactly correct. Given the limits of biological data, the close but not perfect models are sometimes the best. Also, you really want to be able to ask weird questions sometimes. Like, how does this model behave if we apply a perturbation, or series of perturbations to it? What if we simulate the model in some weird, non-conventional way? Then configuring the model checker to give you information about that situation can be really difficult. Like PhD thesis level difficult.

That's why I have always just relied on brute-force simulations. Compute is cheap, my time is not (even as a grad student). Much easier to just submit a job to the cluster and wait a day then try to figure out how to get Z3 to do what I want.

Others will probably disagree.

Unfortunately, I'm not really familiar enough with Petri nets to comment on the relationship to boolean models.