Dynamic Sync-program for Modular Verification of Biological Systems
Peter Drábik, Andrea Maggiolo–Schettini, Paolo Milazzo · Non-Classical Models for Automata and Applications · 2010
We propose dynamic sync-programs, a bio-inspired automata-based formalism for the description and the modular verification of properties of biological systems. The formalism allows entities to be created dynamically, in particular by other already running entities, as it often happens in biological systems. Moreover, multiple copies of the same entities can be present at the same time in a system. Modular verification allows properties expressed as DACTL formulae (dynamic version of the universal fragment of CTL) to be verified on a portion of the model, rather than on the whole model. We show, as an example, the application of our approach to a biological case study, namely the EGF signalling pathway.