Academic Journals Database
Disseminating quality controlled scientific knowledge

Modular Verification of Qualitative Pathway Models with Fairness

ADD TO MY LIST
 
Author(s): P. Drabik | A. Maggiolo-Schettini | P. Milazzo | G. Pardini

Journal: Scientific Annals of Computer Science
ISSN 1843-8121

Volume: 23;
Issue: 1;
Start page: 75;
Date: 2013;
VIEW PDF   PDF DOWNLOAD PDF   Download PDF Original page

Keywords: Systems biology | cellular pathways | model checking | modular verification | model reduction | abstraction

ABSTRACT
Modular verification is a technique used to face the state explosion problem often encountered in the verification of properties of complex systems such as concurrent interactive systems. The modular approach is based on the observation that properties of interest often concern a rather small portion of the system. As a consequence, reduced models can be constructed which approximate the overall system behaviour thus allowing more efficient verification. Biochemical pathways can be seen as complex concurrent interactive systems. Consequently, verification of their properties is often computationally very expensive and could take advantage of the modular approach. In this paper we develop a modular verification framework for biochemical pathways. We view biochemical pathways as concurrent systems of reactions competing for molecular resources. A modular verification technique could be based on reduced models containing only reactions involving molecular resources of interest. For a proper description of the system behaviour we argue that it is essential to consider a suitable notion of fairness, which is a well-established notion in concurrency theory but novel in the field of pathway modelling. The fairness notion we consider forbids starvation of reactions, namely it ensures that a reaction that is enabled infinitely often cannot always occur to the detriment of another infinitely often enabled reaction causing the latter to never occur. We prove the correctness of the approach and demonstrate it on the model of the EGF receptor-induced MAP kinase cascade by Schoeberl et al.

Tango Jona
Tangokurs Rapperswil-Jona

    
RPA Switzerland

RPA Switzerland

Robotic process automation