| 1. |
|
|
| 2. |
- Bengtson, Jesper, et al.
(författare)
-
A completeness proof for bisimulation in the pi-calculus using Isabelle
- 2007
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 192:1, s. 61-75
-
Tidskriftsartikel (refereegranskat)abstract
- We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt;rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.
|
|
| 3. |
- Bengtson, Jesper, 1977-
(författare)
-
Formalising process calculi
- 2010
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- As the complexity of programs increase, so does the complexity of the models required to reason about them. Process calculi were introduced in the early 1980s and have since then been used to model communication protocols of varying size and scope. Whereas modeling sophisticated protocols in simple process algebras like CCS or the pi-calculus is doable, expressing the models required is often gruesome and error prone. To combat this, more advanced process calculi were introduced, which significantly reduce the complexity of the models. However, this simplicity comes at a price -- the theories of the calculi themselves instead become gruesome and error prone, establishing their mathematical and logical properties has turned out to be difficult. Many of the proposed calculi have later turned out to be inconsistent.The contribution of this thesis is twofold. First we provide methodologies to formalise the meta-theory of process calculi in an interactive theorem prover. These are used to formalise significant parts of the meta-theory of CCS and the pi-calculus in the theorem prover Isabelle, using Nominal Logic to allow for a smooth treatment of the binders. Second we introduce and formalise psi-calculi, a framework for process calculi incorporating several existing ones, including those we already formalised, and which is significantly simpler and substantially more expressive. Our methods scale well as complexity of the calculi increases.The formalised results for all calculi include congruence results for both strong and weak bisimilarities, in the case of the pi-calculus for both the early and the late operational semantics. For the finite pi-calculus, we also formalise the proof that the axiomatisation of strong late bisimilarity is sound and complete. We believe psi-calculi to be the state of the art of process calculi, and our formalisation to be the most extensive formalisation of process calculi ever done inside a theorem prover.
|
|
| 4. |
- Bengtson, Jesper, et al.
(författare)
-
Formalising the pi-calculus using nominal logic
- 2007
-
Ingår i: FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS. - 9783540713883 ; , s. 63-77
-
Konferensbidrag (refereegranskat)abstract
- We formalise the pi-calculus using the nominal datatype package, a package based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely following the intuitive arguments found in manual proofs. In this way we have covered many of the standard theorems of bisimulation equivalence and congruence, both late and early, and both strong and weak in a unison manner. We thus provide one of the most extensive formalisations of a process calculus ever done inside a theorem prover. A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic.
|
|
| 5. |
|
|
| 6. |
- Bengtson, Jesper, et al.
(författare)
-
Psi-calculi : a framework for mobile processes with nominal data and logic
- 2011
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 7:1, s. 11-
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 7. |
- Bengtson, Jesper, et al.
(författare)
-
Psi-calculi : Mobile processes, nominal data, and logic
- 2009
-
Ingår i: Proc. 24th Annual IEEE Symposium on Logic in Computer Science. - Piscataway, NJ : IEEE. - 9780769537467 ; , s. 39-48
-
Konferensbidrag (refereegranskat)abstract
- A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Other proposed extensions of pi can be formulated as psi-calculi; examples include 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 a predicate logic for assertions. 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. The proofs are transparent enough to be checked in the interactive proof checker Isabelle. We are the first to formulate a truly compositional labelled operational semantics for calculi of this caliber. Expressiveness and therefore modelling convenience significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.
|
|
| 8. |
- Bengtson, Jesper, et al.
(författare)
-
Psi-Calculi in Isabelle
- 2016
-
Ingår i: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 56:1, s. 1-47
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date.
|
|
| 9. |
- Bengtson, Jesper, et al.
(författare)
-
Psi-calculi in Isabelle
- 2009
-
Ingår i: Theorem Proving in Higher Order Logics. - Berlin : Springer-Verlag. - 9783642033582 ; , s. 99-114
-
Konferensbidrag (refereegranskat)abstract
- Psi-calculi are extensions of the pi-calculus, accommodating arbitrary nominal datatypes to represent not only data but also communication channels, assertions and conditions, giving it an expressive power beyond the applied pi-calculus and the concurrent constraint pi-calculus.We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored.The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. We discuss two approaches to reasoning about binding sequences along with their strengths and weaknesses. We also cover custom induction rules to remove the bulk of manual alpha-conversions.
|
|
| 10. |
- Bengtson, Jesper, 1977-, et al.
(författare)
-
Refinement Types for Secure Implementations
- 2008
-
Ingår i: Proc. 21st IEEE Computer Security Foundations Symposium. - Piscataway, NJ : IEEE. - 9780769531823 ; , s. 17-32
-
Konferensbidrag (refereegranskat)
|
|
| 11. |
- Johansson, Magnus, et al.
(författare)
-
Extended pi-Calculi
- 2008
-
Ingår i: Automata, Languages and Programming, PT 2. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540705826 ; , s. 87-98
-
Konferensbidrag (refereegranskat)abstract
- We demonstrate a general framework for extending the pi-calculus with data terms. In this we generalise and improve on several related efforts such as the spi-calculus and the applied pi-calculus, also including pattern matching and polyadic channels. Our framework uses a single untyped notion of agent, name and scope, an operational semantics without structural equivalence and a simple definition of bisimilarity. We provide general criteria on the semantic equivalence of data terms; with these we prove algebraic laws and that bisimulation is preserved by the operators in the usual way. The definitions are simple enough that an implementation in an automated proof assistant is feasible.
|
|
| 12. |
- Johansson, Magnus, et al.
(författare)
-
Weak Equivalences in Psi-calculi
- 2010
-
Ingår i: Proc. 25th Symposium on Logic in Computer Science. - Piscataway, NJ : IEEE. - 9781424475889 ; , s. 322-331
-
Konferensbidrag (refereegranskat)abstract
- Psi-calculi extend the pi-calculus with nominal datatypes to represent data, communication channels, and logics for facts and conditions. This general framework admits highly expressive formalisms such as concurrent higher-order constraints and advanced cryptographic primitives. We here establish the theory of weak bisimulation, where the tau actions are unobservable. In comparison to other calculi the presence of assertions poses a significant challenge in the definition of weak bisimulation, and although there appears to be a spectrum of possibilities we show that only a few are reasonable. We demonstrate that the complications mainly stem from psi-calculi where the associated logic does not satisfy weakening. We prove that weak bisimulation equivalence has the expected algebraic properties and that the corresponding observation congruence is preserved by all operators. These proofs have been machine checked in Isabelle. The notion of weak barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of barbs in all static contexts. We prove that weak barbed equivalence coincides with weak bisimulation equivalence.
|
|
