Свойство линейного времени

В проверке моделей , разделе информатики , свойства линейного времени используются для описания требований модели компьютерной системы . Примеры свойств включают в себя «торговый автомат не выдает напиток, пока не будут введены деньги» ( свойство безопасности ) или «компьютерная программа в конце концов завершает работу» ( свойство жизнеспособности ). Свойства справедливости можно использовать для исключения нереалистичных путей модели. Например, в модели двух светофоров свойство живучести «оба светофора бесконечно часто горят зеленым» может быть истинным только при условии безусловного ограничения справедливости «каждый светофор меняет цвет бесконечно часто» (чтобы исключить случай, когда один светофор «бесконечно быстрее», чем другой). ^[1]

Формально свойство линейного времени представляет собой ω-язык для степенного множества «атомарных высказываний». То есть свойство содержит последовательности наборов предложений, каждая последовательность известна как «слово». Каждое свойство можно переписать как « и Q оба встречаются» для некоторого свойства безопасности P и свойства жизнеспособности Q. P Инвариант системы — это то, что истинно или ложно для определенного состояния. Инвариантные свойства описывают инвариант, которому должно удовлетворять каждое достижимое состояние модели, в то время как свойства постоянства имеют форму «в конечном итоге навсегда сохраняется какой-то инвариант».

Временная логика, такая как линейная временная логика, описывает типы свойств линейного времени с помощью формул.

Эта статья посвящена пропозициональным свойствам линейного времени и не может обрабатывать предикаты о состояниях программы, поэтому она не может определить такое свойство, как: текущее значение y определяет количество раз, которое x переключается между 0 и 1 перед завершением. С этой задачей может справиться более общий формализм, используемый в свойствах безопасности и живучести .

Определение

Пусть AP — набор атомарных предложений. Слово закончено $2^{AP}$ ( множество AP степенное ) представляет собой бесконечную последовательность множеств утверждений, таких как $w:=\{a\}\{a,b\}\emptyset \{a,b\}^{\omega }$ (для атомарных предложений $AP=\{a,b\}$ ). Свойство линейного времени (LT) над AP является подмножеством $(2^{AP})^{\omega }$ то есть набор слов. ^[2] Пример свойства LT над множеством $\{a,b\}$ — это «набор слов, которые содержат бесконечно часто». Слово w входит в этот набор, потому что a содержится в $\{a,b\}$ , что происходит бесконечно часто. Слово, которого нет в этом наборе, $x:=\{a\}(\{b\}\emptyset )^{\omega }$ , поскольку a встречается только один раз (в первом наборе).

Свойство LT — это ω-язык над алфавитом $\Sigma =2^{AP}$ (и наоборот).

Мы обозначаем pref ( w ) конечные префиксы w (т.е. $\{\{a\},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}$ в приведенном выше случае). Закрытие LT-свойства P :

{\mathit {closure}}(P):=\{\sigma \in (2^{AP})^{\omega }\mid {\mathit {pref}}(\sigma )\subseteq {\mathit {pref}}(P)\}

Приложения

Структура Крипке над $\{p,q\}$ . Он не удовлетворяет свойству LT «бесконечно часто q » из-за пути $s_{1}s_{2}s_{3}^{\omega }$ . Оно действительно удовлетворяет свойству «бесконечно часто p », поскольку все возможные пути входят в него. $s_{1}$ или $s_{3}$ бесконечно часто.

Используя теорию конечных автоматов , программу или компьютерную систему можно смоделировать структурой Крипке . Свойства LT затем описывают ограничения на следы (выходы) структуры Крипке. Например, если два светофора на перекрестке представлены структурой Крипке, тогда атомарными предложениями могут быть возможные цвета каждого светофора, и может быть желательно, чтобы следы удовлетворяли свойству LT: «светофоры не могут оба быть зелеными на перекрестке». в то же время» (чтобы избежать столкновений автомобилей). ^[3]

Если каждый след структуры Крипке TS является следом TS ' , то каждое свойство LT, которому удовлетворяет TS ', удовлетворяется TS . Это полезно при проверке модели, чтобы обеспечить абстракцию: если упрощенная модель системы удовлетворяет свойству LT, то фактическая модель системы также будет ему удовлетворять. ^[4]

