Model-Checking Signal Transduction Networks through Decreasing Reachability Sets

We consider model checking of Qualitative Networks, a popular formalism for modeling signal transduction networks. One of the unique features of qualitative networks, due to them lacking initial states, is that of “reducing reachability sets”. Simply put, a state that is not visited after i steps will not be visited after i′ steps for every i′ > i. We use this feature to create a compact representation of all the paths of a qualitative network of a certain structure. Combining this compact path representation with LTL model checking leads to significant acceleration in performance. In particular, for a recent model of Leukemia, our approach works at least 10 times faster than the standard approach and up to 80 times faster in some cases. Our approach enhances the iterative working process used by biologists, enabling fast turn-around of executable biological models

Details

TypeTechReport
NumberMSR-TR-2013-30
> Publications > Model-Checking Signal Transduction Networks through Decreasing Reachability Sets