LTL-спецификация ограниченных счётчиковых машин

В статье пересматриваются результаты работы, посвящённой задаче представления поведения программной системы в виде набора формул линейной темпоральной логики LTL с последующим использованием этого представления для проверки выполнимости программных свойств системы через процедуру доказательства справедливости логических выводов, выраженных в терминах логики LTL. В качестве программных систем, для спецификации поведения которых применяется логика LTL, рассматриваются счётчиковые машины Минского с ограничениями. Ранее при работе с темпоральной логикой LTL как с программной логикой фактически был введён специальный псевдооператор обращения к предыдущим значениям переменных, задействованных в элементарных высказываниях. Несмотря на то что этот псевдооператор легко реализуется в верификаторе Cadence SMV при доказательстве справедливости логических LTL-выводов, классическое определение логики LTL не предполагает его наличия. В данной статье для построения LTL-спецификации поведения ограниченной счётчиковой машины будут использоваться только бинарные переменные, а отслеживание их предыдущих значений будет осуществляться исключительно в рамках самой логики LTL посредством соответствующих формул.