Verification of probabilistic behaviours

D. Dranidis (Editor), S. Andova, K. Tigka (Editor), T.A.C. Willemse

    Research output: Contribution to conferencePaperAcademicpeer-review

    22 Downloads (Pure)

    Abstract

    We introduce abstraction in a probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviours. Several rules and axioms are identified, allowing us to rewrite processes to less complex processes by removing redundant internal activity. Using these rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. The verifi- cation shows that after abstraction of internal activity, the protocol behaves as a bu er.
    Original languageEnglish
    Pages84-99
    Number of pages16
    Publication statusPublished - 2004
    Event1st South-East European Workshop on Formal Methods: Agile Formal Methods: Practical, Rigorous Methods for a Changing World - Thessaloniki, Greece
    Duration: 20 Nov 200320 Nov 2003

    Workshop

    Workshop1st South-East European Workshop on Formal Methods: Agile Formal Methods: Practical, Rigorous Methods for a Changing World
    Period20/11/0320/11/03
    Other20 November 2003

    Keywords

    • FMT-PA: PROCESS ALGEBRAS

    Fingerprint

    Dive into the research topics of 'Verification of probabilistic behaviours'. Together they form a unique fingerprint.

    Cite this