Modeling and verifying WNT signaling pathway

WNT signaling pathway is an important pathway in the development and disease forming of a variety of animals, concerning such processes as hematopoiesis and oncogenesis. In this paper we use quantitative approach to study the canonical pathway of WNT signaling. We first present the basic knowledge of the WNT signaling pathway, including the necessary elements on the pathway, then introduce the modeling method, the tissue P system, which is a computational device inspired from the behavior of living cells. After that we construct the model of the WNT signaling pathway using the tissue P system. Moreover, we implement the model using Maude, a rewriting logic based interpreter software. Provided with the model implementation, we model check some critical properties on several nodes of the WNT signaling pathway, to show the effect of the modeling and implementation. We draw the conclusion in the end.