Authors: Bhattacharya Arnab, Kuppusamy Lakshmanan, Shukla Ankit, Srivas Mandayam, Thattai Mukund
The inside of a living cell is split into several distinct locations called
organelles. Small transporters called vesicles move cargo between these
organelles, just as trucks move cargo between warehouses in a logistics
network. We are interested in the global mathematical features of the resulting
network, where each organelle is considered as a node, and each vesicle
transport route is considered as a directed edge. The whole structure can be
represented as graph. We have shown that the connectedness of a vesicle graph
is an informative feature. Two - connectedness is necessary and sufficient for
mass balance. Three - connectedness is sufficient (but not necessary) for a
system driven by molecular recognition. Four - connectedness is necessary and
sufficient for the famous Rothman-Schekman-Sudhof model of vesicle traffic. We
have used boolean satisfiability, SAT as a framework via a model-checking tool
(CBMC) to verify these properties and shown further connections between
molecular rules and graph-theoretic properties. Scalability of SAT solvers and
model checkers that use has always been an issue, we have shown by exploiting
structure of formulas it is possible to scale the SAT model checkers to
reasonably complex biological systems. . . .