| 1. |
- Baldamus, Michael, et al.
(författare)
-
A Fully Abstract Encoding of the pi-Calculus with Data Terms
- 2005
-
Ingår i: Proceedings of ICALP 2005. - Berlin : Springer. - 3540275800 ; , s. 1202-1213
-
Konferensbidrag (refereegranskat)abstract
- The π-calculus with data terms (πT) extends the pure π-calculus by data constructors and destructors and allows data to be transmitted between agents. It has long been known how to encode such data types in π, but until now it has been open how to make the encoding fully abstract, meaning that two encodings (in π) are semantically equivalent precisely when the original πT agents are semantically equivalent. We present a new type of encoding and prove it to be fully abstract with respect to may-testing equivalence. To our knowledge this is the first result of its kind, for any calculus enriched with data terms. It has particular importance when representing security properties since attackers can be regarded as may-test observers. Full abstraction proves that it does not matter whether such observers are formulated in π or πT, both are equally expressive in this respect. The technical new idea consists of achieving full abstraction by encoding data as table entries rather than active processes, and using a firewalled central integrity manager to ensure data security.
|
|
| 2. |
- Baldamus, Michael, et al.
(författare)
-
Spi Calculus Translated to pi-Calculus Preserving May-Testing
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a concise and natural encoding of the spi-calculus into the more basic pi-calculus and establish its correctness with respect to a formal notion of testing. This is particularly relevant for security protocols modelled in spi since the tests can be viewed as adversaries. The translation has been implemented in a prototype tool. As a consequence, protocols can be described in the spi calculus and analysed with the emerging flora of tools already available for pi. The translation also entails a more detailed operational understanding of spi since high level constructs like encryption are encoded in a well known lower level. The formal correctness proof is nontrivial and interesting in its own; so called context bisimulations and new techniques for compositionality make the proof simpler and more concise.
|
|
| 3. |
- Baldamus, Michael, et al.
(författare)
-
Spi Calculus Translated to pi-Calculus Preserving May-Tests
- 2004
-
Ingår i: Proceedings of LICS 2004. - Los Alamitos, Calif : IEEE Computer Society. - 0769521924 ; , s. 22-31
-
Konferensbidrag (refereegranskat)abstract
- We present a concise and natural encoding of the spi-calculus into the more basic pi-calculus and establish its correctness with respect to a formal notion of testing. This is particularly relevant for security protocols modelled in spi since the tests can be viewed as adversaries. The translation has been implemented in a prototype tool. As a consequence, protocols can be described in the spi calculus and analysed with the emerging flora of tools already available for pi. The translation also entails a more detailed operational understanding of spi since high level constructs like encryption are encoded in a well known lower level. The formal correctness proof is nontrivial and interesting in its own; so called context bisimulations and new techniques for compositionality make the proof simpler and more concise.
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
|
|
| 8. |
- 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.
|
|
| 9. |
- 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.
|
|
| 10. |
- 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.
|
|
| 11. |
- 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.
|
|
| 12. |
- Berg, Therese
(författare)
-
Regular inference for reactive systems
- 2006
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Models of reactive systems play a central role in many techniques for verification and analysis of reactive systems. Both a specification of the system and the abstract behavior of the system can be expressed in a formal model. Compliance with the functional parts in the specification can be controlled in different ways. Model checking techniques can be applied to a model of the system or directly to source code. In testing, model-based techniques can generate test suites from specification. A bottleneck in model-based techniques is however to construct a model of the system. This work concerns a technique that automatically constructs a model of a system without access to specification, code or internal structure. We assume that responses of the system to sequences of input can be observed. In this setting, so called regular inference techniques build a model of the system based on system responses to selected input sequences.There are three main contributions in this thesis. The first is a survey on the most well-known techniques for regular inference. The second is an analysis of Angluin's algorithm for regular inference on synthesized examples. On a particular type of examples, with prefix-closed languages, typically used to model reactive systems, the required number of input sequences grow approximately quadratically in the number of transitions of the system. However, using an optimization for systems with prefix-closed languages we were able to reduce the number of required input sequences with about 20%. The third contribution is a developed regular inference technique for systems with parameters. This technique aims to better handle entities of communications protocols where messages normally have many parameters of which few determine the subsequent behavior of the system. Experiments with our implementation of the technique confirm a reduction of the required number of input sequences, in comparison with Angluin's algorithm.
|
|
| 13. |
- Borgström, Johannes, et al.
(författare)
-
A Sorted Semantic Framework for Applied Process Calculi
- 2016
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 12:1, s. 1-49
-
Tidskriftsartikel (refereegranskat)abstract
- Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can directly represent several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation; the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.
|
|
| 14. |
- Borgström, Johannes, et al.
(författare)
-
A Sorted Semantic Framework for Applied Process Calculi (extended abstract)
- 2014
-
Ingår i: Trustworthy Global Computing. - Cham : Springer Berlin/Heidelberg. - 9783319051185 ; , s. 103-118
-
Konferensbidrag (refereegranskat)abstract
- Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can accommodate several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Substantial parts of the meta-theory of sorted psi-calculi have been machine-checked using Nominal Isabelle.
|
|
| 15. |
- Borgström, Johannes, et al.
(författare)
-
Broadcast psi-calculi with an application to wireless protocols
- 2015
-
Ingår i: Software and Systems Modeling. - : Springer. - 1619-1366 .- 1619-1374. ; 14:1, s. 201-216
-
Tidskriftsartikel (refereegranskat)abstract
- Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.
|
|
| 16. |
- Borgström, Johannes, et al.
(författare)
-
Broadcast Psi-calculi with an Application to Wireless Protocols
- 2011
-
Ingår i: Software Engineering and Formal Methods. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642246890 ; , s. 74-89
-
Konferensbidrag (refereegranskat)abstract
- Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication % to the psi-calculi framework. in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.
|
|
| 17. |
|
|
| 18. |
- Cleaveland, Rance, et al.
(författare)
-
The Concurrency Workbench : A Semantics Based Tool for the Verification of Concurrent Systems
- 1993
-
Ingår i: ACM Transactions on Programming Languages and Systems. - : Association for Computing Machinery (ACM). - 0164-0925 .- 1558-4593. ; 15:1, s. 36-72
-
Tidskriftsartikel (refereegranskat)abstract
- The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.
|
|
| 19. |
- Cleaveland, Rance, et al.
(författare)
-
The concurrency workbench: A semantics based tool for the verification of concurrent systems
- 1991. - 1
-
Rapport (refereegranskat)abstract
- The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key features is its breadht: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.
|
|
| 20. |
- Gengelbach, Arve
(författare)
-
Conservative Definitions for Higher-order Logic with Ad-hoc Overloading
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- With an ever growing dependency on computer systems, the need to guarantee their correct behaviour increases. Mathematically rigorous techniques like formal verification offer a way to derive a system's mathematical properties for example with the help of a theorem prover. A theorem prover is a type of software that assists a user in deriving theorems expressed in a formal language. With a theorem prover one should never be able to prove something that is contradictory, as otherwise the proof effort is worthless. This property is called consistency and is essential for formal developments.Theorem provers enjoy high confidence, since they often rely on a trusted logical kernel that is enriched with new symbols in a controlled way. Instead of asserting the existence of mathematical objects with their desired properties, new symbols are introduced through definitions. These definitions are checked by this kernel, and expected to act as abbreviations. Any theorem that is expressible without a definition should not need that definition in its proof. A definition satisfying this property is called conservative. Conservative definitions are especially important as they preserve consistency, so that a proof of a contradiction is not possible after adding these definitions.Isabelle/HOL is a prominent theorem prover with the unique feature of permitting different definitions of one constant at non-overlapping types. In addition to these so-called overloading definitions, a symbol may be used before it is defined. These features mean that consistency or conservativity arguments for simpler logics do not immediately apply to Isabelle/HOL. In the past, design flaws in the definitional mechanism made theories in the Isabelle/HOL theorem prover inconsistent, e.g. it was possible to derive a contradiction from cyclic definitions.With this thesis we show that (overloading) definitions in higher-order logic (HOL) are conservative, hence not source of inconsistency. We define and prove a notion of conservativity that applies to theories of overloading definitions in higher-order logic and formalise aspects of our results in a theorem prover. As a practical implication, when searching for a proof of a formula, our syntactic conservativity criterion allows to exclude irrelevant symbols. In particular, our results confirm that Isabelle/HOL theories are consistent, thus users cannot introduce contradictions through definitions. As a specialisation of our work, our notion of conservativity holds for variants of HOL without overloading. Overall, our work contributes to the understanding of higher-order logic with overloading definitions.
|
|
| 21. |
|
|
| 22. |
- Johansson, Magnus, et al.
(författare)
-
A Fully Abstract Symbolic Semantics for Psi-Calculi
- 2010
-
Ingår i: Proc. 6th Workshop on Structural Operational Semantics. ; , s. 17-31
-
Konferensbidrag (refereegranskat)abstract
- We present a symbolic transition system and bisimulation equivalence for psi-calculi, and show that it is fully abstract with respect to bisimulation congruence in the non-symbolic semantics. 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. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus. Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the semantics of a process does not change from the original.
|
|
| 23. |
- Johansson, Magnus, et al.
(författare)
-
Computing Strong and Weak Bisimulations for Psi-Calculi
- 2012
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier. - 1567-8326 .- 1873-5940. ; 81:3, s. 162-180
-
Tidskriftsartikel (refereegranskat)abstract
- We present a symbolic transition system and strong and weak bisimulation equivalences for psi-calculi, and show that they are fully abstract with respect to bisimulation congruences in the non-symbolic semantics. A procedure which computes the most general constraint under which two agents are bisimilar is developed and proved correct. 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. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus. Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the symbolic semantics makes exactly the same distinctions as the original.
|
|
| 24. |
- Johansson, Magnus, et al.
(författare)
-
Computing Strong and Weak Bisimulations for Psi-Calculi – with proofs
- 2011
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a symbolic transition system and strong and weak bisimulation equivalences for psi-calculi, and show that they are fully abstract with respect to bisimulation congruences in the non-symbolic semantics. A procedure which computes the most general constraint under which two agents are bisimilar is developed and proved correct. 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. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus. Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the symbolic semantics makes exactly the same distinctions as the original.
|
|
| 25. |
- 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.
|
|
| 26. |
- Johansson, Magnus, 1976-
(författare)
-
Psi-calculi: a framework for mobile process calculi : Cook your own correct process calculus - just add data and logic
- 2010
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- A psi-calculus is an extension of the pi-calculus with nominal data types for data structures, logical assertions, and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Expressiveness and therefore modelling convenience significantly exceed those of other formalisms: psi-calculi can capture the same phenomena as other extensions of the pi-calculus, and can be more general, e.g. by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions.Ample comparisons to related calculi are provided and a few significant applications are discussed. The labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. Minimal requirements on the nominal data and logic are established in order to prove general algebraic properties of psi-calculi. The purity of the semantics is on par with the pi-calculus.The theory of weak bisimulation is established, where the tau actions are unobservable. The notion of barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of weak barbs in all static contexts. It is proved that weak barbed equivalence coincides with weak bisimulation equivalence.A symbolic transition system and bisimulation equivalence is presented, and shown fully abstract with respect to bisimulation congruence in the non-symbolic semantics. The symbolic semantics is necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means processes are bisimilar in the symbolic setting if they are bisimilar in the original semantics.Psi-calculi remove the necessity of proving general properties every time a new mobile process calculus is defined. By properly instantiating the framework the properties are guaranteed to hold, thus removing the need to do tedious and error-prone proofs.
|
|
| 27. |
- 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.
|
|
| 28. |
- Jonsson, Bengt, et al.
(författare)
-
Deciding bisimulation equivalences for a class of non-finite-state programs
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Traditionally, many automatic program verification techniques are applicable only to finite-state programs. In this paper we show how to extend some verification techniques to infinite-state programs that may read, store, and write data but not perform any other computations. We present algorithms for deciding strong equivalence and observation equivalence, defined by bisimulations (as in CCS), between such programs. These algorithms have major applications in verification of communication protocols. The equivalence problems are shown to be NP-hard in the size of the programs.
|
|
| 29. |
|
|
| 30. |
- Laneve, Cosimo, et al.
(författare)
-
Solo diagrams
- 2001
-
Ingår i: Proceedings of TACS 2001. ; , s. 127-144
-
Konferensbidrag (refereegranskat)abstract
- We address the problems of implementing the replication operator efficiently in the solos calculus---a calculus of mobile processes without prefix. This calculus is expressive enough to admit an encoding of the whole fusion calculus and thus the pi-calculus.We show that nested occurrences of replication can be avoided, that the size of replicated terms can be limited to three particles, and that the usual unfolding semantics of replication can be replaced by three simple reduction rules. To illustrate the results and show how the calculus can be efficiently implemented we present a graphic representation of agents in the solos calculus, adapting ideas from interaction diagrams and pi-nets.
|
|
| 31. |
- Milner, Robin, et al.
(författare)
-
A Calculus of Mobile Processes - Part I
- 1992
-
Ingår i: Information and Computation. - : Elsevier BV. - 0890-5401 .- 1090-2651. ; 100:1, s. 1-40
-
Tidskriftsartikel (refereegranskat)
|
|
| 32. |
- Milner, Robin, et al.
(författare)
-
A Calculus of Mobile Processes - Part II
- 1992
-
Ingår i: Information and Computation. - : Elsevier BV. - 0890-5401 .- 1090-2651. ; 100:1, s. 41-77
-
Tidskriftsartikel (refereegranskat)
|
|
| 33. |
- Milner, Robin, et al.
(författare)
-
Modal Logics for Mobile Processes
- 1993
-
Ingår i: Theoretical Computer Science. - 0304-3975 .- 1879-2294. ; 114:1, s. 149-171
-
Tidskriftsartikel (refereegranskat)abstract
- In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterization in terms of a simple modal logic (sometimes called Hennessy-Milner logic). This paper first defines two forms of bisimulation equivalence for the π-calculus, a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterize the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice. The results are applicable to most value-passing process algebras.
|
|
| 34. |
- Orava, Fredrik, et al.
(författare)
-
An algebraic verification of a mobile network
- 1991. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In a mobile communication network some nodes change location, and are therefore connected to different other nodes at different points in time. We show how such a network can be formally defined and verified using the p-calculus, which is a development of CCS (Calculus of Communicating Systems) allowing port names to be sent as parameters in communication events. An example of a mobile network is the Public Land Mobile Network currently being developed by the European Telecommunication Standards Institute. We concentrate on the handover procedures which controls the dynamic topology of the network.
|
|
| 35. |
|
|
| 36. |
- Parrow, Joachim, et al.
(författare)
-
Algebraic theories for name-passing calculi
- 1993. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In a theory of processes the names are atomic data which can be exchanged and tested for identity, but which admit no other functions or predicates. A well-known example of a calculus for name-passing is the p-calculus, where names additionally are used as communication ports. We provide complete axiomatisations of late and early bisimulation equivalences in such calculi. Since neither of the equivalences is a congruence we also axiomatise the corresponing largest congruences. We consider a few variations of the signature of the language; among these, a calulus of deterministic processes which is reminiscent of sequential functional programs with a conditional construct. Most of our axioms are shown to be independent. The structure of the systems reveals the symmetries of the calculi and equivalences since they differ only by a few simple axioms.
|
|
| 37. |
- Parrow, Joachim, et al.
(författare)
-
Algebraic Theories of Name-Passing Calculi
- 1995
-
Ingår i: Information and Computation. - : Elsevier BV. - 0890-5401 .- 1090-2651. ; 120:2, s. 174-197
-
Tidskriftsartikel (refereegranskat)
|
|
| 38. |
- Parrow, Joachim
(författare)
-
An introduction to the pi-calculus
- 2001
-
Ingår i: Handbook of Pocess Algebra. - : Elsevier. ; , s. 479-543
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)
|
|
| 39. |
|
|
| 40. |
|
|
| 41. |
- Parrow, Joachim
(författare)
-
Expressiveness of Process Algebras
- 2008
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 209, s. 173-186
-
Tidskriftsartikel (refereegranskat)abstract
- We examine ways to measure expressiveness of process algebras, and recapitulate and compare some related results from the literature.
|
|
| 42. |
- Parrow, Joachim
(författare)
-
General conditions for full abstraction
- 2016
-
Ingår i: Mathematical Structures in Computer Science. - 0960-1295 .- 1469-8072. ; 26:4, s. 655-657
-
Tidskriftsartikel (refereegranskat)
|
|
| 43. |
- Parrow, Joachim, et al.
(författare)
-
Higher-order psi-calculi
- 2014
-
Ingår i: Mathematical Structures in Computer Science. - : Cambridge University Press. - 0960-1295 .- 1469-8072. ; 24:2
-
Tidskriftsartikel (refereegranskat)abstract
- Psi-calculi is a parametric framework for extensions of the pi-calculus; in earlier work we have explored their expressiveness and algebraic theory. In this paper we consider higher-order psi-calculi through a technically surprisingly simple extension of the framework, and show how an arbitrary psi-calculus can be lifted to its higher-order counterpart in a canonical way. We illustrate this with examples and establish an algebraic theory of higher-order psi-calculi. The formal results are obtained by extending our proof repositories in Isabelle/Nominal.
|
|
| 44. |
- Parrow, Joachim
(författare)
-
Interaction Diagrams
- 1993. - 1
-
Rapport (refereegranskat)abstract
- Interaction diagrams are graphic representations of concurrent processes with evolving access capabilities; in particular they illustrate the points of access and relations between them. The basic step of computation is the migration of an access point between processes. This paper explains interaction diagrams through a sequence of examples. Diagrams can be regarded as graphic counterparts of terms in the pi-calculus and illuminate some interesting points on its construction.
|
|
| 45. |
- Parrow, Joachim
(författare)
-
Interaction Diagrams
- 1995
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 2:4, s. 407-443
-
Tidskriftsartikel (refereegranskat)
|
|
| 46. |
- Parrow, Joachim, et al.
(författare)
-
Modal logics for mobile processes
- 1991. - 1
-
Rapport (refereegranskat)abstract
- In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterisation in terms of a simple modal logic (sometimes called Hennessy-Milner logic . This paper first defines two forms of bisimulation equivalence for the\031-calculus , a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterise the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice.
|
|
| 47. |
- Parrow, Joachim, et al.
(författare)
-
Modal Logics for Nominal Transition Systems
- 2015
-
Ingår i: 26th International Conference on Concurrency Theory. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783939897910 ; , s. 198-211
-
Konferensbidrag (refereegranskat)
|
|
| 48. |
- Parrow, Joachim, et al.
(författare)
-
Modal Logics for Nominal Transition Systems
- 2021
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 17:1
-
Tidskriftsartikel (refereegranskat)abstract
- We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.
|
|
| 49. |
- Parrow, Joachim, et al.
(författare)
-
Modal Logics for Nominal Transition Systems
- 2015
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.
|
|
| 50. |
- Parrow, Joachim, et al.
(författare)
-
Multiway Synchronization Verified with Coupled Simulation
- 1992
-
Ingår i: Proceedings of CONCUR '92. - Berlin : Springer. - 3540558225 ; , s. 518-533
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of implementing multiway synchronization in a distributed environment providing only binary asynchronous communication. Our implementation strategy is formulated as a transformation on transition systems and we give a distributed algorithm for multiway synchronization. Correctness assertions and proofs are based on a new method: coupled simulations. The coupled simulation equivalence is weaker than observation equivalence and stronger than testing equivalence and combines some of their advantages. Like observation equivalence (and unlike testing) it is established through case analysis over single transitions. Like testing equivalence (and unlike observation) it allows an internal choice to be distributed onto several internal choices. The latter is particularly important when relating our distributed implementations to their specifications.
|
|
