|
времени; время непрерывно (компактно), если между каждой парой точек существует другая точка; • время полное или неполное. Структура полна, если для каждой последовательности точек, которая ограничена сверху другой точкой, существует такая точка, которая является, по крайней мере, верхней границей последовательности. Если время непрерывно, то оно полно, в дискретном времени оно неполно; ♦ время ограниченное или неограниченное, т.е ограничен или неограничен интервал времени, на котором происходит временная интерпретация. На основании проведенного анализа временных логик в качестве базовой для проведения временных рассуждений в ДЭС была принята временная логика с часами TLC (Temporal Logic with Clock), предложенной первоначально в работе [114] для целей верификащш реактивных систем [113]. TLC является временной модальной логикой, семантика которой такова, что каждая формула при конкретной временной интерпретации ассоциируется со своими локальными часами, т.е. с подпоследовательностями последовательности натуральных чисел, мыслимой как “глобальная’' временная шкала (глобальные часы), при этом конкретные значения формула приобретает в соответствии с семантикой TLC только для моментов времени (соответствующих натуральных чисел) на её локальных часах. В остальные моменты времени значение формулы не определено. Такой подход оказался удобным для изучения временных свойств ДЭС. Согласно рассмотренной классификацией TLC является линейной, дискретной, неограниченной временной модальной логикой. В TLC помимо обычных временных операторов □ и 0 (“всегда” и “иногда”) используются ещё два временных оператора • first и next. Их интуитивный смысл заключается в следующем: first А: формула А истинна в первый момент времени, next А: формула А истинна в следующий момент времени. |
85 Выбор структуры времени предполагает решение следующих подпроблем: • время линейное или частично упорядоченное. В большинстве формализмов оно рассматривается как линейное; • время дискретное или непрерывное. Время дискретно, если между каждой парой моментов времени существует конечное множество моментов времени; время непрерывно (компактно), если между каждой парой точек существует другая точка; • время полное или неполное. Структура полна, если для каждой последовательности точек, которая ограничена сверху другой точкой, существует такая точка, которая является, по крайней мере, верхней границей последовательности. Если время непрерывно, то оно полно, в дискретном времени оно неполно; • время ограниченное или неограниченное, т.е ограничен или неограничен интервал времени, на котором происходит временная интерпретация. На основании проведенного анализа временных логик в качестве базовой для проведения временных рассуждений в символьнологическом уровне ИСРВ была принята временная логика с часами TLC (Temporal Logic with Clock), предложенной первоначально в [167] для целей верификации реактивных систем [136]. TLC является временной модальной логикой, семантика которой такова, что каждая формула при конкретной временной интерпретации ассоциируется со своими локальными часами, т.е. с подпоследовательностями последовательности натуральных чисел, мыслимой как “глобальная” временная шкала (глобальные часы), при этом конкретные значения формула приобретает в соответствии с семантикой TLC только для моментов времени (соответствующих натуральных чисел) на её локальных часах. В ос тальные моменты времени значение формулы не определено. Такой подход оказался удобным для изучения временных свойств ИСРВ. Согласно рассмотренной классификацией 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 |