Заметим, что действия операторов 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 |
тальные моменты времени значение формулы не определено. Такой подход оказался удобным для изучения временных свойств ИСРВ. Согласно рассмотренной классификацией 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 Словарь 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 |