Временная и модальная логика в вычислениях

Временная и модальная логики расширяют классическую логику операторами для времени и возможности, предоставляя точные языки для спецификации того, как программа или реактивная система должны вести себя на протяжении всего своего выполнения.

Definition

Временная логика дополняет пропозициональную или логику первого порядка операторами, описывающими, когда свойства выполняются в ходе вычисления, такими как «всегда», «в конечном итоге» и «до тех пор, пока»; модальная логика обобщает это операторами для необходимости и возможности над структурой состояний и переходов.

Scope

Эта тема охватывает линейно-временные и ветвящиеся временные логики, такие как LTL и CTL, модальные логики, включая динамическую логику и модальное мю-исчисление, выражение свойств безопасности и живучести, а также алгоритмические проблемы проверки моделей и выполнимости, которые делают эти логики центральными для автоматизированной верификации.

Core questions

• Как логика может выразить, что что-то хорошее в конечном итоге произойдет или что что-то плохое никогда не произойдет?
• В чем разница между рассуждением об одном выполнении и обо всех возможных будущих состояниях?
• Как проверка того, удовлетворяет ли система временному свойству, становится алгоритмической?
• Какие временные логики обеспечивают баланс между выразительной мощностью и эффективной верификацией?

Key theories

Временная логика для спецификации программ

Пнуэли показал, что временная логика позволяет описывать корректность реактивных и параллельных программ, выражая свойства их выполнений, предоставляя унифицированный язык для требований безопасности и живучести.

Проверка моделей ветвящейся временной логики

Кларк и Эмерсон представили логику деревьев вычислений и алгоритм для ее автоматической верификации по отношению к конечному автомату, заложив основы области проверки моделей.

Clinical relevance

Временные логики являются языками спецификации для средств проверки моделей, рутинно используемых для верификации аппаратных проектов, протоколов связи и параллельного программного обеспечения, выявляя взаимоблокировки и нарушения безопасности и живучести до развертывания; эта технология принесла своим создателям премию Тьюринга и является стандартом в проектировании микросхем.

History

Пнуэли предложил временную логику для рассуждений о программах в 1977 году, а Кларк и Эмерсон, совместно с Кейлем и Сифакисом независимо, разработали проверку моделей около 1981 года. Подход был масштабирован до промышленных систем с помощью символических методов в начале 1990-х годов, и его создатели получили премию Тьюринга за эту технику.

Key figures

• Amir Pnueli
• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis

Seminal works

• clarkeEmerson1981
• huthRyan2004

Frequently asked questions

В чем разница между линейно-временной и ветвящейся временной логикой?

Линейно-временные логики, такие как LTL, описывают свойства одного, возможно бесконечного, пути выполнения. Ветвящиеся временные логики, такие как CTL, квантифицируют по дереву всех возможных будущих состояний из каждого состояния, позволяя утверждать, что свойство выполняется вдоль некоторого пути или вдоль всех путей. Они имеют различные выразительные возможности и алгоритмы верификации.

Как проверка моделей использует эти логики?

Система представляется в виде конечно-автоматной модели, а желаемое свойство — в виде формулы временной логики. Средство проверки моделей исчерпывающе исследует состояния, чтобы определить, выполняется ли формула, и если она не выполняется, оно генерирует трассу контрпримера, делая верификацию как автоматической, так и диагностической.