================================================================================
P9323   M. Kaart & I. Polak
        "Het alternating bit protocol met time out in discrete tijd"


We specificeren en verifieren een variant van het Alternat ing Bit Protocol
waarbij een bovengrens aan het aantal hertransmissies wordt vastgelegd.
Zowel in gewone Process Algebra ACP als in de variant met discrete tijd
ACPdt worden specificaties gegeven. In het discrete tijd geval gebruiken we
temporele logica voor het bewijs.