uu.seUppsala University Publications
Change search
Refine search result
1 - 38 of 38
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.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Annichini, A
    Bouajjani, A
    Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol1999In: Tools and Algorithms for the Construction and Analysis of Systems: Proceddings of TACAS'99 / [ed] W. Rance Cleaveland, 1999, Vol. 1579, p. 208-222Conference paper (Refereed)
    Abstract [en]

    We consider the problem of verifying automatically infinite- state systems that are systems of finite machines that communicate by exchanging messages through unbounded lossy fifo channels. In a previous work [1], we proposed an algorithmic approach based on constructing a symbolic representation of the set of reachable configurations of a system by means of a class of regular expressions (SREs). The construction of such a representation consists of an iterative computation with an acceleration technique which enhances the chance of convergence. This technique is based on the analysis of the effect of iterating control loops. In the work we present here, we experiment our approach and show how it can be effectively applied. For that, we developed a tool prototype based on the results in [1]. Using this tool, we provide an automatic verification of (the parameterized version of) the Bounded Retransmission Protocol.

  • 2.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Bouajjani, A
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    On-the-fly analysis of systems with unbounded, lossy FIFO channels1998In: Computer Aided Verification: Proceedings of 10th International Conference, CAV'98 / [ed] Alan J. Hu, Moshe Y. Vardi, 1998, Vol. 1427, p. 305-318Conference paper (Refereed)
    Abstract [en]

    We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.

  • 3.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Cerans, K
    Simulation is decidable for one-counter nets1998In: CONCUR'98 Concurrency Theory: Proceedings of the 9th International Conference, 1998, Vol. 1466, p. 253-268Conference paper (Refereed)
    Abstract [en]

    We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of simulation preorder between pairs of processes in a class whose elements are neither finite-state nor allow finite partitioning of their state spaces.

  • 4.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Undecidable verification problems for programs with unreliable channels1996In: Automata, Languages and Programming: Proceedings of ICALP 94 / [ed] Serge Abiteboul, Eli Shamir, 1996, Vol. 130, no 1, p. 71-90Conference paper (Refereed)
    Abstract [en]

    We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namely

    • The model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).

    • The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.

    The results are obtained through a reduction from a variant of Post's Correspondence Problem.

  • 5.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Verifying networks of timed processes1998In: Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 4th International Conference, TACAS'98 / [ed] Bernhard Steffen, 1998, Vol. 1384, p. 298-312Conference paper (Refereed)
    Abstract [en]

    Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz. real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.

  • 6.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Kindahl, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Peled, D
    A general approach to partial order reductions in symbolic verification1998In: Computer Aided Verification: Proceedings of CAV'98 / [ed] Alan J. Hu, Moshe Y. Vardi, 1998, Vol. 1427, p. 379-390Conference paper (Refereed)
    Abstract [en]

    The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.

    We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.

  • 7.
    Ahlgren, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems. Swedish Institute of Computer Science.
    Improving Computer Communication Performance by Reducing Memory Bandwidth Consumption1997Doctoral thesis, comprehensive summary (Other academic)
  • 8.
    Berglund, Anders
    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, Computer Systems.
    Daniels, Mats
    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, Computer Systems.
    Improving education quality: a full scale study1997In: ACM SIGCSE Bulletin, ISSN 0097-8418, Vol. 29, no 1, p. 330-334Article in journal (Refereed)
  • 9.
    Björnfot, Lars
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Specification and Implementation of Distributed Real-Time Systems for Embedded Applications1996Doctoral thesis, comprehensive summary (Other academic)
  • 10. Cleaveland, Rance
    et al.
    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.
    Steffen, Bernhard
    The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems1993In: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 15, no 1, p. 36-72Article in journal (Refereed)
  • 11.
    Daniels, Mats
    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, Computer Systems.
    Asyl/EFSM: a language for specification of protocols and computers1985Licentiate thesis, comprehensive summary (Other academic)
  • 12.
    Gällmo, Olle
    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, Computer Systems.
    Learning issues in artificial neural networks for ATM traffic control1995Licentiate thesis, comprehensive summary (Other academic)
  • 13.
    Jonsson, Bengt
    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, Computer Systems.
    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.
    Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs1993In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 107, no 2, p. 272-302Article in journal (Refereed)
  • 14.
    Kindahl, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Verification of Infinite-State Systems: Decision Problems and Efficient Algorithms1999Doctoral thesis, monograph (Other academic)
    Abstract [en]

    This thesis presents methods for the verification of distributed systems with infinite state spaces. We consider several verification problems for lossy channel systems, a class of infinite-state systems consisting of finite-state machines that communicate over unbounded, but lossy, FIFO channels. We also combine partial order techniques with symbolic techniques to improve performance of verification algorithms for infinite state systems.

    We study several implementation relations between lossy channel systems and finite transition systems, and show decidability of the following problems: trace inclusion, trace equivalence, simulation preorder, bisimulation equivalence, weak bisimulation equivalence in both directions, and weak simulation preorder in one direction. We further show that weak simulation preorder in the other direction is undecidable.

    Partial order reduction techniques are utilised to avoid exploring multiple interleavings of independent transitions. Constraint systems are introduced as a symbolic technique to represent (possibly infinite) sets of states. We present general methods for the application of partial order techniques for the verification of constraint systems. The method described is used for checking safety properties using forward or backward reachability analysis. It is based on the use of a—not necessarily symmetric—commutativity relation between operations. In contrast with previously existing approaches to partial order verification, which are based on a symmetric relation on transitions, our method does not require the relation to be symmetric. Partial order verification methods for lossy channel systems and for unsafe (i.e., infinite-state) Petri nets are developed to demonstrate the applicability of this approach.

  • 15. Larsen, Kim Guldstrand
    et al.
    Pettersson, Paul
    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, Computer Systems.
    Yi, Wang
    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, Computer Systems.
    UPPAAL in a nutshell1997In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1385-4879, E-ISSN 1571-8115, Vol. 1, no 1-2, p. 134-152Article in journal (Refereed)
  • 16. Milner, Robin
    et al.
    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.
    Walker, David
    A Calculus of Mobile Processes - Part I1992In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 100, no 1, p. 1-40Article in journal (Refereed)
  • 17. Milner, Robin
    et al.
    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.
    Walker, David
    A Calculus of Mobile Processes - Part II1992In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 100, no 1, p. 41-77Article in journal (Refereed)
  • 18. Milner, Robin
    et al.
    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.
    Walker, David
    Modal Logics for Mobile Processes1993In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 114, no 1, p. 149-171Article in journal (Refereed)
    Abstract [en]

    In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterization in terms of a simple modal logic (sometimes called Hennessy-Milner logic). This paper first defines two forms of bisimulation equivalence for the π-calculus, a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterize the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice. The results are applicable to most value-passing process algebras.

  • 19. 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.

  • 20.
    Nordström, Ernst
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Markov Decision Problems in ATM Traffic Control1998Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This thesis discusses how to make cost-effective use of the communication resources in the Broadband Integrated Services Digital Network (B-ISDN), which is based on the Asynchronous Transfer Mode (ATM) switching and multiplexing technique.

    The thesis deals with two important functions in ATM traffic control, namely Call Admission Control (CAC) and routing, which affects both the network operator's revenue over time and the users' Quality of Service (QOS) and Grade of Service (GOS). The routing function finds a route, expressed in terms of successive links, with sufficient QOS (e.g. cell loss probability) according to the CACQOS function. The CACGOS function accepts or rejects the call request based on fairness (e.g. call blocking probability) and revenue considerations.

    The CACGOS and routing tasks are modelled a Semi-Markov Decision Problem (SMDP). The SMDP solution gives high resource utilization and ability to control GOS distribution between the call classes. In SMDP routing, the task is to control the state transitions between reward generating states such that the average reward rate is maximized. In order to obtain a solution with feasible computational complexity, the network SMDP is decomposed into a set of link SMDPs. Each link SMDP is solved by either dynamic programming (DP) or reinforcement learning (RL). DP is based on a model of the decision task in terms of the state transition probabilities and expected reward in each state. RL is not based on a model of the decision task. Instead, the optimal policy is found from simulated state transitions, where long-term reward predictions are corrected by temporal difference learning.

    We study aspects such as delayed set up of wide-band calls, link-level integration of guaranteed QOS services and best effort services, and Poisson versus self-similar call arrival processes.

  • 21. Orava, Fredrik
    et al.
    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.
    An Algebraic Verification of a Mobile Network1992In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 4, no 6, p. 497-543Article in journal (Refereed)
  • 22.
    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.
    Interaction Diagrams1995In: Nordic Journal of Computing, ISSN 1236-6064, Vol. 2, no 4, p. 407-443Article in journal (Refereed)
  • 23.
    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.
    Programmeraren som Schaman1998In: Forskning och Framsteg, ISSN 0015-7937, no 2, p. 14-19Article in journal (Other (popular science, discussion, etc.))
  • 24.
    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.
    Structural and Behavioural Equivalences of Networks1993In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 107, no 1, p. 58-90Article in journal (Refereed)
  • 25.
    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.
    Submodule Construction as Equation Solving in CCS1989In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 68, no 2, p. 175-202Article in journal (Refereed)
  • 26.
    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.
    The Expressive Power of Parallelism1990In: Future generations computer systems, ISSN 0167-739X, E-ISSN 1872-7115, Vol. 6, no 3, p. 271-285Article in journal (Refereed)
  • 27.
    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.
    Sangiorgi, Davide
    Algebraic Theories of Name-Passing Calculi1995In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 120, no 2, p. 174-197Article in journal (Refereed)
  • 28.
    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.
    Sjödin, Peter
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Designing a Multiway Synchronisation Protocol1996In: Computer Communications, ISSN 0140-3664, E-ISSN 1873-703X, Vol. 19, no 14, p. 1151-1160Article in journal (Refereed)
  • 29.
    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.
    Sjödin, Peter
    Multiway Synchronization Verified with Coupled Simulation1992In: Proceedings of CONCUR '92 / [ed] W.R. Cleaveland, Berlin: Springer , 1992, p. 518-533Conference paper (Refereed)
    Abstract [en]

    We consider the problem of implementing multiway synchronization in a distributed environment providing only binary asynchronous communication. Our implementation strategy is formulated as a transformation on transition systems and we give a distributed algorithm for multiway synchronization. Correctness assertions and proofs are based on a new method: coupled simulations. The coupled simulation equivalence is weaker than observation equivalence and stronger than testing equivalence and combines some of their advantages. Like observation equivalence (and unlike testing) it is established through case analysis over single transitions. Like testing equivalence (and unlike observation) it allows an internal choice to be distributed onto several internal choices. The latter is particularly important when relating our distributed implementations to their specifications.

  • 30.
    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.
    Sjödin, Peter
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    The Complete Axiomatization of Cs-Congruence1994In: Proceedings of STACS 94 / [ed] Patrice Enjalbert, Ernst W. Mayr, Klaus W. Wagner, Berlin: Springer , 1994, p. 557-568Conference paper (Refereed)
    Abstract [en]

    The coupled simulation equivalence is slightly larger than observation equivalence. Where observation equivalence is based on weak bisimulations, coupled simulation equivalence is based on pairs of simulations which coincide at stable states. We establish the corresponding congruence and provide a complete axiomatization by adding a new -law, .(. P + Q) = . P + Q, to the axiomatization of observation congruence. We further indicate how the definition of the equivalence can be extended to divergent transition systems.

  • 31.
    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.

  • 32.
    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.

  • 33.
    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.

  • 34.
    Pettersson, Paul
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
    Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice1999Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    During the last decade, model-checking techniques for the verification of timed system have been developed baaed on the theory of timed automata. The practical limitation in applying these techniques to industrial-size systems is the huge amount of time and memory needed to explore and store the state-space of the system model.

    In this thesis, we improve the current status of model-checking techniques for timed systems by developing symbolic, on-the-fly and compositional verification techniques for timed automata. A common characteristics of the model-checking techniques presented is that they use efficient constraint-solving techniques to symbolically represent and manipulate the state-space. To avoid construction of the full state-space of the system model two techniques are used: on-the-fly generation of the state-space and a compositional model-checking technique. The memory-usage is further reduced by developing a minimal and canonical data structure for the class of constraints used in the model-checking algorithm, which reduces the size of each individual state. Two other techniques to reduce the total number of states explored and stored during verification are also presented.

    The developed techniques have been implemented in the verification tool UPPAAL. To demonstrate the potential applications of our model-checking techniques, we present three industrial-size case studies where the UPPAAL tool is applied.

  • 35.
    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.

  • 36.
    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.

  • 37.
    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.

  • 38.
    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.

1 - 38 of 38
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