LTL и CTL: авторское изложение правил чтения

ru · official · sha256:11679b2df98df33c4fd3f17dcdf5a716ef3a77feb05f85992a824cf51c58796aRU

LTL И CTL: АВТОРСКОЕ ИЗЛОЖЕНИЕ ПРАВИЛ ЧТЕНИЯ Настоящий документ является АВТОРСКИМ ИЗЛОЖЕНИЕМ, составленным для целей формализации пакета logic.temporal. Он не является переводом и не воспроизводит текст ни одного из названных ниже источников: изложение пересказывает их определения своими словами и в каждом разделе называет источник, у которого определение взято. БАЙТЫ НАЗВАННЫХ ИСТОЧНИКОВ НЕ ЗАКРЕПЛЯЮТСЯ И ЗАКРЕПЛЕНЫ БЫТЬ НЕ МОГУТ. Работы A. Pnueli (1977), E. M. Clarke и E. A. Emerson (1981), E. A. Emerson и J. Y. Halpern (1986) и книга C. Baier, J.-P. Katoen «Principles of Model Checking» (MIT Press, 2008) охраняются авторским правом, живого открытого пина у них нет, и подставить сюда чью-то перепечатку значило бы объявить закреплёнными байты, которых репозиторий не видел. Источники названы в пакете декларациями без закрепления; страницы и номера строк не называются вовсе — печатного издания у репозитория нет, и выдумывать их запрещено. ЧТО ЗАКРЕПЛЕНО БАЙТАМИ. Байтами закреплены (а) настоящее изложение и (б) разделы Open Logic Project о темпоральной логике Прайора — операторах P, H, F, G, реляционных моделях времени, операторах Since и Until и о моделях возможных историй. Прайоровская часть пакета анкеруется в те байты; часть про LTL и CTL — в настоящее изложение. Настоящее изложение не является нормативным актом и не имеет силы источника права ни в одной юрисдикции.

ru · official · sha256:4c137577a83dc52b8c16c37e5a1cf4133a0586481a4fcea8d5cd264cef4a81f8RU

Раздел 1. Две традиции и почему их нельзя смешивать. Темпоральная логика Прайора («tense logic») говорит о моментах времени и рассматривает операторы прошлого и будущего над реляционной моделью. Темпоральные логики верификации — LTL и CTL — говорят о ВЫЧИСЛЕНИЯХ системы переходов: о путях, начинающихся в состоянии, и о состояниях вдоль пути. Языки, операторы и понятие истинности у них разные, и настоящий пакет держит их раздельно: формулы одной традиции не являются формулами другой, а правила чтения не переносятся без отдельного утверждения.

Referencing norms: ForeignOperator, foreign_operator

ru · official · sha256:fff70ec806dfc7883d6416f032a0ce08a7adc8542a0236f6e5aa29220b0b4446RU

Раздел 2. Система переходов и путь. Системой переходов называется тройка из множества состояний, тотального отношения переходов и разметки, сопоставляющей каждому состоянию множество истинных в нём атомарных высказываний. Путём называется бесконечная последовательность состояний, в которой каждое следующее достижимо из предыдущего одним переходом. Тотальность отношения переходов принимается ради того, чтобы всякий путь продолжался бесконечно; это условие модели, а не свойство формул. Изложено по: C. Baier, J.-P. Katoen, «Principles of Model Checking», MIT Press, 2008, глава 5 «Linear Temporal Logic».

Referencing norms: PATH, TRANSITION_SYSTEM

ru · official · sha256:c1d8dfb211188abed988a3c9ab9e149b44fcb93aa20b942e655f093d7f9adb24RU

Раздел 3. Язык LTL. Формулы LTL строятся из атомарных высказываний булевыми связками и темпоральными операторами: X («в следующем состоянии»), U («до тех пор, пока»), и производными от них F («когда-нибудь») и G («всегда»). У LTL ОДИН сорт формул: всякая формула LTL истинна или ложна на ПУТИ. Квантификации по путям язык LTL не содержит вовсе. Логика введена A. Pnueli, «The temporal logic of programs», 18th Annual Symposium on Foundations of Computer Science, 1977; изложение операторов — по Baier и Katoen, глава 5.

Referencing norms: LTL_EVENTUALLY, LTL_GLOBALLY, LTL_NEXT, LTL_UNTIL, L_LTL, temporal_operator

ru · official · sha256:7e0b2bd0420d77d4294ae7047ed645a85d5260f105f27c6f3a1f8149406e4cd3RU

