Multi-core model checking for biological applications

Jaco van de Pol
Universiteit Twente

Slides from the talk [pdf]

Abstract: Multi-core model checking algorithms aim at speeding up verification tasks, by using multiple processor cores running in shared memory. Using shared memory avoids communication overhead due to message passing, but it is far from trivial to obtain ideal speedups, since the underlying graph algorithms are memory intensive and irregular.

I will present some key ideas in multi-core model checking, which have enabled us to provide scalable solutions for reachability, LTL model checking, and symbolic model checking. Key ingredients are a scalable shared hashtable, parallel random search algorithms, and an efficient work stealing scheme to implement multi-core decision diagrams.

We implemented our ideas in the LTSmin toolset, providing a high performance model checker through the PINS interface, independent of the specification language. We instantiated this for Promela, mCRL, DVE and UPPAAL timed automata. I will explain how a slight extension of PINS enables LTL model checking for timed automata.

Finally, I will introduce a biological application of model checking. We study networks of signaling pathways, crucial for the correct functioning of living cells. Signaling pathways can be drawn in an existing framework, Cytoscape. Our plugin ANIMO allows interactive modeling and simulation, based on a translation to UPPAAL timed automata. We are currently investigating the signaling network in human chondrocytes, using model checking to study the transition between cartilage and bone formation. The ultimate goal is to find a cure that prevents the devastating damage of osteo-arthritis.

Last changed December 7, 2013 18:09 EET by local organizers, nwpt13 (at) ioc.ee