Классификация свойств линейного времени

Свойства безопасности

Свойство безопасности неформально имеет форму «плохих вещей не случается». ^[5] Например, если система моделирует банкомат (АТМ), то таким свойством будет «деньги не следует выдавать, пока не будет введен ПИН-код». ^[6] Формально свойство безопасности является свойством LT, так что любое слово, нарушающее это свойство, имеет «плохой префикс», для которого ни одно слово с этим префиксом не удовлетворяет этому свойству. То есть, ^[7]

\forall \sigma \in (2^{AP})^{\omega }\setminus P\ \exists {\text{ a finite prefix}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{is a prefix of}}\ \sigma '\}=\emptyset

В примере с банкоматом минимальный неверный префикс представляет собой конечный набор выполняемых шагов, в которых деньги выдаются на последнем этапе, а ПИН-код не вводится ни на одном этапе. Для проверки свойства безопасности достаточно рассмотреть только конечные следы структуры Крипке и проверить, не является ли такой след плохим префиксом. ^[8]

LT-свойство P является свойством безопасности тогда и только тогда, когда ${\mathit {closure}}(P)=P$ . ^[9]

Инвариантные свойства

Инвариантное свойство — это тип свойства безопасности, в котором условие относится только к текущему состоянию. ^[10] Например, пример с банкоматом не является инвариантом, поскольку мы не можем сказать, нарушено ли свойство, видя, что текущее состояние — «выдача денег», только видя, что текущее состояние — «выдача денег», а предыдущее состояние не было «прочитано». ПРИКОЛОТЬ". Примером инварианта является условие светофора «светофоры не могут быть зелеными одновременно» выше. Другой вариант — «переменная x никогда не бывает отрицательной» в модели компьютерной программы.

Формально инвариант имеет вид:

P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisfies}}\ \Phi \}

для некоторой пропозициональной логики формулы $\Phi$ . ^[10]

Структура Крипке удовлетворяет инварианту тогда и только тогда, когда каждое достижимое состояние удовлетворяет инварианту, что можно проверить с помощью поиска в ширину или поиска в глубину . ^[11] Свойства безопасности можно проверить индуктивно с использованием инвариантов. ^[12]

Свойства живости

Свойство жизнеспособности неформально имеет форму «со временем происходит что-то хорошее». ^[5] Формально P является свойством живучести, если ${\mathit {pref}}(P)=(2^{AP})^{*}$ т.е. любая конечная строка может быть продолжена до допустимой трассировки. ^[13]^[7] Примером свойства живучести является предыдущее свойство LT «набор слов, содержащих бесконечно часто». Никакой конечный префикс слова не может доказать, что слово не удовлетворяет этому свойству, поскольку слово может продолжать иметь бесконечное количество букв .

Что касается компьютерных программ, полезные свойства жизнеспособности включают «программа в конечном итоге завершается» и, в параллельных вычислениях , «каждый процесс в конечном итоге должен быть обслужен». ^[14]

Свойства устойчивости

Свойство персистентности — это свойство жизнеспособности формы «в конечном итоге навсегда». $\Phi$ ". То есть свойство вида: ^[15]

P=\{A_{0}A_{1}...\in (2^{AP})^{\omega }\mid \exists N\in \mathbb {N} :\forall n\geq N:A_{n}\ {\text{satisfies}}\ \Phi \}

Связь между свойствами безопасности и живучести

Никакой долгосрочной собственности, кроме $(2^{AP})^{\omega }$ (множество всех слов свыше $2^{AP}$ ) является одновременно свойством безопасности и живучести. ^[16] Хотя не каждое свойство является свойством безопасности или свойством жизнеспособности (считайте, что « а встречается ровно один раз»), каждое свойство является пересечением свойств безопасности и живучести. ^[5]

В топологии совокупность всех слов $(2^{AP})^{\omega }$ может быть оснащен метрикой :

d(w,x):=\inf\{2^{-|s|}\mid s\in {\mathit {pref}}(w)\cap {\mathit {pref}}(x)\}

