Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Переходы, осуществляемые в модели Крипке, можно представить с помо­ щью орграфа см. Рис. 6.6. Пути реализуемые в модели Крипке можно предста­ вить в виде бесконечного дерева, см. Рис. 6.7. Отметим, что к модели Крипке могут быть сведены: булевы схемы, а также последовательные и параллель­ ные программы. Не оплакивай, смертный, вчерашних потерь. Дел сегодняшних завтрашней меркой не мерь. Ни былой, ни грядущей минуте не верь. Верь минуте текущей - будь счастлив теперь! Омар Хайям Если бы все прошедшее было настоящим, а настоя­ щее продолжало существовать наряду с будущим, кто был бы в силах разобрать: где причины и где по­ следствия? Козьма Прутков § 9. Временные (темпоральные) логнкн Временные (темпоральные) логики вводят понятия «было», «есть», «бу­ дет» {«раньше», «одновременно», «позже») и считается, что истинностное зна­ чение высказывания может быть разным в различные моменты времени. Па- пример, «самолёт летит» истинно во все те моменты времени, когда самолёт летит, и ложно во все те, когда он не летит. Темпоральные логики являются модальными логиками, они получаются добавлением к алгебре высказываний новых операторов, отражающих времен­ ные свойства. Темпоральные логики являются хорошим средством спецификации парал­ лельных систем (формулирования требований к параллельным системам). Они позволяют описывать порядок событий во времени, не привлекая время в явном виде. Отметим, что первые системы темпоральной логики были построены А. Прайором в 1954 и предназначались для реконструкции понятий возможности и необходимости. В настоящее время построены различные темпоральные ло­ гики, оперирующие понятиями прошлое, настоящее и будущее, в частности ло­ гики Пнуели. Пнуели впервые использовал их для проведения исследований параллельных систем. Темпоральные логики обычно классифицируются в соответствии с тем, является ли структура времени линейной или ветвящейся. Линейная модель времени предполагает, что в каждый момент времени существует только один непосредственно будущий (следующий) момент вре­ мени. 209