Document Open Access Logo

An Intensionally Fully-abstract Sheaf Model for pi

Authors Clovis Eberhart, Tom Hirschowitz, Thomas Seiller

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.86.pdf
  • Filesize: 0.57 MB
  • 15 pages

Document Identifiers

Author Details

Clovis Eberhart
Tom Hirschowitz
Thomas Seiller

Cite As Get BibTex

Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An Intensionally Fully-abstract Sheaf Model for pi. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 86-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.86

Abstract

Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.

Subject Classification

Keywords
  • concurrency
  • sheaves
  • causal models
  • games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409-470, 2000. Google Scholar
  2. Gérard Berry and Gérard Boudol. The chemical abstract machine. In POPL, pages 81-94, 1990. Google Scholar
  3. Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, and Alexandra Silva. Deriving syntax and axioms for quantitative regular behaviours. In CONCUR, volume 5710 of LNCS, pages 146-162. Springer, 2009. Google Scholar
  4. Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the π-calculus. Acta Informatica, 35(5):353-400, 1998. Google Scholar
  5. Ed Brinksma, Arend Rensink, and Walter Vogler. Fair testing. In CONCUR, volume 962 of LNCS, pages 313-327. Springer, 1995. Google Scholar
  6. Nadia Busi and Roberto Gorrieri. Distributed semantics for the π-calculus based on Petri nets with inhibitor arcs. Journal of Logic and Algebraic Programming, 78(3):138-162, 2009. Google Scholar
  7. Diletta Cacciagrano, Flavio Corradini, and Catuscia Palamidessi. Explicit fairness in testing semantics. Logical Methods in Computer Science, 5(2), 2009. Google Scholar
  8. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of pcf. In LICS. IEEE Computer Society, 2015. Google Scholar
  9. Gian Luca Cattani and Peter Sewell. Models for name-passing processes: Interleaving and causal. In LICS, pages 322-333. IEEE Computer Society, 2000. Google Scholar
  10. Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. Event structure semantics of parallel extrusion in the pi-calculus. In FoSSaCS, volume 7213 of LNCS, pages 225-239. Springer, 2012. Google Scholar
  11. Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984. Google Scholar
  12. Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. A πlayground. http://lama.univ-smb.fr/~hirschowitz/papers/pilayground.pdf, 2015.
  13. Joost Engelfriet. A multiset semantics for the pi-calculus with replication. Theoretical Computer Science, 153(1&2):65-94, 1996. Google Scholar
  14. Marcelo P. Fiore, Eugenio Moggi, and Davide Sangiorgi. A fully-abstract model for the pi-calculus (extended abstract). In LICS, pages 43-54. IEEE Computer Society, 1996. Google Scholar
  15. Peter Freyd and G. M. Kelly. Categories of continuous functors, I. Journal of Pure and Applied Algebra, 2:169-191, 1972. Google Scholar
  16. Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, 2001. Google Scholar
  17. Gregor Gößler, Daniel Le Métayer, and Jean-Baptiste Raclet. Causality analysis in contract violation. In Runtime Verification, volume 6418 of LNCS, pages 270-284. Springer, 2010. Google Scholar
  18. Russell Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for innocent strategies. In LICS, pages 379-388. IEEE Computer Society, 2007. Google Scholar
  19. Matthew Hennessy. A fully abstract denotational semantics for the π-calculus. Theoretical Computer Science, 278(1-2):53-89, 2002. Google Scholar
  20. Thomas T. Hildebrandt. Towards categorical models for fairness: fully abstract presheaf semantics of SCCS with finite delay. Theoretical Computer Science, 294(1/2):151-181, 2003. Google Scholar
  21. Tom Hirschowitz. Full abstraction for fair testing in CCS. In CALCO, volume 8089 of LNCS, pages 175-190. Springer, 2013. Google Scholar
  22. Tom Hirschowitz. Full abstraction for fair testing in CCS (expanded version). Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  23. Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive equivalences for CCS. In ICE, pages 2-24, 2011. Google Scholar
  24. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. Google Scholar
  25. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  26. André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps. In LICS, pages 418-427. IEEE Computer Society, 1993. Google Scholar
  27. James Laird. Game semantics for higher-order concurrency. In FSTTCS, volume 4337 of LNCS, pages 417-428. Springer, 2006. Google Scholar
  28. Saunders Mac Lane. Duality for groups. Bulletin of the American Mathematical Society, 56, 1950. Google Scholar
  29. Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer, 2nd edition, 1998. Google Scholar
  30. Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. Springer, 1992. Google Scholar
  31. Guy McCusker, John Power, and Cai Wingfield. A graphical foundation for schedules. Electronic Notes in Theoretical Computer Science, 286:273-289, 2012. Google Scholar
  32. Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional linear logic. In LICS, pages 386-395. IEEE Computer Society, 2005. Google Scholar
  33. Paul-André Melliès. Game semantics in string diagrams. In LICS, pages 481-490. IEEE, 2012. Google Scholar
  34. Ugo Montanari and Marco Pistore. Concurrent semantics for the π-calculus. Electronic Notes in Theoretical Computer Science, 1:411-429, 1995. Google Scholar
  35. V. Natarajan and Rance Cleaveland. Divergence and fair testing. In ICALP, volume 944 of LNCS, pages 648-659. Springer, 1995. Google Scholar
  36. Hanno Nickau. Hereditarily sequential functionals. In LFCS, volume 813 of LNCS, pages 253-264. Springer, 1994. Google Scholar
  37. M. Nielsen, G. Plotkin, and G. Winskel. Event structures and domains, part 1. Theoretical Computer Science, 13:65-108, 1981. Google Scholar
  38. Arend Rensink and Walter Vogler. Fair testing. Information and Computation, 205(2):125-198, 2007. Google Scholar
  39. Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, pages 409-418. IEEE Computer Society, 2011. Google Scholar
  40. Ian Stark. A fully abstract domain model for the π-calculus. In LICS, pages 36-42. IEEE Computer Society, 1996. Google Scholar
  41. Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In LICS. IEEE Computer Society, 2015. Google Scholar
  42. Glynn Winskel. Event structure semantics for CCS and related languages. In Mogens Nielsen and Erik Meineche Schmidt, editors, ICALP, volume 140 of LNCS, pages 561-576. Springer, 1982. Google Scholar
  43. Glynn Winskel. Strategies as profunctors. In FoSSaCS, volume 7794 of LNCS, pages 418-433. Springer, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact