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