Многие варианты коммуникационного протокола скользящего окна, который предназначен обеспечивать надежную передачу данных по ненадежным каналам, были специфицированы и верифицированы с использованием различных техник проверки, таких как доказательство теорем, проверка моделей и их комбинаций. В данной работе предлагается рассмотреть спецификацию протокола скользящего окна как мультиагентной модели. Темпоральные и эпистемические свойства протокола сформулированы с помощью логики знаний и времени.