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.
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.
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.
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.
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.
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.
High-level formalisms for concurrency are often defined as extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms. Psi-calculi is a parametric framework that can accommodate a wide spectrum of such calculi. It allows the definition of process calculi that extend the pi-calculus with arbitrary data, logic and logical assertions. All such psi calculi inherit machine-checked proofs of the meta-theory such as compositionality and bisimulation congruence.
We present a generic tool for analysing processes from any psi calculus instance, and for implementing new instances with the help of a supporting library. The tool implements symbolic execution and bisimulation algorithms for both unicast and wireless broadcast communication. We illustrate the tool by examples from pi-calculus and the area of wireless sensor networks.
Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.
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.
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.
An engineering graduate needs to master a number of important skills: problem solving, critical thinking, communication, collaboration, etc. In this paper we describe how a course in computer security, taught in the Computer and Information Engineering programme at Uppsala University, has been developed over a period of three years. The aim is to better develop the engineering competencies of students, improving their understanding of course contents, training their ability to reflect on it, and to apply their knowledge when facing realistic problems.
The course is designed to activate students, based on practical labs and theoretical tasks which are solved in groups. The student reports are assessed at seminars, where the solutions are presented orally, peer-reviewed and discussed. The seminars encourage and reward activities at the higher levels of taxonomies such as Bloom's.
The results of the development, based on a CEQ-based course evaluation, indicate that students take a deeper approach to learning. They develop their problem-solving skills to a high degree, appreciate the practical solving of open-ended problems, and take responsibility for collaborative learning. Their overall satisfaction with the course is quite high, despite indications that they find the workload high.
Students in engineering are well trained in solving specified problems, but some have trouble when given problems where there is more than one solution. In their professional life they are much more often confronted with open-ended problems, where there may be more than one solution, and where there may be many ways to reach each one. The goals may be vague, the problem may be underspecified, and the fresh graduate frustrated by the new situation.
We present a structured approach to training students in open-ended problem solving. We have introduced a half-day workshop to help students learn to work with open-ended, ill-structured problems, using a different approach than they would for the well-structured problems they are used to.
Our results indicate that students have become more creative. Compared to previous years, the students explore more paths towards the goal, and use more elaborate methods. Their approach is similar to that typically used by the best students in previous instances of the course. Students mention creativity and group dynamics as positive aspects of the workshop and the following lab.
We conclude that with proper guidance and training, even weaker students can become more creative when solving open-ended problems.
We propose a coalgebraic model of the Fusion calculus based on HD-automata. The main advantage of the approach is that the partition refinement algorithm designed for HD-automata is easily adapted to handle Fusion calculus processes. Hence, the transition systems of Fusion calculus processes can be minimised according to the notion of observational semantics of the calculus. As a beneficial side effect, this also provides a bisimulation checker for Fusion calculus.
We apply the recently developed techniques of higher order abstract syntax and functorial operational semantics to give a compositional and fully abstract semantics for the π-calculus equipped with open bisimulation. The key novelty in our work is the realisation that the sophistication of open bisimulation requires us to move from the usual semantic domain of presheaves over subcategories of Set to presheaves over subcategories of Rel. This extra structure is crucial in controlling the renaming of extruded names and in providing a variety of different dynamic allocation operators to model the different binders of the π-calculus.
We apply the recently developed techniques of higher order abstract syntax and functorial operational semantics to give a compositional and fully abstract semantics for the π-calculus equipped with open bisimulation. The key novelty in our work is the realisation that the sophistication of open bisimulation requires us to move from the usual semantic domain of presheaves over subcategories of \mathbfSet to presheaves over subcategories of \mathbfRel. This extra structure is crucial in controlling the renaming of extruded names and in providing a variety of different dynamic allocation operators to model the different binders of the π-calculus.
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.
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.
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.
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.
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.
To complement previous research on the top-down inclusion of ethics training within engineering programs, this Innovative Practice Work in Progress paper describes a supplementary strategy acknowledging and supporting ethics training as a shared responsibility. As science and technology have ethical impact, accreditation bodies have in the past decades mandated the inclusion of ethics in STEM education. However, the implementation of ethics education is fraught with obstacles. Through a case study of a Faculty-wide effort to support shared responsibility for ethics training, the pros and cons of an institutionally embedded ethics approach are discussed. It is argued that such an approach can provide a rooted base that can also serve to comply with more formal ethics evaluations, by strengthening a view of ethics as craft, acknowledging subject teachers as ethics ambassadors, reforming the hidden curriculum, and depoliticizing institutional politics.
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.
We present a calculus of mobile processes without prefix or summation, called the solos calculus. Using two different encodings, we show that the solos calculus can express both action prefix and guarded summation. One encoding gives a strong correspondence but uses a match operator; the other yields a slightly weaker correspondence but uses no additional operators. We also show that the expressive power of the solos calculus is still retained by the sub-calculus where actions carry at most two names. On the contrary, expressiveness is lost in the solos calculus without match and with actions carrying at most one name.
We present a calculus of mobile processes without prefix or summation, and using two different encodings we show that it can express both action prefix and guarded summation. One encoding gives a strong correspondence but uses a match operator; the other yields a slightly weaker correspondence but uses no additional operators.
With this note we present a quick overview on the work that has been done to collect (online) resources - an extensive up-to-date bibliography and a web page for further information - covering the area of calculi for mobile processes. Therefore, we quickly recapitulate the history of this area from our point of view, which is witnessed by the number of respective research papers in the field.
We present an expressiveness study of linearity and persistence of processes. We choose the pi-calculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the pi-calculus. Each one singles out a natural source of linearity/persistence also present in other frameworks such as Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing (or proving the non-existence of) encodings among the fragments, a processes-as-formulae interpretation and a reduction from Minsky machines.
We present the fusion calculus as a significant step towards a canonical calculus of concurrency. It simplifies and extends the pi-calculus.
The fusion calculus contains the polyadic pi-calculus as a proper subcalculus and thus inherits all its expressive power. The gain is that fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models such as concurrent constraints formalisms. It is also easy to represent the so called strong reduction strategies in the lambda-calculus, involving reduction under abstraction. In the pi-calculus these tasks require elaborate encodings.
The dramatic main point of this paper is that we achieve these improvements by simplifying the pi-calculus rather than adding features to it. The fusion calculus has only one binding operator where the pi-calculus has two (input and restriction). It has a complete symmetry between input and output actions where the pi-calculus has not. There is only one sensible variety of bisimulation congruence where the pi-calculus has at least three (early, late and open). Proofs about the fusion calculus, for example in complete axiomatizations and full abstraction, therefore are shorter and clearer.
Our results on the fusion calculus in this paper are the following. We give a structured operational semantics in the traditional style. The novelty lies in a new kind of action, fusion actions for emulating updates of a shared state. We prove that the calculus contains the pi-calculus as a subcalculus. We define and motivate the bisimulation equivalence and prove a simple characterization of its induced congruence, which is given two versions of a complete axiomatization for finite terms. The expressive power of the calculus is demonstrated by giving a straight-forward encoding of the strong lazy lambda-calculus, which admits reduction under lambda abstraction.
We present complete axiomatizations of weak hypercongruence in the finite fragment of the fusion calculus, an extension and simplification of the pi-calculus. We treat both the full fusion calculus and the subcalculus without mismatch operators. The axiomatizations are obtained from the laws for hyperequivalence and adding so called tau-laws. These are similar to the well known tau-laws for CCS and the pi-calculus, but there is an interesting difference which highlights an aspect of the higher expressive power of the fusion calculus.
In the update calculus concurrent processes can perform update actions with side effects, and a scoping operator can be used to control the extent of the update. In this way it incorporates fundamental concepts both from imperative languages or concurrent constraints formalisms, and from functional formalisms such as the lambda- and pi-calculi. Structurally it is similar to but simpler than the pi-calculus; it has only one binding operator and a symmetry between input and output. We define the structured operational semantics and the proper bisimulation equivalence and congruence, and give a complete axiomatization. The pi-calculus turns out to be an asymmetric subcalculus.
We propose two strategies to reduce energy consumption for secure data aggregation in wireless sensor networks. While the purpose of data aggregation is to reduce energy consumption, secure data aggregation introduces an overhead making the total energy consumption comparable to naive secure non-aggregation. Another aspect is that the secure data aggregation has higher node congestion than non-aggregation schemes for networks of sizes up to about 100 nodes. Considering a secure data aggregation protocol, our strategies are to reduce the height of the aggregation tree and limit its node degree. The former results in fewer verification messages and a lower total communication load, and the latter reduces node congestion. The most heavily burdened node sends a third of the messages required in the original protocol, which for small networks is lower than with non-aggregation, and the total communication load is lowered compared to non-aggregation.
We extend History Dependent Automata to handle polyadic labels, and using a new symbolic semantics of fusion calculus we give a mapping into these Polyadic HDA with Negative Transitions, and show that the mapping is adequate with respect to hyperequivalence in the fusion calculus. This lays the grounds for HD-automata-based tools applicable not only to the monadic pi-calculus but also to the fusion calculus and polyadic pi-calculus, allowing implementation efforts to be focused at a foundational level rather than being multiplied in several tools.
The fusion calculus is presented as a significant step towards a canonical calculus of concurrency. It simplifies and extends the π-calculus of Milner, Parrow and Walker.
The fusion calculus contains the polyadic π-calculus as a proper subcalculus and thus inherits all its expressive power. In addition fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models with shared state, including concurrent constraint formalisms. It is also easy to represent the so called strong reduction strategies in the Λ-calculus, involving reduction under abstraction. In the π-calculus thesetasks require elaborate encodings.
The fusion calculus simplifies the π-calculus by reducing the number of binding operators and the number of bisimulation equivalences, and by making input and output symmetric like in pure CCS. We attain a calculus where concepts from other models of computation are more easily expressed than in the π-calculus, thereby taking a step towards a unified yet simple model of computation.
In this thesis we present a broad foundational theory of the fusion calculus. We define its labelled and unlabelled operational semantics, and treat strong and weak bisimulation equivalences for both semantics in some detail, including complete axiom systems for finite terms. The equivalences are given symbolic characterisations, leading to algorithms and an automatic tool for equivalence checking. We demonstrate the expressive power of the fusion calculus to give simple encodings of foundational calculi for functional and concurrent constraint programming.
In this paper we describe the first prototype version of the Mobility Workbench (MWB), an automated tool for manipulating and analyzing mobile concurrent systems (those with evolving connectivity structures) described in the pi-calculus. The main feature of this version of the MWB is checking open bisimulation equivalences. We illustrate the MWB with an example automated analysis of a handover protocol for a mobile telephone system.
We use the fusion calculus, a generalization and simplification of the pi-calculus, to model concurrent constraint programming. In particular we encode three basic variants of the rho-calculus, which is a foundational calculus for the concurrent constraint programming language Oz. Using a new reduction-based semantics and weak barbed congruences for the fusion calculus we formally establish an operational correspondence between the rho-calculi and their encodings. These barbed congruences are shown to coincide with the hyperequivalences previously adopted for the fusion calculus.
We present a compositional encoding of the gamma-calculus into the pi-calculus. The former, used in the Oz semantics, is a recent small language with equational constraints over logical variables; the latter is a basic calculus of interacting processes. We establish a close correspondence between the reductions in the gamma-calculus and its encoding, using weak barbed bisimulation congruence.