Nothing Special   »   [go: up one dir, main page]

Skip to main content

Signaling P Systems and Verification Problems

  • Conference paper
Automata, Languages and Programming (ICALP 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3580))

Included in the following conference series:

Abstract

We introduce a new model of membrane computing system (or P system), called signaling P system. It turns out that signaling systems are a form of P systems with promoters that have been studied earlier in the literature. However, unlike non-cooperative P systems with promoters, which are known to be universal, non-cooperative signaling systems have decidable reachability properties. Our focus in this paper is on verification problems of signaling systems; i.e., algorithmic solutions to a verification query on whether a given signaling system satisfies some desired behavioral property. Such solutions not only help us understand the power of “maximal parallelism” in P systems but also would provide a way to validate a (signaling) P system in vitro through digital computers when the P system is intended to simulate living cells. We present decidable and undecidable properties of the model of non-cooperative signaling systems using proof techniques that we believe are new in the P system area. For the positive results, we use a form of “upper-closed sets” to serve as a symbolic representation for configuration sets of the system, and prove decidable symbolic model-checking properties about them using backward reachability analysis. For the negative results, we use a reduction via the undecidability of Hilbert’s Tenth Problem. This is in contrast to previous proofs of universality in P systems where almost always the reduction is via matrix grammar with appearance checking or through Minsky’s two-counter machines. Here, we employ a new tool using Diophantine equations, which facilitates elegant proofs of the undecidable results. With multiplication being easily implemented under maximal parallelism, we feel that our new technique is of interest in its own right and might find additional applications in P systems.

The work by Cheng Li and Zhe Dang was supported in part by NSF Grant CCF-0430531. The work by Oscar H. Ibarra was supported in part by NSF Grants CCR-0208595 and CCF-0430945.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. Ardelean, I.I., Cavaliere, M., Sburlan, D.: Computing using signals: From cells to P Systems. In: Second Brainstorming Week on Membrane Computing, Sevilla, Spain, February 2-7, pp. 60–73 (2004)

    Google Scholar 

  3. Becker, W.M., Kleinsmith, L.J., Hardin, J.: The World of the Cell, 5th edn. Benjamin Cummings, San Francisco (2003)

    Google Scholar 

  4. Bottoni, P., Martin-Vide, C., Paun, G., Rozenberg, G.: Membrane systems with promoters/inhibitors. Acta Informatica 38(10), 695–720 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. TOPLAS 21(4), 747–789 (1999)

    Article  Google Scholar 

  6. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  7. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  8. Dang, Z., Ibarra, O.H., Li, C., Xie, G.: On model-checking of P systems (2005) (submitted)

    Google Scholar 

  9. Esparza, J.: Decidability and complexity of Petri net problems - an introduction. In: Petri Nets, pp. 374–428 (1996)

    Google Scholar 

  10. Freund, R., Kari, L., Oswald, M., Sosik, P.: Computationally universal P systems without priorities: two catalysts are sufficient (2003), Available at http://psystems.disco.unimib.it

  11. Freund, R., Paun, G.: On deterministic P systems (2003), Available at http://psystems.disco.unimib.it

  12. Ibarra, O.H.: The number of membranes matters. In: Martín-Vide, C., Mauri, G., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2003. LNCS, vol. 2933, pp. 218–231. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Ibarra, O.H., Dang, Z., Egecioglu, O.: Catalytic P systems, semilinear sets, and vector addition systems. Theoretical Computer Science 312(2-3), 379–399 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  14. Ibarra, O.H., Yen, H., Dang, Z.: The power of maximal parallelism in P systems. In: Calude, C.S., Calude, E., Dinneen, M.J. (eds.) DLT 2004. LNCS, vol. 3340, pp. 212–224. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Ito, M., Martin-Vide, C., Paun, G.: A characterization of Parikh sets of ET0L languages in terms of P systems. In: Words, Semigroups, and Transducers, pp. 239–254. World Scientific, Singapore

    Google Scholar 

  16. Martin-Vide, C., Paun, G.: Computing with membranes (P systems): universality results. In: Margenstern, M., Rogozhin, Y. (eds.) MCU 2001. LNCS, vol. 2055, pp. 82–101. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Matiyasevich, Y.V.: Hilbert’s Tenth Problem. MIT Press, Cambridge (1993)

    Google Scholar 

  18. Paun, G.: Computing with membranes. JCSS 61(1), 108–143 (2000)

    MATH  MathSciNet  Google Scholar 

  19. Paun, G.: Membrane Computing: An Introduction. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  20. Paun, G., Rozenberg, G.: A guide to membrane computing. TCS 287(1), 73–100 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  21. Sosik, P.: P systems versus register machines: two universality proofs. In: Păun, G., Rozenberg, G., Salomaa, A., Zandron, C. (eds.) WMC 2002. LNCS, vol. 2597, pp. 371–382. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  22. Sosik, P., Freund, R.: P systems without priorities are computationally universal. In: Păun, G., Rozenberg, G., Salomaa, A., Zandron, C. (eds.) WMC 2002. LNCS, vol. 2597, pp. 400–409. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Li, C., Dang, Z., Ibarra, O.H., Yen, HC. (2005). Signaling P Systems and Verification Problems. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds) Automata, Languages and Programming. ICALP 2005. Lecture Notes in Computer Science, vol 3580. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11523468_118

Download citation

  • DOI: https://doi.org/10.1007/11523468_118

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27580-0

  • Online ISBN: 978-3-540-31691-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics