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