Проверяемый текст
Фоминых, Игорь Борисович; Нейрологические модели и методы решения задач в интеллектуальных системах реального времени (Диссертация 2000)
[стр. 151]

Заметим, что действия операторов first и next соотносятся с локальными часами формулы А (обозначаемыми как ск-, ), а не с глобальными часами (обозначаемыми как gck), если только глобальные часы не совпадают с локальными часами данной формулы.
TLC в отличии от других временных логик позволяет при выражении временных ограничений обходиться без использования
ыелогических символов в явных ссылках на длительность временных интервалов (измеряемую в количестве дискретов времени), что облегчает процесс доказательства формул, выражающих временные свойства исследуемых систем.
Например, свойство, смысл которого состоит в том, что формула q должна оказаться истинной не позднее, чем через 3 секунды после того, как окажется истинной формула р, выражается формулой р (q v next q v next next q v next next next q), или, короче з p
v next [i] q, где next [i] означает i применений оператора next.
Синтаксические конструкции TLC определяются следующим образом.

Словарь TLC включает помимо констант, переменных, функциональных и предикатных символов примитивные пропозициональные связки
i и а , универсальный квантор V н три временных оператора: first (начальный момент времени), next (следующий момент времени) и □ (всегда).
Термы в TLC определяются как обычно в логике первого порядка.
Определения правильно построенной формулы (ппф)
начнем с определения временного атома.
Определение 1.
Временной атом определяется рекурсивно следующим образом:
151
[стр. 86]

тальные моменты времени значение формулы не определено.
Такой подход оказался удобным для изучения временных свойств ИСРВ.
Согласно рассмотренной классификацией TLC является линейной, дискретной, неограниченной временной модальной логикой.
В TLC помимо обычных временных операторов □ и 0 (“всегда” и “иногда”) используются ещё два временных оператора first и next.
Их интуитивный смысл заключается в следующем: first А: формула А истинна в первый момент времени, next А: формула А истинна в следующий момент времени.
Заметим, что действия операторов first и next соотносятся с локальными часами формулы А (обозначаемыми как ск4 ), а не с глобальными часами (обозначаемыми как gck), если только глобальные часы не совпадают с локальными часами данной формулы.
TLC в отличии от других временных логик позволяет при выражении временных ограничений обходиться без использования
нелогических символов в явных ссылках на длительность временных интервалов (измеряемую в количестве дискретов времени), что облегчает процесс доказательства формул, выражающих временные свойства исследуемых систем.
Например, свойство, смысл которого состоит в том, что формула q должна оказаться истинной не позднее, чем через 3 секунды после того, как окажется истинной формула р, выражается формулой р -» (q V next q v next next q v next next next q), или, короче з p
-> v next [i] q, где next [i] означает i применений оператора next.
Синтаксические конструкции TLC определяются следующим образом.

86

[стр.,87]

Словарь TLC включает помимо констант, переменных, функциональных и предикатных символов примитивные пропозициональные связки 1 и л, универсальный квантор V и три временных оператора: first (начальный момент времени), next (следующий момент времени) и □ (всегда).
Термы в TLC определяются как обычно в логике первого порядка.
Определения правильно построенной формулы (ппф)
начнём с определения временного атома.
Определение 1.
Временной атом определяется рекурсивно следующим образом:
• если р является n-местным предикатным символом, a ei,...,en термы, то р (еь...,е„ ) временной атом.
Такие формулы будем называтсь чистыми временными атомами; • если А временной атом, то временными атомами являются также first A, next А.
Определение 2.
Правильно построенная формула (ППФ) определяется рекурсивно следующим образом: • все временные атомы суть ппф.
• если А и В ппф, то ппф будут также и -> A, first A, next А, □ А.
• если А и В ппф, то ппф будет также и (А д В).
• если А ппф, х переменная, свободная в А, то ппф будет также и (Vx ) А.
Логические связки v , — > , о и квантор существования 3 могут быть получены из примитивных связок и универсального квантора обычным путём.
Для временного оператора 0 (иногда) также используется обычное определение: dcf ОА “ — I [] — IА .
87

[Back]