Тогда свойство безопасности — это замкнутое множество , а свойство живучести — плотное множество . ^[17]

Свойства справедливости

Свойства справедливости — это предварительные условия, налагаемые на систему для исключения нереалистичных следов. ^[18]^[19] Безусловная справедливость имеет форму «каждый процесс бесконечно часто получает свою очередь». Сильная справедливость имеет форму: «каждый процесс получает свою очередь бесконечно часто, если он включается бесконечно часто». Слабая справедливость имеет форму «каждый процесс получает свою очередь бесконечно часто, если он постоянно активируется из определенной точки». ^[20]

В некоторых системах ограничение справедливости определяется набором состояний, а «справедливый путь» — это путь, который бесконечно часто проходит через какое-либо состояние в ограничении справедливости. Если существует несколько ограничений справедливости, то справедливый путь должен бесконечно часто проходить через одно состояние для каждого ограничения. ^[21] Программа «вполне удовлетворяет» свойству LT P относительно набора условий справедливости, если для каждого пути либо путь не соответствует условию справедливости, либо он удовлетворяет P . То есть свойство P выполняется для всех справедливых путей. ^[22]

Свойство справедливости реализуемо для структуры Крипке, если каждое достижимое состояние имеет справедливый путь, начинающийся из этого состояния. Пока ряд условий справедливости реализуем, они не имеют отношения к свойствам безопасности. ^[23]

Временная логика

Временная логика , такая как логика дерева вычислений (CTL), может использоваться для указания некоторых свойств LT. ^[24] Все формулы линейной темпоральной логики (LTL) являются свойствами LT. Используя аргумент подсчета, мы видим, что любая логика, в которой каждая формула является конечной строкой, не может представлять все свойства LT, поскольку должно быть счетное множество формул, но существует несчетное количество свойств LT.

Примечания

^ Байер и Катоен (2008) , с. 126.
^ Байер и Катоен (2008) , стр. 97–98.
^ Байер и Катоен (2008) , стр. 97–99.
^ Байер и Катоен (2008) , с. 102.
^ Jump up to: ^а ^б ^с Альперн и Шнайдер (1987) .
^ Байер и Катоен (2008) , с. 109.
^ Jump up to: ^а ^б Финкбайнер и Торфа (2017) , с. 4.
^ Байер и Катоен (2008) , с. 112.
^ Байер и Катоен (2008) , с. 113.
^ Jump up to: ^а ^б Байер и Катоен (2008) , с. 105.
^ Байер и Катоен (2008) , стр. 105–106.
^ Керн и Гринстрит (1999) , с. 135.
^ Байер и Катоен (2008) , с. 119.
^ Д'Сильва, Кронинг и Вайссенбахер (2008) , стр. 5.
^ Байер и Катоен (2008) , с. 197.
^ Байер и Катоен (2008) , с. 121.
^ Байер и Катоен (2008) , стр. 123–124.
^ Байер и Катоен (2008) , с. 124.
^ Керн и Гринстрит (1999) , стр. 131–132.
^ Байер и Катоен (2008) , стр. 126–127.
^ Кларк, Грумберг и Кронинг (2018) , стр. 32–33.
^ Байер и Катоен (2008) , с. 132.
^ Байер и Катоен (2008) , стр. 137–139.
^ Керн и Гринстрит (1999) , с. 127.

Ссылки

Альперн, Б.; Шнайдер, ФБ (1987). «Признание безопасности и живучести». Распределенные вычисления . 2 (3): 117. CiteSeerX 10.1.1.20.5470 . дои : 10.1007/BF01782772 . S2CID 9717112 .
Байер, Кристель ; Коттон, Йост-Питер (2008). Принципы проверки моделей . МТИ Пресс. ISBN 9780262026499 .
Кларк, Эдмунд М .; Грумберг, Орна ; Кренинг, Дэниел (2018). Проверка модели . МТИ Пресс. ISBN 9780262038836 .
Д'Сильва, Виджай; Кренинг, Даниэль ; Вайсенбахер, Георг (2008). «Обзор автоматизированных методов формальной верификации программного обеспечения» . Транзакции IEEE по автоматизированному проектированию интегральных схем и систем . 27 (7): 1165–1178. дои : 10.1109/TCAD.2008.923410 . S2CID 8921624 .
Финкбайнер, Бернд; Торфа, Хазем (2017). «Плотность свойств линейного времени». Конспекты лекций по информатике . Автоматизированная технология проверки и анализа. Том. 10482. Спрингер.
Керн, Кристоф; Гринстрит, Марк Р. (1999). «Формальная проверка проектирования аппаратного обеспечения: опрос». Труды АСМ по автоматизации проектирования электронных систем . 4 (2). Ассоциация вычислительной техники. дои : 10.1145/307988.307989 . ISSN 1084-4309 . S2CID 13994730 .

