Psi-calculi: a framework for mobile processes with nominal data and logic

Jesper Bengtson; Magnus Johansson; Joachim Parrow; BjÃ¶rn Victor

doi:10.2168/LMCS-7(1:11)2011

Jesper Bengtson ; Magnus Johansson ; Joachim Parrow ; BjÃ¶rn Victor - Psi-calculi: a framework for mobile processes with nominal data and logic

lmcs:696 - Logical Methods in Computer Science, March 29, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:11)2011

Psi-calculi: a framework for mobile processes with nominal data and logicArticle

Authors: Jesper Bengtson ; Magnus Johansson ; Joachim Parrow ; BjÃ¶rn Victor

The framework of psi-calculi extends the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Psi-calculi can capture the same phenomena as other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions. We provide ample comparisons to related calculi and discuss a few significant applications. Our labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic properties of psi-calculi, all of which have been checked in the interactive theorem prover Isabelle. Expressiveness of psi-calculi significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.

https://doi.org/10.2168/LMCS-7(1:11)2011

Source: arXiv.org:1101.3262

Volume: Volume 7, Issue 1

Published on: March 29, 2011

Imported on: December 30, 2009

Keywords: Computer Science - Logic in Computer Science,F.1.2, F.3.1, F.3.2

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

52 Documents citing this article

Alex Rønning Bendixen;Bjarke Bredow Bojesen;Hans Hüttel;Stian Lybech, 2022, A Generic Type System for Higher-Order Ψ-calculi, arXiv (Cornell University), 368, pp. 43-59, 10.4204/eptcs.368.3.

Stian Lybech, 2022, Encodability and Separation for a Reflective Higher-Order Calculus, arXiv (Cornell University), 368, pp. 95-112, 10.4204/eptcs.368.6.

Yehia Abd Alrahman;Mauricio Martel;Nir Piterman, Lecture notes in computer science, A PO Characterisation of Reconfiguration, pp. 42-59, 2022, 10.1007/978-3-031-17715-6_5.

Mauricio Cano;Hugo A. López;Jorge A. Pérez;Camilo Rueda, 2021, Session-based concurrency, declaratively, Acta Informatica, 59, 1, pp. 1-87, 10.1007/s00236-021-00395-w, https://doi.org/10.1007/s00236-021-00395-w.

Ross Horne;Sjouke Mauw;Semen Yurkov, Lecture notes in computer science, Compositional Analysis of Protocol Equivalence in the Applied $$\pi $$-Calculus Using Quasi-open Bisimilarity, pp. 235-255, 2021, 10.1007/978-3-030-85315-0_14, https://doi.org/10.1007/978-3-030-85315-0_14.

Yehia Abd Alrahman;Nir Piterman, 2021, Modelling and verification of reconfigurable multi-agent systems, Autonomous Agents and Multi-Agent Systems, 35, 2, 10.1007/s10458-021-09521-x, https://doi.org/10.1007/s10458-021-09521-x.

Doriana Medić;Claudio Antares Mezzina;Iain Phillips;Nobuko Yoshida, 2020, A parametric framework for reversible π-calculi, Information and Computation, 275, pp. 104644, 10.1016/j.ic.2020.104644, https://doi.org/10.1016/j.ic.2020.104644.

Ioana Cristescu;Thomas Given-Wilson;Axel Legay, 2020, Expressiveness of concurrent intensionality, Theoretical Computer Science, 837, pp. 54-83, 10.1016/j.tcs.2020.05.007, https://doi.org/10.1016/j.tcs.2020.05.007.

Wolfgang Jeltsch, arXiv (Cornell University), A Process Calculus for Formally Verifying Blockchain Consensus Protocols, pp. 24-39, 2020, 10.1007/978-3-030-46714-2_2, https://arxiv.org/abs/1911.08033.

Jean-Bernard Stefani;Martin Vassor, Encapsulation and Sharing in Dynamic Software Architectures: The Hypercell Framework, pp. 242-260, 2019, 10.1007/978-3-030-21759-4_14, https://hal.inria.fr/hal-02313751/file/478668_1_En_14_Chapter.pdf.

Johannes Åman Pohjola, Psi-Calculi Revisited: Connectivity and Compositionality, pp. 3-20, 2019, 10.1007/978-3-030-21759-4_1, https://hal.inria.fr/hal-02313748/file/478668_1_En_1_Chapter.pdf.

Rob van Glabbeek, 2019, Ensuring liveness properties of distributed systems: Open problems, Journal of Logical and Algebraic Methods in Programming, 109, pp. 100480, 10.1016/j.jlamp.2019.100480, https://doi.org/10.1016/j.jlamp.2019.100480.

Rocco De Nicola;Gianluigi Ferrari;Rosario Pugliese;Francesco Tiezzi, 2019, A formal approach to the engineering of domain-specific distributed systems, Journal of Logical and Algebraic Methods in Programming, 111, pp. 100511, 10.1016/j.jlamp.2019.100511, https://doi.org/10.1016/j.jlamp.2019.100511.

