uu.seUppsala University Publications
Change search
Refine search result
1 - 44 of 44
CiteExportLink to result list
Permanent 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
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1. Aceto, Luca
    et al.
    Longo, GiuseppeVictor, BjörnUppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    The difference between concurrent and sequential computation2003Collection (editor) (Other (popular science, discussion, etc.))
  • 2. Aceto, Luca
    et al.
    Victor, BjörnUppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    EXPRESS'00: 7th International Workshop on Expressiveness in Concurrency2000Conference proceedings (editor) (Other academic)
  • 3.
    Baldamus, Michael
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A Fully Abstract Encoding of the pi-Calculus with Data Terms2005In: Proceedings of ICALP 2005 / [ed] Luís Caires; Guiseppe F. Italiano; Luís Monteiro; Catuscia Palamidessi; Moti Yung, Berlin: Springer , 2005, p. 1202-1213Conference paper (Refereed)
    Abstract [en]

    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.

  • 4.
    Baldamus, Michael
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Spi Calculus Translated to pi-Calculus Preserving May-Testing2003Report (Other academic)
    Abstract [en]

    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.

  • 5.
    Baldamus, Michael
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Spi Calculus Translated to pi-Calculus Preserving May-Tests2004In: Proceedings of LICS 2004: Logic in Computer Science, Los Alamitos, Calif: IEEE Computer Society, 2004, p. 22-31Conference paper (Refereed)
    Abstract [en]

    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.

  • 6.
    Bengtson, Jesper
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Johansson, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Psi-calculi: a framework for mobile processes with nominal data and logic2011In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 7, no 1, p. 11-Article in journal (Refereed)
    Abstract [en]

    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.

  • 7.
    Bengtson, Jesper
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Johansson, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Psi-calculi: Mobile processes, nominal data, and logic2009In: Proc. 24th Annual IEEE Symposium on Logic in Computer Science, Piscataway, NJ: IEEE , 2009, p. 39-48Conference paper (Refereed)
    Abstract [en]

    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.

  • 8.
    Borgström, Johannes
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Gutkovas, Ramunas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Åman Pohjola, Johannes
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A Sorted Semantic Framework for Applied Process Calculi2016In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 12, no 1, p. 1-49, article id 8Article in journal (Refereed)
    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.

  • 9.
    Borgström, Johannes
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Gutkovas, Ramunas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Åman Pohjola, Johannes
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A Sorted Semantic Framework for Applied Process Calculi (extended abstract)2014In: Trustworthy Global Computing: TGC 2013, Springer Berlin/Heidelberg, 2014, p. 103-118Conference paper (Refereed)
    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 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.

  • 10.
    Borgström, Johannes
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Gutkovas, Ramunas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Rodhe, Ioana
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A Parametric Tool for Applied Process Calculi2013In: 13th International Conference on Application of Concurrency to System Design (ACSD 2013), IEEE Computer Society, 2013, p. 180-185Conference paper (Refereed)
    Abstract [en]

    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.

  • 11.
    Borgström, Johannes
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Gutkovas, Ramunas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Rodhe, Ioana
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    The Psi-Calculi Workbench: A Generic Tool for Applied Process Calculi2015In: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 14, no 1, article id 9Article in journal (Refereed)
    Abstract [en]

    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.

  • 12.
    Borgström, Johannes
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Huang, Shuqin
    Johansson, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Raabjerg, Palle
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Åman Pohjola, Johannes
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Broadcast psi-calculi with an application to wireless protocols2015In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 14, no 1, p. 201-216Article in journal (Refereed)
    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.

  • 13.
    Borgström, Johannes
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Huang, Shuqin
    Peking University, China.
    Johansson, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Raabjerg, Palle
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Åman Pohjola, Johannes
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Broadcast Psi-calculi with an Application to Wireless Protocols2011In: Software Engineering and Formal Methods: SEFM 2011, Springer Berlin/Heidelberg, 2011, p. 74-89Conference paper (Refereed)
    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 % 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.

  • 14.
    Cajander, Åsa
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computerized Image Analysis and Human-Computer Interaction.
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bernáld, Helena
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Professionella kompetenser i projektkurser2012In: Proc. 3:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar / [ed] Gunnarsson, Svante, Linköping University Electronic Press, 2012, p. 123-128Conference paper (Refereed)
  • 15.
    Cambazoglu, Volkan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Gutkovas, Ramunas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Åman Pohjola, Johannes
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support2015Report (Other academic)
  • 16.
    Cambazoglu, Volkan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Rohner, Christian
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    The impact of trace and adversary models on location privacy provided by K-anonymity2012In: Proc. 1st Workshop on Measurement, Privacy, and Mobility, New York: ACM Press, 2012, article id 6Conference paper (Refereed)
  • 17.
    Cassel, Sofia
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Nylén, Aletta
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Enhanced learning by promoting engineering competencies2014In: Proc. 44th ASEE/IEEE Frontiers in Education Conference, Piscataway, NJ: IEEE Press, 2014, p. 2044-2049Conference paper (Refereed)
    Abstract [en]

    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.

  • 18.
    Cassel, Sofia
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A structured approach to training open-ended problem solving2015In: Proc. 45th ASEE/IEEE Frontiers in Education Conference, Piscataway, NJ: IEEE Press, 2015, p. 417-420Conference paper (Refereed)
    Abstract [en]

    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.

  • 19.
    Cassel, Sofia
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Fördjupat lärande genom aktiverande examination2013In: 4:e Utvecklingskonferensen för Sveriges ingenjörsutbildningar, 2013, p. 51-54Conference paper (Refereed)
  • 20. Castellani, Ilaria
    et al.
    Victor, BjörnUppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    EXPRESS'99: 6th International Workshop on Expressiveness in Concurrency1999Conference proceedings (editor) (Other academic)
  • 21. Ferrari, Gianluigi
    et al.
    Montanari, Ugo
    Tuosto, Emilio
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Yemane, Kidane
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Modelling and Minimising the Fusion Calculus using HD-automata2005In: Proceedings of CALCO 2005, 2005Conference paper (Refereed)
    Abstract [en]

    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.

  • 22. Ferrari, Gianluigi
    et al.
    Montanari, Ugo
    Tuosto, Emilio
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Yemane, Kidane
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Modelling Fusion Calculus using HD-Automata2005Report (Other academic)
    Abstract [en]

    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.

  • 23. Ghani, Neil
    et al.
    Yemane, Kidane
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Relationally Staged Computations in Calculi of Mobile Processes2004In: Proc. 7th Workshop on Coalgebraic Methods in Computer Science / [ed] J. Adámek, S. Milius, Elsevier , 2004, p. 105-120Conference paper (Refereed)
    Abstract [en]

    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.

  • 24.
    Johansson, Magnus
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Bengtson, Jesper
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Weak Equivalences in Psi-calculi2010In: Proc. 25th Symposium on Logic in Computer Science: LICS 2010, Piscataway, NJ: IEEE , 2010, p. 322-331Conference paper (Refereed)
    Abstract [en]

    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.

  • 25.
    Johansson, Magnus
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Bengtson, Jesper
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Extended pi-Calculi2008In: Automata, Languages and Programming, PT 2: Proceedings of ICALP 2008 / [ed] Aceto L, Damgard I, Goldberg LA, Halldorsson MM, Ingolfsdottir A, Walukiewicz I, 2008, p. 87-98Conference paper (Refereed)
    Abstract [en]

    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
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    A Fully Abstract Symbolic Semantics for Psi-Calculi2010In: Proc. 6th Workshop on Structural Operational Semantics: SOS 2009, 2010, p. 17-31Conference paper (Refereed)
    Abstract [en]

    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.

  • 27.
    Johansson, Magnus
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Computing Strong and Weak Bisimulations for Psi-Calculi2012In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 81, no 3, p. 162-180Article in journal (Refereed)
    Abstract [en]

    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.

  • 28. Laneve, Cosimo
    et al.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Solo diagrams2001In: Proceedings of TACS 2001, 2001, p. 127-144Conference paper (Refereed)
    Abstract [en]

    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.

  • 29. Laneve, Cosimo
    et al.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Solos in Concert2003In: Mathematical Structures in Computer Science, ISSN 0960-1295, Vol. 13, no 5, p. 657-683Article in journal (Refereed)
    Abstract [en]

    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.

  • 30. Laneve, Cosimo
    et al.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Solos in Concert1999In: Proceedings of ICALP'99, 1999Conference paper (Refereed)
    Abstract [en]

    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.

  • 31. Nestmann, Uwe
    et al.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Calculi for Mobile Processes: Bibliography and Web Pages1998In: Bulletin of the EATCS, Vol. 64Article, review/survey (Other (popular science, discussion, etc.))
    Abstract [en]

    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.

  • 32. Nestmann, Uwe
    et al.
    Victor, BjörnUppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Special issue on the pi-calculus2004Collection (editor) (Other academic)
  • 33. Palamidessi, Catuscia
    et al.
    Saraswat, Vijay
    Valencia, Frank D.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus2006In: Proc. 21st Symposium on Logic In Computer Science: LICS 2006, Piscataway, NJ: IEEE , 2006, p. 59-68Conference paper (Refereed)
    Abstract [en]

    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.

  • 34.
    Parrow, Joachim
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes1998In: Proceedings of LICS'98, Los Alamitos, CA: IEEE Computer Society, 1998, p. 176-185Conference paper (Refereed)
    Abstract [en]

    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.

  • 35.
    Parrow, Joachim
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    The Tau-Laws of Fusion1998In: Proceedings of CONCUR'98 / [ed] Davide Sangiorgi, Robert de Simone, Berlin: Springer, 1998, p. 99-114Conference paper (Refereed)
    Abstract [en]

    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.

  • 36.
    Parrow, Joachim
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    The Update Calculus1997In: Proceedings of AMAST'97 / [ed] Michael Johnson, Berlin: Springer , 1997, p. 409-423Conference paper (Refereed)
    Abstract [en]

    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.

  • 37.
    Pålsson, Stefan
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computational Science.
    Victor, BjörnUppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Proceedings från 5:e utvecklingskonferensen för Sveriges ingenjörsutbildningar2016Conference proceedings (editor) (Other academic)
  • 38. Sutic, Davor
    et al.
    Rodhe, Ioana
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Rohner, Christian
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Lower trees with fixed degrees: a recipe for efficient secure hierarchical aggregation in WSNs2011In: 2011 IEEE WIRELESS COMMUNICATIONS AND NETWORKING CONFERENCE (WCNC), IEEE Computer Society, 2011, p. 659-664Conference paper (Refereed)
    Abstract [en]

    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.

  • 39. Tuosto, Emilio
    et al.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Yemane, Kidane
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. COMPUTER SYSTEMS.
    Polyadic History-Dependent Automata for the Fusion Calculus2003Report (Other academic)
    Abstract [en]

    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.

  • 40.
    Victor, Björn
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes1998Doctoral thesis, monograph (Other academic)
    Abstract [en]

    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.

  • 41.
    Victor, Björn
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Moller, Faron
    The Mobility Workbench: A Tool for the Pi-Calculus1994In: Proceedings of CAV'94, 1994, p. 428-440Conference paper (Refereed)
    Abstract [en]

    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.

  • 42.
    Victor, Björn
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Concurrent Constraints in the Fusion Calculus1998In: Proceedings of ICALP'98 / [ed] Kim G. Larsen, Sven Skyum, Glynn Winskel, Berlin: Springer, 1998, p. 455-469Conference paper (Refereed)
    Abstract [en]

    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.

  • 43.
    Victor, Björn
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Parrow, Joachim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Constraints as Processes1996In: Proceedings of CONCUR'96 / [ed] Ugo Montanari, Vladimiro Sassone, Berlin: Springer , 1996, p. 389-405Conference paper (Refereed)
    Abstract [en]

    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.

  • 44.
    Victor, Björn
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Yi, WangUppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Proceedings of the 11th Nordic Workshop on Programming Theory1999Conference proceedings (editor) (Other academic)
1 - 44 of 44
CiteExportLink to result list
Permanent 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