Logo: to the web site of Uppsala University

uu.sePublications from Uppsala University
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Culling Concurrency Theory: Reusable and trustworthy meta-theory, proof techniques and separation results
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. (Mobility)
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

As concurrent systems become ever more complex and ever more ubiquitous, the need to understand and verify them grows ever larger. For this we need formal modelling languages that are well understood, with rigorously verified foundations and proof techniques, applicable to a wide variety of concurrent systems.

Defining modelling languages is easy; there is a stupefying variety of them in the literature. Verifying their foundations and proof techniques, and developing an understanding of their interrelationship with other modelling languages, is difficult, tedious and error-prone. The contributions of this thesis support these tasks in reusable and trustworthy ways, by results that apply to a wide variety of modelling languages, verified to the highest standards of mathematical rigour in an interactive theorem prover.

To this end, we extend psi-calculi - a family of process calculi with reusable foundations for formal verification - with several new language features. We prove that the bisimulation meta-theory of psi-calculi carries over to these extended settings. This widens the scope of psi-calculi to important application areas, such as cryptography and wireless communication. We develop bisimulation up-to techniques - powerful proof techniques for showing that two processes exhibit the same observable behaviour - that apply to all psi-calculi. By showing how psi-calculi can encode dynamic priorities under very strong quality criteria, we demonstrate that the expressive power is greater than previously thought. Finally, we develop a simple and widely applicable technique for showing that a process calculus adds expressiveness over another, based on little more than whether parallel components may act independently or not. Many separation results, both novel ones and strengthenings of known results from the literature, emerge as special cases of this technique.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2016. , p. 113
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1397
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-297488ISBN: 978-91-554-9639-5 (print)OAI: oai:DiVA.org:uu-297488DiVA, id: diva2:951006
Public defence
2016-09-22, ITC/2446, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Projects
UPMARCAvailable from: 2016-08-26 Created: 2016-06-23 Last updated: 2019-02-25Bibliographically approved
List of papers
1. Broadcast psi-calculi with an application to wireless protocols
Open this publication in new window or tab >>Broadcast psi-calculi with an application to wireless protocols
Show others...
2015 (English)In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 14, no 1, p. 201-216Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2015
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-205258 (URN)10.1007/s10270-013-0375-z (DOI)000349026100012 ()
Projects
UPMARCProFuN
Funder
Swedish Research Council, 2013-4853
Available from: 2013-11-08 Created: 2013-08-15 Last updated: 2024-01-17Bibliographically approved
2. Higher-order psi-calculi
Open this publication in new window or tab >>Higher-order psi-calculi
2014 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 24, no 2, article id e240203Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Cambridge University Press, 2014
Keywords
process calculi, psi calculi, isabelle, theorem proving, nominal, higher-order
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-183610 (URN)10.1017/S0960129513000170 (DOI)000343643500003 ()
Projects
UPMARCProFuN
Funder
Swedish Foundation for Strategic Research
Available from: 2013-06-24 Created: 2012-10-30 Last updated: 2018-01-12Bibliographically approved
3. A Sorted Semantic Framework for Applied Process Calculi
Open this publication in new window or tab >>A Sorted Semantic Framework for Applied Process Calculi
Show others...
2016 (English)In: Logical Methods in Computer Science, E-ISSN 1860-5974, Vol. 12, no 1, p. 1-49, article id 8Article in journal (Refereed) Published
Abstract [en]

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.

Keywords
Expressiveness, Pattern matching, Type systems, Theorem proving, pi-calculus, Nominal sets
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-262199 (URN)10.2168/LMCS-12(1:8)2016 (DOI)000374769600004 ()
Projects
UPMARC
Funder
Swedish Research Council, 2013-4853
Available from: 2016-03-31 Created: 2015-09-09 Last updated: 2024-07-04Bibliographically approved
4. Priorities Without Priorities: Representing Preemption in Psi-Calculi
Open this publication in new window or tab >>Priorities Without Priorities: Representing Preemption in Psi-Calculi
2014 (English)In: Proc. 21st International Workshop on Expressiveness in Concurrency, and 11th Workshop on Structural Operational Semantics, 2014, p. 2-15Conference paper, Published paper (Refereed)
Series
Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180 ; 160
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-297468 (URN)10.4204/EPTCS.160.2 (DOI)
Conference
EXPRESS/SOS 2014, September 1st, Rome, Italy
Available from: 2014-08-07 Created: 2016-06-23 Last updated: 2018-01-10Bibliographically approved
5. Bisimulation up-to techniques for psi-calculi
Open this publication in new window or tab >>Bisimulation up-to techniques for psi-calculi
2016 (English)In: Proc. 5th ACM SIGPLAN Conference on Certified Programs and Proofs / [ed] Avigad, J; Chlipala, A, New York: ACM Press, 2016, p. 142-153Conference paper, Published paper (Refereed)
Abstract [en]

Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi-calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.

Place, publisher, year, edition, pages
New York: ACM Press, 2016
Keywords
Bisimulation up-to, process calculus, psi-calculi, Isabelle, Nominal Isabelle, nominal logic
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-229008 (URN)10.1145/2854065.2854080 (DOI)000389021600016 ()9781450341271 (ISBN)
Conference
CPP 2016, January 18–19, Saint Petersburg, FL
Available from: 2016-01-18 Created: 2014-07-25 Last updated: 2018-01-11Bibliographically approved
6. The Expressive Power of Monotonic Parallel Composition
Open this publication in new window or tab >>The Expressive Power of Monotonic Parallel Composition
2016 (English)In: Programming Languages and Systems, Berlin: Springer, 2016, p. 780-803Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9632
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-297465 (URN)10.1007/978-3-662-49498-1_30 (DOI)000401936100030 ()978-3-662-49497-4 (ISBN)
Conference
ESOP 2016, April 3–7, Eindhoven, The Netherlands
Available from: 2016-03-22 Created: 2016-06-23 Last updated: 2018-01-10Bibliographically approved

Open Access in DiVA

fulltext(764 kB)1185 downloads
File information
File name FULLTEXT01.pdfFile size 764 kBChecksum SHA-512
dd6aab083d70a471d1677a4571a14fa375b796f406b69595e516299221a082e9ada1d5c3e9696d1895513c1ee19479ed78b1c59e7058684630422ebeb6bac97c
Type fulltextMimetype application/pdf

Authority records

Åman Pohjola, Johannes

Search in DiVA

By author/editor
Åman Pohjola, Johannes
By organisation
Computing ScienceDivision of Computing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 1192 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 2520 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf