Model checking of apoptosis signaling pathways in lung cancers

Abstract

Model denetleme farklı alanlarda otomatik geçerleme ve analiz yapmak için yaygınolarak kullanılan bir formel geçerleme tekniğidir. Bu çalışmada bir model denetlemeyöntemini biyolojik bir sisteme uyguladık. Öncelikle akciğer kanseri vakalarındaapoptoz yani programlanmış hücre ölümü sinyal yollarını, boole değerler alabilen birağa dönüştürdükten sonra NuSMV modeline çevirdik. Bu ağı içsel ve dışsal apoptozyolları ile p53 sinyal yolunu ve akciğer kanserlerinde gözlenen p53 - DAP Kinazyolunu birleştirerek oluşturduk. Sonrasında oluşturduğumuz bu modeli, deneyselsonuçlara uygunluk açısından kontrol ettik ve akciğer kanserlerinde apoptozdinamiklerini sembolik model denetleyici NuSMV kullanarak sorguladık ve apoptozile akciğer kanseri arasındaki ilişkiyi belirledik. Son olarak bütün süreci, çevrimkuralları ve biyolojik sorgular için zamansal özellik paternleri sunarak genelledik.Böylece herhangi bir sinyal yolunun model denetleme sürecinin otomatizeedilebilmesine zemin hazırladık.

Model checking is a formal verification technique which is widely used in differentareas for automated verification and analysis. In this study, we applied a ModelChecking method to a biological system. Firstly we constructed a single-cell,Boolean network model for the signaling pathways of apoptosis (programmed celldeath) in lung cancers by combining the intrinsic and extrinsic Apoptosis pathways,p53 signaling pathway and p53 - DAP Kinase pathway in Lung cancers. Wetranslated this model to the NuSMV input language. Then we converted knownexperimental results to CTL properties and checked the conformance of our modelwith respect to biological experimental results. We examined the dynamics of theapoptosis in lung cancer using NuSMV symbolic model checker and identified therelationship between apoptosis and lung cancer. Finally we generalized the wholeprocess by introducing translation rules and CTL property patterns for biologicalqueries so that model checking any signaling pathway can be automated .