An Integrated Approach to P Systems Formal Verification

  • Marian Gheorghe
  • Florentin Ipate
  • Raluca Lefticaru
  • Ciprian Dragomir
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6501)


This paper presents a method to formally verify P system specifications by first identifying invariants and then checking them, using the NuSMV model checker, against a Kripke structure representation. The method is applied to a basic class of P systems with transformation and communication rules using either maximal parallelism or asynchronous rewriting strategy and for a special variant of P systems with electrical charges, but without active membranes.


Linear Temporal Logic Atomic Proposition Kripke Structure Computation Tree Logic Linear Temporal Logic Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andrei, O., Ciobanu, G., Lucanu, D.: A rewriting logic framework for operational semantics of membrane systems. Theor. Comput. Sci. 373(3), 163–181 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bernardini, F., Gheorghe, M., Romero-Campero, F.J., Walkinshaw, N.: A hybrid approach to modeling biological systems. In: Eleftherakis, G., Kefalas, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2007. LNCS, vol. 4860, pp. 138–159. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Ciobanu, G.: Semantics of P systems. In: Păun, G., Rozenberg, G., Salomaa, A. (eds.) Handbook of Membrane Computing, ch. 16, pp. 413–436. Oxford University Press, Oxford (2010)Google Scholar
  4. 4.
    Ciobanu, G., Pérez-Jiménez, M.J., Păun, G. (eds.): Applications of Membrane Computing. Natural Computing Series. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  5. 5.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  6. 6.
    Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  7. 7.
    Dang, Z., Ibarra, O.H., Li, C., Xie, G.: On the decidability of model-checking for P systems. Journal of Automata, Languages and Combinatorics 11(3), 279–298 (2006)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Díaz-Pernil, D., Graciani, C., Gutiérrez-Naranjo, M.A., Pérez-Hurtado, I., Pérez-Jiménez, M.J.: Software for P systems. In: Păun, G., Rozenberg, G., Salomaa, A. (eds.) Handbook of membrane computing, ch. 17, pp. 437–454. Oxford University Press, Oxford (2010)Google Scholar
  9. 9.
    Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC 1982, pp. 169–180. ACM Press, New York (1982)CrossRefGoogle Scholar
  10. 10.
    Fontana, F., Manca, V.: Predator-prey dynamics in P systems ruled by metabolic algorithm. Biosystems 91, 545–557 (2008)CrossRefGoogle Scholar
  11. 11.
    Gheorghe, M., Ipate, F.: On testing P systems. In: Corne, D.W., Frisco, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 204–216. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Ipate, F., Gheorghe, M.: Testing non-deterministic stream X-machine models and P systems. Electronic Notes in Theoretical Computer Science 227, 113–126 (2009)CrossRefzbMATHGoogle Scholar
  14. 14.
    Ipate, F., Gheorghe, M., Lefticaru, R.: Test generation from P systems using model checking. Journal of Logic and Algebraic Programming 79(6), 350–362 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Kleijn, J., Koutny, M.: Petri nets and membrane computing. In: Păun, G., Rozenberg, G., Salomaa, A. (eds.) Handbook of membrane computing, ch. 15, pp. 389–412. Oxford University Press, Oxford (2010)Google Scholar
  16. 16.
    Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics 24(16), 227–233 (2008)CrossRefGoogle Scholar
  17. 17.
    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, FOCS 1977, pp. 46–57. IEEE, Los Alamitos (1977)Google Scholar
  18. 18.
    Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Păun, G.: Computing with membranes. Journal of Computer and System Sciences 61(1), 108–143 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Păun, G.: Membrane Computing: An Introduction. Springer, Heidelberg (2002)CrossRefzbMATHGoogle Scholar
  21. 21.
    Păun, G., Rozenberg, G., Salomaa, A. (eds.): The Oxford Handbook of Membrane Computing. Oxford University Press, Oxford (2010)zbMATHGoogle Scholar
  22. 22.
    Şerbănuţă, T., Ştefănescu, G., Roşu, G.: Defining and executing P systems with structured data in K. In: Corne, D.W., Frisco, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 374–393. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Marian Gheorghe
    • 1
    • 2
  • Florentin Ipate
    • 2
  • Raluca Lefticaru
    • 2
  • Ciprian Dragomir
    • 1
  1. 1.Department of Computer ScienceUniversity of SheffieldSheffieldUK
  2. 2.Department of Computer ScienceUniversity of PitestiPitestiRomania

Personalised recommendations