TY - GEN
T1 - Abstract Interpretation of Cellular Signalling Networks
AU - Danos, Vincent
AU - Feret, Jérôme
AU - Fontana, Walter
AU - Krivine, Jean
PY - 2008
Y1 - 2008
N2 - Cellular signalling pathways, where proteins can form complexes and undergo a large array of post translational modifications are highly combinatorial systems sending and receiving extra-cellular signals and triggering appropriate responses. Process-centric languages seem apt to their representation and simulation [1,2,3]. Rule-centric languages such as κ [4,5,6,7,8] and BNG [9,10] bring in additional ease of expression. We propose in this paper a method to enumerate a superset of the reachable complexes that a κ rule set can generate. This is done via the construction of a finite abstract interpretation. We find a simple criterion for this superset to be the exact set of reachable complexes, namely that the superset is closed under swap, an operation whereby pairs of edges of the same type can permute their ends. We also show that a simple syntactic restriction on rules is sufficient to ensure the generation of a swap-closed set of complexes. We conclude by showing that a substantial rule set (presented in Ref. [4]) modelling the EGF receptor pathway verifies that syntactic condition (up to suitable transformations), and therefore despite its apparent complexity has a rather simple set of reachables.
AB - Cellular signalling pathways, where proteins can form complexes and undergo a large array of post translational modifications are highly combinatorial systems sending and receiving extra-cellular signals and triggering appropriate responses. Process-centric languages seem apt to their representation and simulation [1,2,3]. Rule-centric languages such as κ [4,5,6,7,8] and BNG [9,10] bring in additional ease of expression. We propose in this paper a method to enumerate a superset of the reachable complexes that a κ rule set can generate. This is done via the construction of a finite abstract interpretation. We find a simple criterion for this superset to be the exact set of reachable complexes, namely that the superset is closed under swap, an operation whereby pairs of edges of the same type can permute their ends. We also show that a simple syntactic restriction on rules is sufficient to ensure the generation of a swap-closed set of complexes. We conclude by showing that a substantial rule set (presented in Ref. [4]) modelling the EGF receptor pathway verifies that syntactic condition (up to suitable transformations), and therefore despite its apparent complexity has a rather simple set of reachables.
UR - https://www.scopus.com/pages/publications/40549119812
U2 - 10.1007/978-3-540-78163-9_11
DO - 10.1007/978-3-540-78163-9_11
M3 - Conference contribution
SN - 978-3-540-78162-2
T3 - Lecture Notes in Computer Science
SP - 83
EP - 97
BT - Verification, Model Checking, and Abstract Interpretation
A2 - Logozzo, Francesco
A2 - Peled, Doron
A2 - Zuck, Lenore
PB - Springer
ER -