Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Interpreted Systems Semantics for Process Algebra with Identity Annotations

  • Conference paper
Logic, Language, and Computation (TbiLLC 2011)

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

Included in the following conference series:

Abstract

Process algebras have been developed as formalisms for specifying the behavioral aspects of protocols. Interpreted systems have been proposed as a semantic model for multi-agent communication. In this paper, we connect these two formalisms by defining an interpreted systems semantics for a generic process algebraic formalism. This allows us to translate and compare the vast body of knowledge and results for each of the two formalisms to the other and perform epistemic reasoning, e.g., using model-checking tools for interpreted systems, on process algebraic specifications. Based on our translation we formulate and prove some results about the interpreted systems generated by process algebraic specifications.

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

Access this chapter

Log in via an institution

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.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. Aceto, L., Birgisson, A., Ingólfsdóttir, A., Mousavi, M.: Decompositional Reasoning about the History of Parallel Processes. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 32–47. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. Bhargava, M., Palamidessi, C.: Probabilistic Anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press (2009)

    Google Scholar 

  4. van Benthem, J., Gerbrandy, J., Hoshi, T., Pacuit, E.: Merging frameworks for interaction. Journal of Philosophical Logic 38(5), 491–526 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  5. Boureanu, I., Cohen, M., Lomuscio, A.: A Compilation Method for the Verification of Temporal-Epistemic Properties of Cryptographic Protocols. Journal of Applied Non-Classical Logics 19(4), 463–487 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Chadha, R., Delaune, S., Kremer, S.: Epistemic Logic for the Applied Pi Calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 182–197. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Chatzikokolakis, K., Knight, S., Panangaden, P.: Epistemic Strategies and Games on Concurrent Processes. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 153–166. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1, 65–75 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  9. Dechesne, F., Mousavi, M.R., Orzan, S.: Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 226–241. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Dechesne, F., Mousavi, M.R., Orzan, S.: Operational and epistemic approaches to protocol analysis: bridging the gap. Technical Report CSR-07-15, Department of Computer Science, Eindhoven University of Technology (2007)

    Google Scholar 

  11. Dechesne, F., Wang, Y.: To know or not to know: epistemic approaches to security protocol verification. Synthese 177, 51–76 (2010)

    Article  MATH  Google Scholar 

  12. van Eijk, R., de Boer, F., van der Hoek, W., Meyer, J.-J.C.: Operational Semantics for Agent Communication Languages. In: Dignum, F.P.M., Greaves, M. (eds.) Issues in Agent Communication. LNCS, vol. 1916, pp. 80–95. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. van Eijk, R.M., de Boer, F.S., van der Hoek, W., Meyer, J.-J.Ch.: Process Algebra for Agent Communication: A General Semantic Approach. In: Huget, M.-P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 113–128. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  14. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press (1995)

    Google Scholar 

  15. Halpern, J.Y., Moses, Y.: Knowledge and Common Knowledge in a distributed environment. In: Proceedings of the 3rd ACM Conference on Principles of Distributed Computing, pp. 50–61. ACM (1984); Reprinted in the Journal of the Association for Computing Machinery 37(3), 549–587 (1990)

    Google Scholar 

  16. Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. Journal of Computer Security, 483–514 (2005)

    Google Scholar 

  17. Halpern, J., Vardi, M.Y.: Reasoning about knowledge and time in asynchronous systems. In: Proceedings of STOC 1988, pp. 53–65. ACM Press (1988)

    Google Scholar 

  18. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hoare, T.: Communicating Sequential Processes. Prentice-Hall (1985)

    Google Scholar 

  20. van der Hoek, W., van Hulst, M., Meyer, J.-J.Ch.: Towards an Epistemic Approach to Reasoning about Concurrent Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1992. LNCS, vol. 666, pp. 261–287. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  21. Hoshi, T.: Merging DEL and ETL. J. of Logic, Lang. and Inf. 19, 413–430 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  22. Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: A modular approach. Journal of Computer Security 12(1), 3–36 (2004)

    Google Scholar 

  23. van Hulst, M., Meyer, J.-J.Ch.: An epistemic proof system for parallel processes: extended abstract. In: Proceeding of TARK 1994, pp. 243–254. ACM Press (1994)

    Google Scholar 

  24. Katz, S., Taubenfeld, G.: What Processes Know: Definitions and Proof Methods. In: Proceedings of PODC 1986, pp. 249–262. ACM Press (1986)

    Google Scholar 

  25. Kramer, S., Palamidessi, C., Segala, R., Turrini, A., Braun, C.: A quantitative doxastic logic for probabilistic processes and applications to information-hiding. The Journal of Applied Non-Classical Logic 19(4), 489–516 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  26. Lomuscio, A., Ryan, M.: Ideal agents sharing (some!) knowledge. In: Proceedings of ECAI 1998, pp. 557–561. John Wiley and Sons (1998)

    Google Scholar 

  27. Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  28. van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proceedings of CSFW 2004, pp. 280–291. IEEE (2004)

    Google Scholar 

  29. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Book  Google Scholar 

  30. Parikh, R., Ramanujam, R.: Distributed Processes and the Logic of Knowledge. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 256–268. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  31. Park, D.M.R.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  32. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60, 17–139 (2004)

    Article  MathSciNet  Google Scholar 

  33. Raimondi, F., Lomuscio, A.: A tool for specification and verification of epistemic properties in interpreted systems. Electronic Notes in Theoretical Computer Science 85(4) (2004)

    Google Scholar 

  34. Richards, S., Sadrzadeh, M.: Aximo: Automated axiomatic reasoning for information update. In: Proceedings of M4M5 2007. ENTCS, vol. 231, pp. 211–225. Elsevier (2009)

    Google Scholar 

  35. Schneider, S., Sidiropoulos, A.: CSP and Anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  36. Toninho, B., Caires, L.: A spatial-epistemic logic for reasoning about security protocols. In: Proceedings of SecCo 2010. EPTCS, vol. 51, pp. 1–15 (2010)

    Google Scholar 

  37. de Vries, W., de Boer, F.S., van der Hoek, W., Meyer, J.-J.Ch.: A Truly Concurrent Model for Interacting Agents. In: Yuan, S.-T., Yokoo, M. (eds.) PRIMA 2001. LNCS (LNAI), vol. 2132, pp. 16–30. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Philosophy Section, Faculty of Technology, Policy and Management, Delft University of Technology, The Netherlands

    Francien Dechesne

  2. Department of Computer Science, Eindhoven University of Technology, The Netherlands

    Mohammad Reza Mousavi

Authors
  1. Francien Dechesne
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohammad Reza Mousavi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematical Sciences, New Mexico State University, 88003, Las Cruces, NM, USA

    Guram Bezhanishvili

  2. Department of Language and Information, Heinrich Heine Universität, Kruppstrasse 108, 40227, Düsseldorf, Germany

    Sebastian Löbner

  3. Dipartimento di Matematica "Fredigo Enriques", Università degli Studi di Milano, via Cesare Saldini, 50, 20133, Milan, Italy

    Vincenzo Marra

  4. Seminar für Sprachwissenschaft, Universität Tübingen, Wilhelmstraße 19, 72074, Tübingen, Germany

    Frank Richter

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dechesne, F., Reza Mousavi, M. (2013). Interpreted Systems Semantics for Process Algebra with Identity Annotations. In: Bezhanishvili, G., Löbner, S., Marra, V., Richter, F. (eds) Logic, Language, and Computation. TbiLLC 2011. Lecture Notes in Computer Science, vol 7758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36976-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-36976-6_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-36975-9

  • Online ISBN: 978-3-642-36976-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation