Published in Volume XXI, Issue 1, 2011, pages 39-72

Authors: P. Drabik, A. Maggiolo-Schettini, P. Milazzo


We propose sync-programs, an automata-based formalism for the description of biological systems, and a modular verification technique for such a formalism that allows properties expressed in the universal fragment of CTL to be verified on suitably chosen fragments of models, rather than on whole models. As an application we show the modelling of the lac operon regulation process and the modular verification of some properties. Verification of properties is performed by using the NuSMV model checker and we show that by applying our modular verification technique we can verify properties in shorter times than those necessary to verify the same properties in the whole model.

Full Text (PDF)


[1] Andre Arnold. The AltaRica formalism for describing concurrent systems. Fundamenta Informaticae, 1999.

[2] Paul C. Attie. Synthesis of large dynamic concurrent programs from dynamic specifications. CoRR, abs/0801.1687, 2008.

[3] Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, and Gigliola Vaglini. LORETO: A tool for reducing state explosion in verification of LOTOS programs. Softw., Pract. Exper., 29(12):1123-1147, 1999.

[4] Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, and Angelo Troina. A calculus of looping sequences for modelling microbiological systems. Fundam. Inf., 72(1-3):21-35, 2006.

[5] Glenn Bruns. A practical technique for process abstraction. In Proceedings of the 4th International Conference on Concurrency Theory, CONCUR ’93, pages 37-49, London, UK, 1993. Springer-Verlag.

[6] Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Inf. Comput., 98(2):142-170, 1992.

[7] Laurence Calzone, Nathalie Chabrier-Rivier, Fran¸cois Fages, and Sylvain Soliman. Machine learning biochemical networks from temporal logic properties. Transactions on Computational Systems Biology VI, pages 68-94, 2006.

[8] Luca Cardelli. Brane calculi. Computational Methods in Systems Biology, pages 257-278, 2005.

[9] Luca Cardelli. Artificial biochemistry. Algorithmic Bioprocesses, pages 429-462, 2009.

[10] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS, Copenhagen, Denmark, July 2002. Springer.

[11] Federica Ciocchetta, Maria Luisa Guerriero, and Jane Hillston. Investigating modularity in the analysis of process algebra models of biochemical systems. CoRR, abs/1002.4063, 2010.

[12] Federica Ciocchetta and Jane Hillston. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theor. Comput. Sci., 410(33-34):3065-3084, 2009.

[13] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, pages 52-71, London, UK, 1982. Springer-Verlag.

[14] Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512- 1542, 1994.

[15] Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253-291, 1997.

[16] Vincent Danos and Cosimo Laneve. Formal molecular biology. Theor. Comput. Sci., 325(1):69-110, 2004.


[18] Glycolytic pathway and lac operon of e. coli. CSML Model database.

[19] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. Dynamic sync-programs for modular verification of biological systems. In 2nd Int. Workshop on Non-Classical Models of Automata and applications (NCMA’10), Jena, Germany, 2010.

[20] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. Modular verification of interactive systems with an application to biology. Electronic Notes in Theoretical Computer Science, 268:61-75, 12 2010.

[21] Peter Drabik and Guido Scatena. An application of model checking to epidemiology (extended abstract). In 1st Int. Workshop on Applications of Membrane computing, Concurrency and Agent-based modelling in POPulation biology (AMCA-POP 2010), Jena, Germany, 2010.

[22] Francois Fages, Sylvain Soliman, and Nathalie Chabrier-Rivier. Modelling and querying interaction networks in the biochemical abstract machine biocham. Journal of Biological Physics and Chemistry, 4:64- 73, 2004.

[23] Orna Grumberg and David E. Long. Model checking and modular verification. ACM Trans. Program. Lang. Syst., 16(3):843-871, 1994.

[24] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker, and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. Theor. Comput. Sci., 391(3):239-257, 2008.

[25] F Jacob and J Monod. Genetic regulatory mechanisms in the synthesis of proteins. J Mol Biol, 3:318-356, 06 1961.

[26] Jetty Kleijn. Team Automata for CSCW-A Survey-. Petri Net Technology for Communication-Based Systems, pages 295-320, 2003.

[27] I.A. Lomazova. Communities of interacting automata for modelling distributed systems with dynamic structure. Fundamenta Informaticae, 60(1-4):225-236, 2004.

[28] Nancy Lynch. Input/output automata: Basic, timed, hybrid, probabilistic, dynamic,… In Roberto Amadio and Denis Lugiez, editors, CONCUR 2003 – Concurrency Theory, volume 2761 of Lecture Notes in Computer Science, pages 191-192. Springer Berlin / Heidelberg, 2003.

[29] Pedro T. Monteiro, Delphine Ropers, Radu Mateescu, Ana T. Freitas, and Hidde de Jong. Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics, 24(16):i227- 233, 8 2008.

[30] Michael Pedersen. Compositional definitions of minimal flows in Petri nets. In Computational Methods in Systems Biology, pages 288-307. Springer, 2008.

[31] Marcelo Cezar Pinto, Luciana Foss, Jos´e Carlos Merino Mombach, and Leila Ribeiro. Modelling, property verification and behavioural equivalence of lactose operon regulation. Computers in Biology and Medicine, 37(2):134-148, 2007.

[32] Corrado Priami, Aviv Regev, Ehud Shapiro, and William Silverman. Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Inf. Process. Lett., 80(1):25- 31, 2001.

[33] Aviv Regev, Ekaterina M. Panina, William Silverman, Luca Cardelli, and Ehud Shapiro. Bioambients: an abstraction for biological compartments. Theor. Comput. Sci., 325(1):141-167, September 2004.

[34] B. Zimmerov´a. Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction. PhD thesis, Masaryk University, Brno, Czech Republic, 2008.


  title={Modular Verification of Interactive Systems with an Application to Biology},
  author={P. Drabik and A. Maggiolo-Schettini and P. Milazzo},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}