Верификация мультиагентной модели протокола скользящего окна

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