Process Algebra with Action Dependencies

Arend Rensink, Heike Wehrheim

    Research output: Book/ReportReportProfessional

    17 Downloads (Pure)

    Abstract

    Process algebras are a frequently used tool for the specification and verification of distributed reactive systems. In process algebras, actions are used to denote the basic entities of systems. In general, actions are just abstract names with no particular interpretation. The semantics of a system description, given in form of a process algebra term, is not in uenced by the choice of names. In this paper, we equip a process algebra with a simple semantics for the actions, given in the form of dependencies. The action dependencies are to be interpreted in the Mazurkiewicz sense: independent actions should be able to commute, or (from a different perspective) should be unordered, whereas dependent actions are always ordered. In this approach, the operators are used to describe the conceptual behavioural structure of the system and the action dependencies determine the minimal necessary orderings and thereby the additionally possible parallelism within this structure. In previous work on the semantics of specifications using Mazurkiewicz dependencies, the main interest has been on linear time. We present in this paper a branching time semantics, both operationally and denotationally. For this purpose, we present a process algebra that incorporates, besides some standard operators, also an operator for action refinement. For interpreting the operators in the presence of action dependencies, a new concept of partial termination has to be developed. We show consistency of the operational and denotational semantics; furthermore, we give a axiomatisation of bisimilarity, which is complete for finite terms. Some small examples demonstrate the exibility of this process algebra in the design of distributed reactive systems.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherUniversiteit Twente
    Number of pages59
    Publication statusPublished - Feb 1999

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-99-02
    ISSN (Print)1381-3625

    Fingerprint

    Dive into the research topics of 'Process Algebra with Action Dependencies'. Together they form a unique fingerprint.

    Cite this