Model Checking Multi-agent Sliding Window Protocol

Many variants of the communication sliding window
protocol were specified and verified using various techniques like
theorem proving, model checking and their combinations. In this
paper we consider a specification of the Sliding window protocol
as a multi-agent affine model. Temporal and epistemic properties
of the protocol are expressed in Logic of Knowledge and Time.