Verification of probabilistic behaviours

D. Dranidis; S. Andova; K. Tigka; T.A.C. Willemse

Verification of probabilistic behaviours

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

Research output: Contribution to conference › Paper › peer-review

36 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 language	English
Pages	84-99
Number of pages	16
Publication status	Published - 2004
Event	1st South-East European Workshop on Formal Methods: Agile Formal Methods: Practical, Rigorous Methods for a Changing World - Thessaloniki, Greece Duration: 20 Nov 2003 → 20 Nov 2003

Workshop

Workshop	1st South-East European Workshop on Formal Methods: Agile Formal Methods: Practical, Rigorous Methods for a Changing World
Period	20/11/03 → 20/11/03
Other	20 November 2003

Keywords

FMT-PA: PROCESS ALGEBRAS

Access to Document

ArticleFinal published version, 249 KB

Cite this

@conference{6e5b285279354e7db504c54355be975d,

title = "Verification of probabilistic behaviours",

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.",

keywords = "FMT-PA: PROCESS ALGEBRAS",

author = "D. Dranidis and S. Andova and K. Tigka and T.A.C. Willemse",

year = "2004",

language = "English",

pages = "84--99",

note = "1st South-East European Workshop on Formal Methods: Agile Formal Methods: Practical, Rigorous Methods for a Changing World ; Conference date: 20-11-2003 Through 20-11-2003",

}

TY - CONF

T1 - Verification of probabilistic behaviours

AU - Andova, S.

AU - Willemse, T.A.C.

A2 - Dranidis, D.

A2 - Tigka, K.

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

KW - FMT-PA: PROCESS ALGEBRAS

M3 - Paper

SP - 84

EP - 99

T2 - 1st South-East European Workshop on Formal Methods: Agile Formal Methods: Practical, Rigorous Methods for a Changing World

Y2 - 20 November 2003 through 20 November 2003

ER -

Verification of probabilistic behaviours

Abstract

Workshop

Keywords

Access to Document

Fingerprint

Cite this