Thomas Given-Wilson;Axel Legay, On the Expressiveness of Joining and Splitting, pp. 326-355, 2019, 10.1007/978-3-030-22348-9_20, https://hal.inria.fr/hal-01955922.

Thomas Troels Hildebrandt;Christian Johansen;Håkon Normann, 2019, A stable non-interleaving early operational semantics for the pi-calculus, Journal of Logical and Algebraic Methods in Programming, 104, pp. 227-253, 10.1016/j.jlamp.2019.02.006, https://doi.org/10.1016/j.jlamp.2019.02.006.

Yehia Abd Alrahman;Rocco De Nicola;Michele Loreti, 2019, A calculus for collective-adaptive systems and its behavioural theory, Information and Computation, 268, pp. 104457, 10.1016/j.ic.2019.104457, https://doi.org/10.1016/j.ic.2019.104457.

Doriana Medic;Claudio Antares Mezzina;Iain Phillips;Nobuko Yoshida, 2018, A Parametric Framework for Reversible Pi-Calculi, arXiv (Cornell University), 276, pp. 87-103, 10.4204/eptcs.276.8.

Jens Aagaard;Hans Hüttel;Mathias Jakobsen;Mikkel Kettunen, 2018, Context-Free Session Types for Applied Pi-Calculus, arXiv (Cornell University), 276, pp. 3-18, 10.4204/eptcs.276.3.

Martín Abadi;Bruno Blanchet;Cédric Fournet, 2017, The Applied Pi Calculus, Journal of the ACM, 65, 1, pp. 1-41, 10.1145/3127586, https://doi.org/10.1145/3127586.

Myrto Arapinis;Jia Liu;Eike Ritter;Mark Ryan, 2017, Stateful applied pi calculus: Observational equivalence and labelled bisimilarity, Journal of Logical and Algebraic Methods in Programming, 89, pp. 95-149, 10.1016/j.jlamp.2017.03.001, https://doi.org/10.1016/j.jlamp.2017.03.001.

Thomas Troels Hildebrandt;Christian Johansen;Håkon Normann, Duo Research Archive (University of Oslo), A Stable Non-interleaving Early Operational Semantics for the Pi-Calculus, pp. 51-63, 2017, 10.1007/978-3-319-53733-7_3, http://hdl.handle.net/10852/77405.

Hans Hüttel, Lecture notes in computer science, Binary Session Types for Psi-Calculi, pp. 96-115, 2016, 10.1007/978-3-319-47958-3_6.

Håkon Normann;Christian Johansen;Thomas Hildebrandt, 2016, Declarative event based models of concurrency and refinement in psi-calculi, Journal of Logical and Algebraic Methods in Programming, 85, 3, pp. 368-398, 10.1016/j.jlamp.2015.12.007, https://doi.org/10.1016/j.jlamp.2015.12.007.

Johannes Åman Pohjola;Joachim Parrow, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Bisimulation up-to techniques for psi-calculi, pp. 142-153, 2016, St. Petersburg FL USA, 10.1145/2854065.2854080.

Stéphanie Delaune;Lucca Hirschi, 2016, A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols, Journal of Logical and Algebraic Methods in Programming, 87, pp. 127-144, 10.1016/j.jlamp.2016.10.005, https://doi.org/10.1016/j.jlamp.2016.10.005.

Thomas Given-Wilson;Axel Legay, On the Expressiveness of Symmetric Communication, pp. 139-157, 2016, 10.1007/978-3-319-46750-4_9, https://hal.inria.fr/hal-01241839.

Hanne Riis Nielson;Flemming Nielson;Roberto Vigo, 2015, A calculus of quality for robustness against unreliable communication, Journal of Logical and Algebraic Methods in Programming, 84, 5, pp. 611-639, 10.1016/j.jlamp.2015.04.002, https://doi.org/10.1016/j.jlamp.2015.04.002.

Jean-Bernard Stefani, Components as Location Graphs, pp. 3-23, 2015, 10.1007/978-3-319-15317-9_1, https://hal.inria.fr/hal-01094208.

Jesper Bengtson;Joachim Parrow;Tjark Weber, 2015, Psi-Calculi in Isabelle, Journal of Automated Reasoning, 56, 1, pp. 1-47, 10.1007/s10817-015-9336-2.

Johannes Borgstrom;Ramūnas Gutkovas;Ioana Rodhe;Björn Victor, 2015, The Psi-Calculi Workbench, KTH Publication Database DiVA (KTH Royal Institute of Technology), 14, 1, pp. 1-25, 10.1145/2682570, http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-233750.

Thomas Given-Wilson;Axel Legay, 2015, On the Expressiveness of Joining, arXiv (Cornell University), 189, pp. 99-113, 10.4204/eptcs.189.9.

Cristian Prisacariu, 2014, Actor Network Procedures as Psi-calculi for Security Ceremonies, arXiv (Cornell University), 148, pp. 63-77, 10.4204/eptcs.148.5.

Hans Hüttel, Lecture notes in computer science, Types for Resources in $$\psi $$-calculi, pp. 83-102, 2014, 10.1007/978-3-319-05119-2_6.

