В логике , временная логика является любая система правил и символика для представления и рассуждения о, предложения квалифицируются по времени (например, «Я всегда голоден», «Я в конце концов , быть голодным», или «Я буду голодным пока я что-нибудь не съем "). Иногда он также используется для обозначения временной логики , основанной на модальной логике системы темпоральной логики, введенной Артуром Прайором в конце 1950-х годов с важным вкладом Ханса Кампа . Дальнейшее развитие он получил компьютерными учеными , в частности Амиром Пнуэли , илогики .
Временная логика нашла важное применение в формальной верификации , где она используется для определения требований к аппаратным или программным системам. Например, можно сказать, что всякий раз , когда делается запрос, доступ к ресурсу в конечном итоге предоставляется, но он никогда не предоставляется двум запросчикам одновременно. Такое утверждение удобно выразить во временной логике.
Мотивация
Рассмотрим высказывание «Я голоден». Хотя его значение постоянно во времени, истинность утверждения может меняться во времени. Иногда это правда, а иногда ложь, но никогда одновременно истина и ложь. Во временной логике утверждение может иметь значение истинности, которое изменяется во времени - в отличие от вневременной логики, которая применяется только к утверждениям, значения истинности которых постоянны во времени. Такой подход к значению истинности с течением времени отличает темпоральную логику от вычислительной глагольной логики .
Временная логика всегда имеет возможность рассуждать о временной шкале. Так называемая линейная «логика времени» ограничивается этим типом рассуждений. Однако логика ветвления может приводить к нескольким временным рамкам. Это предполагает среду, которая может действовать непредсказуемо. Чтобы продолжить пример, в логике ветвления мы можем заявить, что «есть вероятность, что я останусь голодным вечно», и что «есть вероятность, что со временем я перестану есть». Если мы не знаем, накормят ли меня когда-нибудь, оба эти утверждения могут быть правдой.
История
Хотя логика Аристотеля почти полностью связана с теорией категориального силлогизма , в его работе есть отрывки, которые теперь рассматриваются как предвосхищение темпоральной логики и могут подразумевать раннюю, частично развитую форму временной модальной бинарной логики первого порядка. . Аристотель был особенно озабочен проблемой будущих контингентов , где он не мог согласиться с тем, что принцип бивалентности применим к утверждениям о будущих событиях, то есть что мы можем в настоящее время решить, является ли утверждение о будущем событии истинным или ложным, например, «там завтра будет морской бой ». [1]
Чарльз Сандерс Пирс отмечал в XIX веке, что в течение тысячелетий не было большого развития : [2]
Логики обычно считают время тем, что называется «внелогической» материей. Я никогда не разделял этого мнения. Но я думал, что логика еще не достигла той стадии развития, при которой введение временных модификаций ее форм не привело бы к большой путанице; и я еще в значительной степени придерживаюсь этого образа мыслей.
Артур Прайор был озабочен философскими вопросами свободы воли и предопределения . По словам его жены, он впервые задумался о формализации темпоральной логики в 1953 году. Он читал лекции по этой теме в Оксфордском университете в 1955–1956 годах, а в 1957 году опубликовал книгу « Время и модальность» , в которой представил модальную логику высказываний с две временные связки ( модальные операторы ), F и P, соответствующие «когда-нибудь в будущем» и «когда-нибудь в прошлом». В этой ранней работе Приор считал время линейным. Однако в 1958 году он получил письмо от Сола Крипке , в котором указывалось, что это предположение, возможно, необоснованно. В развитии, которое предвосхитило подобное в компьютерных науках, Приор принял это во внимание и разработал две теории ветвления времени, которые он назвал «Оккамистом» и «Пирсаном». [2] [ требуется разъяснение ] Между 1958 и 1965 годами Приор также переписывался с Чарльзом Леонардом Хамблином , и ряд ранних достижений в этой области можно проследить в этой переписке, например, следствия Гамблина . В 1967 году Прайор опубликовал свою наиболее зрелую работу по этой теме - книгу « Прошлое, настоящее и будущее» . Два года спустя он умер. [3]
Бинарные временные операторы Since и Again были введены Хансом Кампом в его докторскую диссертацию 1968 года. тезис, [4], который также содержит важный результат, связывающий темпоральную логику с логикой первого порядка - результат, теперь известный как теорема Кампа . [5] [2] [6]
Двумя первыми претендентами на формальную проверку были линейная временная логика , линейная временная логика Амира Пнуели и логика дерева вычислений, логика ветвящегося времени Мордехая Бен-Ари , Зохара Манна и Амира Пнуели. Практически эквивалентный CTL формализм был предложен примерно в то же время Э. М. Кларком и Э. А. Эмерсоном . Тот факт, что вторая логика может быть решена более эффективно, чем первая, не влияет на ветвление и линейную логику в целом, как это иногда утверждается. Напротив, Эмерсон и Лей показывают, что любую линейную логику можно расширить до логики ветвления, решение которой может быть решено с такой же сложностью.
Логика предшествующего времени (TL)
Сентенциальная напряжены логика введены в время и модальности имеет четыре (не- правды-функциональных ) модальные оператор (в дополнении ко всем обычным истинность-функциональные операторам в пропозициональной логике первого порядка . [7]
- П : «Дело было в том, что ...» (П означает «прошлое»)
- F : «Будет так, что ...» (F означает «будущее»)
- G : "Всегда будет так, что ..."
- H : "Всегда было так, что ..."
Их можно объединить, если мы позволим π быть бесконечным путем: [8]
- : "В какой-то момент верно во всех будущих состояниях пути "
- : " верно в бесконечно многих состояниях на пути "
Из P и F можно определить G и H , и наоборот:
Синтаксис и семантика
Минимальный синтаксис для TL определяется следующей грамматикой BNF :
где a - некоторая атомарная формула . [9]
Модели Крипке используются для оценки истинности предложений в TL. Пара ( T , <) множества T и бинарного отношения <на T (называемая «приоритетом») называется фреймом . Модель определяется тройка ( Т , <, V ) из рамы и функции V называется оценка , которая сопоставляет каждой паре ( , у ) атомарной формулы и значение времени некоторое значение истина. Понятие « ϕ истинно в модели U = ( T , <, V ) в момент u » обозначается сокращенно U ⊨ ϕ [ u ]. В этих обозначениях [10]
Заявление | ... верно только тогда, когда |
---|---|
U ⊨ a [ u ] | V ( a , u ) = верно |
U ⊨¬ ϕ [ u ] | не U ⊨ ϕ [ u ] |
U ⊨ ( ϕ ∧ ψ ) [ u ] | U ⊨ ϕ [ u ] и U ⊨ ψ [ u ] |
U ⊨ ( ϕ ∨ ψ ) [ u ] | U ⊨ ϕ [ u ] или U ⊨ ψ [ u ] |
U ⊨ ( ϕ → ψ ) [ u ] | U ⊨ ψ [ u ], если U ⊨ ϕ [ u ] |
U ⊨G ϕ [ u ] | U ⊨ ϕ [ v ] для всех v с u < v |
U ⊨H ϕ [ u ] | U ⊨ ϕ [ v ] для всех v с v < u |
Для класса F фреймов предложение ϕ языка TL является
- действует по отношению к F , если для каждой модели U = ( Т , <, V ) с ( Т , <) в F и для каждого U в T , U ⊨ ф [ у ]
- выполнима по отношению к F , если существует модель U = ( Т , <, V ) с ( Т , <) в F таким образом, что для некоторых U в T , U ⊨ ф [ у ]
- является следствием предложения ψ относительно F, если для любой модели U = ( T , <, V ) с ( T , <) в F и для любого u в T , если U ⊨ ψ [ u ], то U ⊨ ϕ [ u ]
Многие предложения действительны только для ограниченного класса фреймов. Обычно класс фреймов ограничивают теми, которые имеют отношение <, которое является транзитивным , антисимметричным , рефлексивным , трихотомическим , иррефлексивным , полным , плотным или некоторым их сочетанием.
Минимальная аксиоматическая логика
Берджесс излагает логику, которая не делает никаких предположений относительно отношения <, но допускает значимые выводы, основанные на следующей схеме аксиом: [11]
- , Где является тавтологией из логики первого порядка
- G ( A → B ) → (G A → G B )
- H ( A → B ) → (H A → H B )
- А → ГП А
- А → ВЧ А
со следующими правилами удержания:
- учитывая A → B и A , выведите B ( modus ponens )
- учитывая тавтологию A , вывести G A
- учитывая тавтологию A , вывести H A
Можно вывести следующие правила:
- Правило Беккера : для данного A → B выведите T A → T B, где T - время , любую последовательность, состоящую из G, H, F и P.
- Зеркальное отображение : по теореме A выведите ее зеркальное утверждение A § , которое получается заменой G на H (и, следовательно, F на P), и наоборот.
- Двойственность : по теореме A выведите двойственное утверждение A *, которое получается заменой на, G на F и H на P.
Перевод в логику предикатов
Берджесс дает перевод Мередита из утверждений в TL в утверждения в логике первого порядка с одной свободной переменной x 0 (представляющей настоящий момент). Эта трансляция M рекурсивно определяется следующим образом: [12]
где это приговор со всеми индексами переменных, увеличенными на 1 и является одноместным предикатом, определяемым .
Временные операторы
Временная логика имеет два типа операторов: логические операторы и модальные операторы [1] . Логические операторы - это обычные функциональные операторы истинности (). Модальные операторы, используемые в линейной временной логике и логике дерева вычислений, определены следующим образом.
Текстовый | Символический | Определение | Объяснение | Диаграмма |
---|---|---|---|---|
Бинарные операторы | ||||
φ U ψ | U ntil: ф имеет при токе или позиции в будущем, и φ имеет держать до этой позиции. В этой позиции φ больше не должно удерживаться. | |||
φ R ψ | R elease: ф - релизы ф если ψ верно вплоть до и включая первое положение , в котором φ истинно (или навсегда , если такая позиция не существует). | |||
Унарные операторы | ||||
N φ | N ext: φ должен удерживаться в следующем состоянии. ( X используется как синоним.) | |||
F φ | F uture: φ в конечном счете должен провести (где - то на последующем пути). | |||
G φ | G lobally: φ должен держать на весь последующий путь. | |||
А φ | A ll: φ должен удерживать все пути, начиная с текущего состояния. | |||
E φ | E xists: существует по крайней мере один путь , начиная с текущего состояния , где φ имеет место. |
Альтернативные символы:
- оператор R иногда обозначают через V
- Оператор W является слабым оператором до : эквивалентно
Унарные операторы - это правильно сформированные формулы, если B ( φ ) правильно сформирован. Бинарные операторы - это правильно сформированные формулы, если B ( φ ) и C ( φ ) правильно сформированы.
В некоторых логиках некоторые операторы не могут быть выражены. Например, оператор N нельзя выразить во временной логике действий .
Временная логика
Временная логика включает
- Интервальная временная логика (ITL)
- Линейная временная логика (LTL)
- Логика дерева вычислений (CTL)
- Временная логика сигнала (STL) [13]
- Временная логика отметки времени (TTL) [14]
- Язык спецификации свойств (PSL)
- CTL *, который обобщает LTL и CTL
- Логика Хеннесси-Милнера (HML)
- Модальное μ-исчисление, включающее в качестве подмножества HML и CTL *
- Метрическая временная логика (MTL) [15]
- Временная логика метрических интервалов (MITL) [13]
- Временная пропозициональная темпоральная логика (TPTL)
- Усеченная линейная временная логика (TLTL) [16]
- Гипервременная логика (HyperLTL) [17]
Вариация, тесно связанная с временной, хронологической или временной логикой, представляет собой модальную логику, основанную на «топологии», «месте» или «пространственном положении». [18] [19]
Смотрите также
- Формализм HPO
- Структура Крипке
- Теория автоматов
- Грамматика Хомского
- Система перехода состояний
- Расчет продолжительности (DC)
- Гибридная логика
- Временная логика в проверке с конечным числом состояний
- Временная логика действий (ВЛА)
- Важные публикации в формальной верификации (включая использование темпоральной логики в формальной верификации )
- Рео Координационный Язык
- Модальная логика
- Материалы исследования: Архив Общества Макса Планка
Заметки
- Перейти ↑ Vardi 2008, p. 153
- ^ а б в Варди 2008, стр. 154
- ^ Питер Эрстрём; Пер Ф.В. Хасле (1995). Временная логика: от древних идей до искусственного интеллекта . Springer. ISBN 978-0-7923-3586-3. С. 176–178, 210
- ^ «Темпоральная логика (Стэнфордская энциклопедия философии)» . Plato.stanford.edu . Проверено 30 июля 2014 .
- ^ Вальтер Карниелли; Клаудио Пицци (2008). Модальности и мультимодальности . Springer. п. 181. ISBN. 978-1-4020-8589-5.
- ^ Серджио Тессарис; Энрико Франкони; Томас Эйтер (2009). Reasoning Web. Семантические технологии для информационных систем: 5-я Международная летняя школа 2009 г., Бриксен-Брессаноне, Италия, 30 августа - 4 сентября 2009 г., Учебные лекции . Springer. п. 112. ISBN 978-3-642-03753-5.
- ^ Прайор, Артур Норман (2003). Время и методика: лекции Джона Локка за 1955-196 гг., Прочитанные в Оксфордском университете . Оксфорд: The Clarendon Press. ISBN 9780198241584. OCLC 905630146 .
- ^ Лоуфорд, М. (2004). «Введение в темпоральную логику» (PDF) . Департамент компьютерных наук Университета Макмастера .
- ^ Горанко, Валентин; Гальтон, Энтони (2015). Залта, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (зима 2015 г.). Лаборатория метафизических исследований Стэнфордского университета.
- ^ Мюллер, Томас (2011). «Временная или временная логика» (PDF) . В Хорстене, Леон (ред.). Непрерывный спутник философской логики . A&C Black. п. 329.
- ^ Берджесс, Джон П. (2009). Философская логика . Принстон, Нью-Джерси: Издательство Принстонского университета. п. 21. ISBN 9781400830497. OCLC 777375659 .
- ^ Берджесс, Джон П. (2009). Философская логика . Принстон, Нью-Джерси: Издательство Принстонского университета. п. 17. ISBN 9781400830497. OCLC 777375659 .
- ^ a b Maler, O .; Никович, Д. (2004). «Мониторинг временных свойств непрерывных сигналов». DOI : 10.1007 / 978-3-540-30206-3_12 .
- ^ https://asu.pure.elsevier.com/en/publications/timestamp-temporal-logic-ttl-for-testing-the-timing-of-cyber-phys
- ^ Koymans, R. (1990). «Определение свойств реального времени с помощью метрической временной логики», Real-Time Systems 2 (4): 255–299. DOI : 10.1007 / BF01995674 .
- ↑ Ли, Сяо, Кристиан-Иоан Василе и Калин Белта. «Обучение с подкреплением с вознаграждением временной логики». DOI : 10,1109 / IROS.2017.8206234
- ^ https://link.springer.com/chapter/10.1007/978-3-642-54792-8_15
- ^ Решер, Николай (1968). «Топологическая логика». Разделы философской логики . С. 229–249. DOI : 10.1007 / 978-94-017-3546-9_13 . ISBN 978-90-481-8331-9.
- ^ фон Райт, Георг Хенрик (1979). «Модальная логика места». Философия Николая Решера . С. 65–73. DOI : 10.1007 / 978-94-009-9407-2_9 . ISBN 978-94-009-9409-6.
Рекомендации
- Мордехай Бен-Ари, Зохар Манна, Амир Пнуели: временная логика разветвления времени . POPL 1981: 164–176
- Амир Пнуэли: временная логика программ FOCS 1977: 46–57
- Venema, Yde, 2001, «Temporal Logic», в Goble, Lou, ed., The Blackwell Guide to Philosophical Logic . Блэквелл.
- Э.А. Эмерсон и К. Лей, « Модальности для проверки модели: логика времени ветвления наносит ответный удар », в Science of Computer Programming 8, pp. 275–306, 1987.
- Э.А. Эмерсон, " Временная и модальная логика ", Справочник по теоретической информатике , глава 16, MIT Press, 1990
- Практическое введение в PSL , Синди Эйснер, Дана Фисман
- Варди, Моше Ю. (2008). «От церкви и до PSL ». В Орне Грумберг; Гельмут Вейт (ред.). 25 лет проверки моделей: история, достижения, перспективы . Springer. ISBN 978-3-540-69849-4. препринт . Исторический взгляд на то, как, казалось бы, разрозненные идеи соединились в информатике и инженерии. (Упоминание Черча в названии этой статьи - это ссылка на малоизвестную статью 1957 года, в которой Черч предложил способ проверки оборудования.)
дальнейшее чтение
- Питер Эрстрём; Пер Ф.В. Хасле (1995). Временная логика: от древних идей до искусственного интеллекта . Springer. ISBN 978-0-7923-3586-3.
Внешние ссылки
- Стэнфордская энциклопедия философии : « Временная логика » - Энтони Гальтон.
- Временная логика Yde Venema, формальное описание синтаксиса и семантики, вопросы аксиоматизации. Рассмотрение также диадических темпоральных операторов Кампа (с, до)
- Заметки Яна Ходкинсона об играх по темпоральной логике , включая формальное описание темпоральной логики первого порядка
- CADP - предоставляет общие средства проверки моделей для различной временной логики.
- PAT - это мощная бесплатная программа проверки моделей, проверка LTL, симулятор и проверка уточнения для CSP и его расширений (с общей переменной, массивами, широким диапазоном справедливости).