| 1. |
- 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 .- 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.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
- 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.
|
|
| 5. |
- 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.
|
|
| 6. |
- Åman Pohjola, Johannes, et al.
(författare)
-
Negative premises in applied process calculi
- 2013
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We explore two applications of negative premises to increase the expressive power of psi-calculi: reliable broadcasts and priorities. Together, these can be used to model discrete time, which we illustrate with an example from automotive applications. The negative premises can be encoded by a two-level structural operational semantics without negative premises; we use this fact to prove the standard congruence and structural laws of bisimulation with Nominal Isabelle.
|
|
| 7. |
- Andersson, Erik, et al.
(författare)
-
A context-sensitive systems approach for understanding and enabling ecosystem service realization in cities
- 2021
-
Ingår i: Ecology & Society. - : Resilience Alliance, Inc.. - 1708-3087. ; 26:2
-
Tidskriftsartikel (refereegranskat)abstract
- Understanding opportunities as well as constraints for people to benefit from and take care of urban nature is an important step toward more sustainable cities. In order to explore, engage, and enable strategies to improve urban quality of life, we combine a social-ecological-technological systems framework with a flexible methodological approach to urban studies. The framework focuses on context dependencies in the flow and distribution of ecosystem service benefits within cities. The shared conceptual system framework supports a clear positioning of individual cases and integration of multiple methods, while still allowing for flexibility for aligning with local circumstances and ensuring context-relevant knowledge. To illustrate this framework, we draw on insights from a set of exploratory case studies used to develop and test how the framework could guide research design and synthesis across multiple heterogeneous cases. Relying on transdisciplinary multi- and mixed methods research designs, our approach seeks to both enable within-case analyses and support and gradually build a cumulative understanding across cases and city contexts. Finally, we conclude by discussing key questions about green and blue infrastructure and its contributions to urban quality of life that the approach can help address, as well as remaining knowledge gaps both in our understanding of urban systems and of the methodological approaches we use to fill these gaps.
|
|
| 8. |
- Andersson, Erik, et al.
(författare)
-
Enabling Green and Blue Infrastructure to Improve Contributions to Human Well-Being and Equity in Urban Systems
- 2019
-
Ingår i: BioScience. - : Oxford University Press (OUP). - 0006-3568 .- 1525-3244. ; 69:7, s. 566-574
-
Tidskriftsartikel (refereegranskat)abstract
- The circumstances under which different ecosystem service benefits can be realized differ. The benefits tend to be coproduced and to be enabled by multiple interacting social, ecological, and technological factors, which is particularly evident in cities. As many cities are undergoing rapid change, these factors need to be better understood and accounted for, especially for those most in need of benefits. We propose a framework of three systemic filters that affect the flow of ecosystem service benefits: the interactions among green, blue, and built infrastructures; the regulatory power and governance of institutions; and people's individual and shared perceptions and values. We argue that more fully connecting green and blue infrastructure to its urban systems context and highlighting dynamic interactions among the three filters are key to understanding how and why ecosystem services have variable distribution, continuing inequities in who benefits, and the long-term resilience of the flows of benefits.
|
|
| 9. |
- Andersson, Erik, et al.
(författare)
-
Urban resilience thinking in practice : ensuring flows of benefit from green and blue infrastructure
- 2021
-
Ingår i: Ecology & Society. - : Resilience Alliance, Inc.. - 1708-3087. ; 26:4
-
Tidskriftsartikel (refereegranskat)abstract
- Present and future urbanization together with climate change and other uncertainties make urban quality of life a criticalissue, and one that will need constant attention and deliberation. Across cities and contexts, urban ecosystems in the form of greenand blue infrastructure, have the potential to contribute to human well-being as well as supporting biodiversity, and to do so underdiverse conditions. However, the realization of this potential depends not only on the green and blue infrastructure itself, the well-beingbenefits are outcomes of the structures and processes of the entire urban system. Drawing on theory and insights from social-ecologicaltechnological systems (SETS) research and resilience assessments, we describe how a systemic understanding of the generation anddelivery of green and blue infrastructure benefits may inform cross-sectoral strategies and interventions for building resilience aroundthis particular aspect of human well-being. Connecting SETS to non-academic discourse and practice, we describe the urban systemin terms of three systemic controlling variables: infrastructure, institutions, and the perceptions of individual beneficiaries, which wecall filters, and how these can be used in different participatory processes to assess and build resilience around green and blueinfrastructure and its benefits.To ground the conceptual and theoretical framework in real world complexity and make it operational in practice we discuss three casestudies applying the framework in Barcelona, Halle, and Stockholm. All cases share the same general three-step process but theirindividual combinations of methods and adaptions of the filters framework are designed to fit with three necessarily unique collaborative,transdisciplinary processes. The cases are discussed in terms of outcomes and output, the ways they made use of the conceptualframework, and the challenges they faced. This exploratory work points to a new way of engaging with urban resilience—the strengthof the approach is that it is not limited to the identification of specific interventions or policy options, nor trying to prevent change;rather it focuses on how to move with change and build resilience through constant balancing of different types of SETS change. Ourstudy reinforces the growing understanding of how well-being benefits positioned as emergent outcomes of internal SETS interactionsoffers leverage for mainstreaming green and blue infrastructure throughout diverse governance processes and sectors.
|
|
| 10. |
- Andersson, Erik, et al.
(författare)
-
Urban resilience thinking in practice: ensuring flows of benefit from green and blue infrastructure
- 2021
-
Ingår i: Ecology & Society. - : Resilience Alliance, Inc.. - 1708-3087. ; 26:4
-
Tidskriftsartikel (refereegranskat)abstract
- Present and future urbanization together with climate change and other uncertainties make urban quality of life a critical issue, and one that will need constant attention and deliberation. Across cities and contexts, urban ecosystems in the form of green and blue infrastructure, have the potential to contribute to human well-being as well as supporting biodiversity, and to do so under diverse conditions. However, the realization of this potential depends not only on the green and blue infrastructure itself, the well-being benefits are outcomes of the structures and processes of the entire urban system. Drawing on theory and insights from social-ecological-technological systems (SETS) research and resilience assessments, we describe how a systemic understanding of the generation and delivery of green and blue infrastructure benefits may inform cross-sectoral strategies and interventions for building resilience around this particular aspect of human well-being. Connecting SETS to non-academic discourse and practice, we describe the urban system in terms of three systemic controlling variables: infrastructure, institutions, and the perceptions of individual beneficiaries, which we call filters, and how these can be used in different participatory processes to assess and build resilience around green and blue infrastructure and its benefits.To ground the conceptual and theoretical framework in real world complexity and make it operational in practice we discuss three case studies applying the framework in Barcelona, Halle, and Stockholm. All cases share the same general three-step process but their individual combinations of methods and adaptions of the filters framework are designed to fit with three necessarily unique collaborative, transdisciplinary processes. The cases are discussed in terms of outcomes and output, the ways they made use of the conceptual framework, and the challenges they faced. This exploratory work points to a new way of engaging with urban resilience—the strength of the approach is that it is not limited to the identification of specific interventions or policy options, nor trying to prevent change; rather it focuses on how to move with change and build resilience through constant balancing of different types of SETS change. Our study reinforces the growing understanding of how well-being benefits positioned as emergent outcomes of internal SETS interactions offers leverage for mainstreaming green and blue infrastructure throughout diverse governance processes and sectors.
|
|
