Львов M. C.
Метод доказательства инвариантности линейных неравенств для линейных циклов

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

PDF

Бібліографічний опис:
Львов M. C.  Метод доказательства инвариантности линейных неравенств для линейных циклов. Кибернетика и системный анализ. 2014. Т. 50, № 4. С. 180-185. URL: http://jnas.nbuv.gov.ua/article/UJRN-0000412709