Verification of probabilistic behaviours

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

    Research output: Contribution to conferencePaperAcademicpeer-review

    26 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 languageUndefined
    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
    • IR-66291
    • EWI-6542

    Cite this