Verification of random behaviours

S. Andova, T.A.C. Willemse

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    12 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 verification shows that after abstraction of internal activity, the protocol behaves as a buffer.
    Original languageEnglish
    Title of host publicationSEEFM 200: First south-east europian workshop on formal methods
    EditorsY. Manolopoulos, P. Spirakis
    Place of PublicationThessaloniki, Greece
    PublisherAristotle University of Thessaloniki
    Pages84-99
    Number of pages16
    Publication statusPublished - 20 Nov 2003
    Event1st South-East Europian Workshop on Formal Methods, SEEFM 2003 - Thessaloniki, Greece
    Duration: 20 Nov 200320 Nov 2003
    Conference number: 1

    Conference

    Conference1st South-East Europian Workshop on Formal Methods, SEEFM 2003
    Country/TerritoryGreece
    CityThessaloniki
    Period20/11/0320/11/03

    Fingerprint

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

    Cite this