Professor, Department of Computer Science, Stanford University
The Pathalyzer: a Tool for Analysis of Signal Transduction Pathways
This is an unusual application of model checking to biological applications. Signal transduction pathways in cells are chains of chemical reactions that convey information from the outside world to the nucleus of the cell, to affect gene expression. There are many pathways, which overlap and interact, much like asynchronous digital logic. Petri Nets seem to be an appropriate qualitative model for signal transduction pathways, but building a useful tool requires rapid exploration of state spaces -- which is achieved in this case using partial order reduction.