Раздел 4. Правило чтения формулы LTL. Формула читается относительно пути и позиции на нём. X A истинна в позиции i, если A истинна в позиции i+1. A U B истинна в позиции i, если существует позиция j не меньше i, в которой истинна B, и во всех позициях от i до j, не включая j, истинна A. F A есть сокращение для «истина U A»; G A есть сокращение для «не F не A». Формула истинна в СОСТОЯНИИ, если она истинна на всех путях, начинающихся в этом состоянии; это отдельное соглашение о переходе от путей к состояниям, а не часть определения операторов.

Referencing norms: Readable, readable, reading_rule

ru · official · sha256:d493dfb752e16f7965a8610d450d64105495027367e52ed5a4ae73264ff231ceRU

Раздел 5. Язык CTL. CTL различает ДВА сорта формул: формулы состояний и формулы путей. Формула состояния строится из атомарных высказываний булевыми связками и парами «квантор по путям плюс темпоральный оператор»: A («на всех путях») и E («на некотором пути») в паре с X, U, F, G. Формула пути в CTL есть в точности одно применение темпорального оператора к формулам состояний: X A, A U B, F A, G A — и ничего сверх. Отсюда синтаксическое правило CTL: каждый темпоральный оператор обязан стоять непосредственно под квантором по путям, а каждый квантор по путям — непосредственно над темпоральным оператором. Логика введена E. M. Clarke и E. A. Emerson, «Design and synthesis of synchronization skeletons using branching time temporal logic», Logic of Programs, 1981; изложение — по Baier и Katoen, глава 6 «Computation Tree Logic».

Referencing norms: CTL_ALL_PATHS, CTL_EVENTUALLY, CTL_GLOBALLY, CTL_NEXT, CTL_SOME_PATH, CTL_UNTIL, L_CTL, OperatorProfile, PairingRequired, formula_sort, must_be_paired, operator_profile, pairing_required

ru · official · sha256:e0669477242777967a94a8e9803ac4906b08320f53831aa4acbe311fd67d2d1cRU

Раздел 6. Правило чтения формулы CTL. Формула состояния читается в СОСТОЯНИИ. E φ истинна в состоянии s, если существует путь из s, на котором истинна формула пути φ. A φ истинна в состоянии s, если на всяком пути из s истинна φ. Формула пути читается на пути и в позиции ноль: X A истинна, если A истинна во втором состоянии пути; A U B истинна, если существует позиция, в которой истинна B, и во всех предшествующих ей позициях пути истинна A. Десять базовых сочетаний — EX, AX, EF, AF, EG, AG, EU, AU — читаются этим правилом и никаким другим.

ru · official · sha256:52e6f05716e160384b02d02569e7c8b104391120061c44ad973d3c282e0c98d2RU

Раздел 7. Линейное и ветвящееся время. LTL говорит о множестве путей системы, рассматривая каждый путь отдельно; CTL говорит о дереве вычислений, растущем из состояния. Отсюда разница выразительных средств, установленная в литературе, а не выведенная настоящим пакетом: существуют свойства, выразимые в CTL и невыразимые в LTL, и свойства, выразимые в LTL и невыразимые в CTL, так что ни одна из двух логик не включает другую. Стандартные примеры: AG EF p («из любого достижимого состояния достижимо p») не выражается в LTL; F G p («начиная с некоторого момента всегда p») не выражается в CTL. Утверждения о невыразимости приводятся здесь КАК УТВЕРЖДЕНИЯ ИСТОЧНИКА и настоящим пакетом не доказываются; источник — E. A. Emerson, J. Y. Halpern, «"Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic», Journal of the ACM, том 33, номер 1, 1986, и изложение в Baier и Katoen, глава 6.

Referencing norms: Incomparable, expressiveness_claim, incomparable

ru · official · sha256:965c30ed15f9b5a25aecf7ac8b3f71b1419cf044e0990efac72266d2f9f87318RU

Раздел 8. Общая надстройка. CTL* есть логика, снимающая ограничение CTL на чередование кванторов по путям и темпоральных операторов; LTL и CTL суть её фрагменты. Настоящий пакет называет CTL* как общую надстройку и не описывает её правил чтения отдельно: описаны LTL и CTL, объявленные предметом работы.

Referencing norms: CTL_STAR

ru · official · sha256:96e9bc538584ee7f54cea49d9412643d0d6898c889ec6b850509e50e24b43b29RU

Раздел 9. Чего пакет не делает. Пакет не производит проверки моделей, не строит систем переходов, не перебирает путей и не решает задачи выполнимости. Формулы LTL и CTL представлены в нём как структуры — операторы, аргументы, сорт формулы, — а правила чтения как инструкции, привязанные к сорту формулы и к выбранному языку. Слово «истинна» в разделах 4 и 6 принадлежит ПЕРЕСКАЗУ ОПРЕДЕЛЕНИЯ ИСТОЧНИКА, а не результату какого-либо вычисления движка.