Håkon Normann;Cristian Prisacariu;Thomas Hildebrandt, 2014, Concurrency Models with Causality and Events as Psi-calculi, arXiv (Cornell University), 166, pp. 4-20, 10.4204/eptcs.166.3.

Johannes Borgström;Ramūnas Gutkovas;Joachim Parrow;Björn Victor;Johannes Åman Pohjola, CiteSeer X (The Pennsylvania State University), A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract), pp. 103-118, 2014, 10.1007/978-3-319-14128-2_7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.298.3632.

Johannes Borgström;Ramūnas Gutkovas;Joachim Parrow;Björn Victor;Johannes Åman Pohjola, CiteSeer X (The Pennsylvania State University), A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract), pp. 103-118, 2014, 10.1007/978-3-319-05119-2_7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.298.3632.

Johannes Åman Pohjola;Joachim Parrow, 2014, Priorities Without Priorities: Representing Preemption in Psi-Calculi, arXiv (Cornell University), 160, pp. 2-15, 10.4204/eptcs.160.2.

Jos C.M. Baeten;Davide Sangiorgi, Data Archiving and Networked Services (DANS), Concurrency Theory: A Historical Perspective on Coinduction and Process Calculi, pp. 399-442, 2014, 10.1016/b978-0-444-51624-4.50009-5, https://ir.cwi.nl/pub/23510.

Myrto Arapinis;Jia Liu;Eike Ritter;Mark Ryan, Lecture notes in computer science, Stateful Applied Pi Calculus, pp. 22-41, 2014, 10.1007/978-3-642-54792-8_2, https://doi.org/10.1007/978-3-642-54792-8_2.

Thomas Given-Wilson, Expressiveness via Intensionality and Concurrency, pp. 206-223, 2014, 10.1007/978-3-319-10882-7_13, https://hal.inria.fr/hal-00999082.

Thomas Given-Wilson, 2014, An Intensional Concurrent Faithful Encoding of Turing Machines, arXiv (Cornell University), 166, pp. 21-37, 10.4204/eptcs.166.4.

Thomas Given-Wilson, 2014, On the Expressiveness of Intensional Communication, arXiv (Cornell University), 160, pp. 30-46, 10.4204/eptcs.160.4.

Vincenzo Ciancia;Matteo Sammartino, CiteSeer X (The Pennsylvania State University), A Class of Automata for the Verification of Infinite, Resource-Allocating Behaviours, pp. 97-111, 2014, 10.1007/978-3-662-45917-1_7, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.589.2217.

Carlos Olarte;Camilo Rueda;Frank D. Valencia, 2013, Models and emerging trends of concurrent constraint programming, 18, 4, pp. 535-578, 10.1007/s10601-013-9145-3, https://hal.inria.fr/hal-00869192.

Joachim Parrow;Johannes Borgström;Palle Raabjerg;Johannes Åman Pohjola, 2013, Higher-order psi-calculi, Mathematical Structures in Computer Science, 24, 2, 10.1017/s0960129513000170.

Johannes Borgstrom;Ramunas Gutkovas;Ioana Rodhe;Bjorn Victor, 2013 13th International Conference on Application of Concurrency to System Design, A Parametric Tool for Applied Process Calculi, 1119, pp. 180-185, 2013, Barcelona, Spain, 10.1109/acsd.2013.22.

Johannes Borgström;Shuqin Huang;Magnus Johansson;Palle Raabjerg;Björn Victor;et al., 2013, Broadcast psi-calculi with an application to wireless protocols, Uppsala University Publications (Uppsala University), 14, 1, pp. 201-216, 10.1007/s10270-013-0375-z, http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-205258.

Thomas Given-Wilson;Daniele Gorla, Lecture notes in computer science, Pattern Matching and Bisimulation, pp. 60-74, 2013, 10.1007/978-3-642-38493-6_5, https://doi.org/10.1007/978-3-642-38493-6_5.

Magnus Johansson;Björn Victor;Joachim Parrow, 2012, Computing strong and weak bisimulations for psi-calculi, The Journal of Logic and Algebraic Programming, 81, 3, pp. 162-180, 10.1016/j.jlap.2012.01.001, https://doi.org/10.1016/j.jlap.2012.01.001.

Cezary Kaliszyk;Henk Barendregt, CiteSeer X (The Pennsylvania State University), Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem, pp. 87-102, 2011, 10.1007/978-3-642-25379-9_9, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.703.934.

Johannes Borgström;Shuqin Huang;Magnus Johansson;Palle Raabjerg;Björn Victor;et al., KTH Publication Database DiVA (KTH Royal Institute of Technology), Broadcast Psi-calculi with an Application to Wireless Protocols, pp. 74-89, 2011, 10.1007/978-3-642-24690-6_7, http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-156736.

Pedro Matiello;Ana C. V. de Melo, Lecture notes in computer science, PiStache: Implementing π-Calculus in Scala, pp. 76-91, 2011, 10.1007/978-3-642-25032-3_6.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 32544 times.

This article's PDF has been downloaded 460 times.