| 1. |
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
- 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.
|
|
| 6. |
- 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.
|
|
| 7. |
- 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.
|
|
| 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. |
- Bjerg, Anders, et al.
(författare)
-
Shorter time to clinical decision in work-related asthma using a digital tool
- 2020
-
Ingår i: ERJ open research. - Lausanne, Switzerland : European Respiratory Society (ERS). - 2312-0541. ; 6:3
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- PEF curves are a useful but cumbersome tool in diagnosing work-related asthma. Using a digital spirometer and smartphone app, time to clinical decision could be shortened by 6-7 weeks. Physician's time spent analysing PEF data is also shortened.
|
|
