We introduce a formalism to represent and analyze protein-protein and protein-DNA interaction networks. We illustrate the expressivity of this language, by proposing a formal counterpart of Kohn's compilation on the mammalian cell cycle control. This e#ectively turns an otherwise static knowledge into a discrete transition system incorporating a qualitative description of the dynamics. We then propose to use the Computation Tree Logic CTL as a query language for querying the possible...