Partial-order models for quantitative extensions of LOTOS

    Research output: Contribution to journalArticleAcademicpeer-review

    12 Citations (Scopus)

    Abstract

    Event structures are a prominent model for non-interleaving concurrency. The use of event structures for providing a compositional non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time – both of deterministic and stochastic nature – and probability. The suitability of these models for giving a non-interleaving semantics to a timed, stochastic and probabilistic extension of LOTOS is investigated. Consistency between the event structure semantics and an (event-based) operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail. These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and provide a justification for the event structure semantics. As a running example an infinite buffer is used in which gradually timing constraints on latency and rates of accepting and producing data and the probability of loss of messages are incorporated
    Original languageEnglish
    Pages (from-to)925-950
    Number of pages26
    JournalComputer networks and ISDN systems
    Volume30
    Issue number9-10
    DOIs
    Publication statusPublished - 1998

    Fingerprint

    Specification languages
    Semantics
    Trajectories

    Keywords

    • FMT-NIM: NON-INTERLEAVING MODELS
    • FMT-PA: PROCESS ALGEBRAS
    • FMT-PM: PROBABILISTIC METHODS
    • Deterministic time
    • Event structures
    • Probability
    • Process algebra
    • Semantics
    • Stochastic time
    • True concurrency

    Cite this

    @article{30c2b050b788443c8a6ace699d8aa864,
    title = "Partial-order models for quantitative extensions of LOTOS",
    abstract = "Event structures are a prominent model for non-interleaving concurrency. The use of event structures for providing a compositional non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time – both of deterministic and stochastic nature – and probability. The suitability of these models for giving a non-interleaving semantics to a timed, stochastic and probabilistic extension of LOTOS is investigated. Consistency between the event structure semantics and an (event-based) operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail. These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and provide a justification for the event structure semantics. As a running example an infinite buffer is used in which gradually timing constraints on latency and rates of accepting and producing data and the probability of loss of messages are incorporated",
    keywords = "FMT-NIM: NON-INTERLEAVING MODELS, FMT-PA: PROCESS ALGEBRAS, FMT-PM: PROBABILISTIC METHODS, Deterministic time, Event structures, Probability, Process algebra, Semantics, Stochastic time, True concurrency",
    author = "Ed Brinksma and Joost-Pieter Katoen and Rom Langerak and Diego Latella",
    year = "1998",
    doi = "10.1016/S0169-7552(97)00134-7",
    language = "English",
    volume = "30",
    pages = "925--950",
    journal = "Computer networks",
    issn = "1389-1286",
    publisher = "Elsevier",
    number = "9-10",

    }

    Partial-order models for quantitative extensions of LOTOS. / Brinksma, Ed; Katoen, Joost-Pieter; Langerak, Rom; Latella, Diego.

    In: Computer networks and ISDN systems, Vol. 30, No. 9-10, 1998, p. 925-950.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Partial-order models for quantitative extensions of LOTOS

    AU - Brinksma, Ed

    AU - Katoen, Joost-Pieter

    AU - Langerak, Rom

    AU - Latella, Diego

    PY - 1998

    Y1 - 1998

    N2 - Event structures are a prominent model for non-interleaving concurrency. The use of event structures for providing a compositional non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time – both of deterministic and stochastic nature – and probability. The suitability of these models for giving a non-interleaving semantics to a timed, stochastic and probabilistic extension of LOTOS is investigated. Consistency between the event structure semantics and an (event-based) operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail. These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and provide a justification for the event structure semantics. As a running example an infinite buffer is used in which gradually timing constraints on latency and rates of accepting and producing data and the probability of loss of messages are incorporated

    AB - Event structures are a prominent model for non-interleaving concurrency. The use of event structures for providing a compositional non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time – both of deterministic and stochastic nature – and probability. The suitability of these models for giving a non-interleaving semantics to a timed, stochastic and probabilistic extension of LOTOS is investigated. Consistency between the event structure semantics and an (event-based) operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail. These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and provide a justification for the event structure semantics. As a running example an infinite buffer is used in which gradually timing constraints on latency and rates of accepting and producing data and the probability of loss of messages are incorporated

    KW - FMT-NIM: NON-INTERLEAVING MODELS

    KW - FMT-PA: PROCESS ALGEBRAS

    KW - FMT-PM: PROBABILISTIC METHODS

    KW - Deterministic time

    KW - Event structures

    KW - Probability

    KW - Process algebra

    KW - Semantics

    KW - Stochastic time

    KW - True concurrency

    U2 - 10.1016/S0169-7552(97)00134-7

    DO - 10.1016/S0169-7552(97)00134-7

    M3 - Article

    VL - 30

    SP - 925

    EP - 950

    JO - Computer networks

    JF - Computer networks

    SN - 1389-1286

    IS - 9-10

    ER -