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.
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.