О выразительности подхода к построению ПЛК-программ по LTL-спецификации

Статья посвящена подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV.
В статье демонстрируется состоятельность подхода к построению и верификации ПЛК-программ по LTL-спецификации с точки зрения тьюринговой мощности. Доказывается, что в соответствии с этим подходом для произвольной счётчиковой машины Минского может быть построена LTL-спецификация, по которой осуществляется её программная реализация на любом из языков программирования ПЛК стандарта МЭК 61131-3. Поскольку счётчиковые машины Минского равномощны машинам Тьюринга, то и рассматриваемый подход к программированию ПЛК будет обладать тьюринговой мощностью.
В доказательстве основное внимание уделяется заданию поведения счётчиковой машины в виде набора LTL-формул и сопоставлению этим формулам конструкций языков ST и SFC. SFC представляет интерес с точки зрения специфики графического языка, а язык ST рассматривается в качестве базового в том смысле, что реализация счётчиковой машины на языках IL, FBD/CFC и LD сводится к переписыванию на них конструкций ST-программы.
Идея доказательства демонстрируется на примере трехсчетчиковой машины Минского, реализующей функцию возведения числа в квадрат.