%0 Conference Proceedings
%T Psi-Calculi Revisited: Connectivity and Compositionality
%+ Data61 [Canberra] (CSIRO)
%+ University of New South Wales [Sydney] (UNSW)
%A Åman Pohjola, Johannes
%Z Part 1: Full Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Copenhagen, Denmark
%Y Jorge A. Pérez
%Y Nobuko Yoshida
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-11535
%P 3-20
%8 2019-06-17
%D 2019
%R 10.1007/978-3-030-21759-4_1
%K Process algebra
%K Psi-calculi
%K Nominal logic
%K Interactive theorem proving
%K Bisimulation
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Mechanised proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework.A limitation of psi-calculi is that communication channels must be symmetric and transitive. In this paper, we give a new operational semantics to psi-calculi that allows us to lift these restrictions and simplify some of the proofs. The key technical innovation is to annotate transitions with a provenance—a description of the scope and channel they originate from.We give mechanised proofs that our extension is conservative, and that the standard algebraic and congruence properties of bisimilarity are maintained. We show correspondence with a reduction semantics and barbed bisimulation. We show how a pi-calculus with preorders that was previously beyond the scope of psi-calculi can be captured, and how to encode mixed choice under very strong quality criteria.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-02313748/document
%2 https://inria.hal.science/hal-02313748/file/478668_1_En_1_Chapter.pdf
%L hal-02313748
%U https://inria.hal.science/hal-02313748
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-11535