Дальнейшее чтение

Эмерсон, Э. Аллен (1990). «Временная и модальная логика». Справочник по теоретической информатике . Б.
Пнуэли, Амир (1986). «Применение темпоральной логики к спецификации и проверке реактивных систем: обзор текущих тенденций». В Дж. В. Баккере; В.-П. Ровер; Г. Розенберг (ред.). Текущие тенденции в параллелизме . Конспекты лекций по информатике. Том. 224. Спрингер. стр. 510–584. дои : 10.1007/BFb0027047 . ISBN 978-3-540-16488-3 .

[FOOTNOTEBaierKatoen2008126-1] Байер и Катоен (2008) , с. 126.

[FOOTNOTEBaierKatoen200897–98-2] Байер и Катоен (2008) , стр. 97–98.

[FOOTNOTEBaierKatoen200897–99-3] Байер и Катоен (2008) , стр. 97–99.

[FOOTNOTEBaierKatoen2008102-4] Байер и Катоен (2008) , с. 102.

[FOOTNOTEAlpernSchneider1987-5] Jump up to: ^а ^б ^с Альперн и Шнайдер (1987) .

[FOOTNOTEBaierKatoen2008109-6] Байер и Катоен (2008) , с. 109.

[FOOTNOTEFinkbeinerTorfah20174-7] Jump up to: ^а ^б Финкбайнер и Торфа (2017) , с. 4.

[FOOTNOTEBaierKatoen2008112-8] Байер и Катоен (2008) , с. 112.

[FOOTNOTEBaierKatoen2008113-9] Байер и Катоен (2008) , с. 113.

[FOOTNOTEBaierKatoen2008105-10] Jump up to: ^а ^б Байер и Катоен (2008) , с. 105.

[FOOTNOTEBaierKatoen2008105–106-11] Байер и Катоен (2008) , стр. 105–106.

[FOOTNOTEKernGreenstreet1999135-12] Керн и Гринстрит (1999) , с. 135.

[FOOTNOTEBaierKatoen2008119-13] Байер и Катоен (2008) , с. 119.

[FOOTNOTED'SilvaKroeningWeissenbacher20085-14] Д'Сильва, Кронинг и Вайссенбахер (2008) , стр. 5.

[FOOTNOTEBaierKatoen2008197-15] Байер и Катоен (2008) , с. 197.

[FOOTNOTEBaierKatoen2008121-16] Байер и Катоен (2008) , с. 121.

[FOOTNOTEBaierKatoen2008123–124-17] Байер и Катоен (2008) , стр. 123–124.

[FOOTNOTEBaierKatoen2008124-18] Байер и Катоен (2008) , с. 124.

[FOOTNOTEKernGreenstreet1999131–132-19] Керн и Гринстрит (1999) , стр. 131–132.

[FOOTNOTEBaierKatoen2008126–127-20] Байер и Катоен (2008) , стр. 126–127.

[FOOTNOTEClarkeGrumbergKroening201832–33-21] Кларк, Грумберг и Кронинг (2018) , стр. 32–33.

[FOOTNOTEBaierKatoen2008132-22] Байер и Катоен (2008) , с. 132.

[FOOTNOTEBaierKatoen2008137–139-23] Байер и Катоен (2008) , стр. 137–139.

[FOOTNOTEKernGreenstreet1999127-24] Керн и Гринстрит (1999) , с. 127.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]