Лекция 5. Логика линейного времени (LTL) (Лекции), страница 2
Описание файла
Файл "Лекция 5. Логика линейного времени (LTL)" внутри архива находится в папке "Лекции". PDF-файл из архива "Лекции", который расположен в категории "". Всё это находится в предмете "надёжность программного обеспечения" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
,где значения пропозициональных формул накаждом интервале совпадают.•Обозначим E(φ) набор всех трасс,отличающихся лишь значениями n1, n2,n3 (т.е. длиной интервалов)– E(φ) называется расширением прореживанияφ.Расширениепрореживанияx = 1 (y==0) mutex++ printf mutex‐‐ x = 0x==0y==0mutex==0трасса φтрасса φ1E(φ)x==1y==0mutex==0x==1x==1x==1x==1x==0y==0y==0y==0y==0y==0mutex==0 mutex==1 mutex==1 mutex==0 mutex==0p!q!pq!pqpqpqp!pp!pp!qqqq!q!pqp!qСвойства, инвариантныек прореживанию• Свойство φ, инвариантное к прореживанию, либоистинно для всех трасс из E(φ), либо ни дляодной из них:f v E( ), vf• истинность такого свойства зависит от порядка, вкотором пропозициональные формулы меняютсвои значения, и не зависит от длины трассы;• Теорема: все формулы LTL без оператора Xинвариантны к прореживанию.• Более того, в рамках LTL без X можно описать всесвойства, инвариантные к прореживанию.Практические приёмыописания свойств на LTLПрактические приёмы описаниясвойств на LTL• Выполнимость формулы LTL проверяетсятолько для первого состояния в трассе• Темпоральные операторы управляютпроверкой выполнимости своих аргументов• Сложное свойство можно (и нужно!)строить как суперпозицию простых• Суперпозиция темпоральных операторовне ограничивает диапазон действия«вложенного» оператора.Выполнимость формул LTL• Выполнимость формулы LTL определена ипроверяется для одного (первого)состояния трассы• Распространение свойств на другиесостояния управляется темпоральнымиоператорами• Единственный оператор, который можетограничить сверху проверкувыполнимости формулы – Un†lСуперпозиция формул LTL• Составлять сложные формулы LTL нужно методомсуперпозиции простых формул• Внешняя формула задаёт, на каких участкахвычислений будет проверятся подформула• Подформула задаёт свойства, проверяемые дляучастков вычислений• Суперпозиция темпоральных операторов неограничивает диапазон действия «вложенного»оператора.База шаблонов темпоральной логикиhttp://patterns.
projects.cis.ksu.eduЛогические паттерны (LTL/CTL/GIL)встречаемость(occurence)отсутствие(absense)порядок(order, sequence)универсальность(universality)существование(existence)boundedexistenceприоритет(precedence)chainprecedenceотклик(response)База шаблонов темпоральной логикиhttp://patterns. projects.cis.ksu.edu• Для каждого шаблона – пять вариантов формул:имяпример для “absense” и LTLвсегда[](!p)В чём разница?перед r<>r -> (!p U r)после q[](q -> [](!p))между r и q[]((r && !q && <>q) -> (!p U q))после r до q[]((r && !q) -> ((!p U q) || []!p))•База шаблонов темпоральнойлогики http://patterns.Для каждого шаблона– пять вариантов формул:projects.cis.ksu.eduимяпример для “absense” и LTLвсегдаrrqqqперед rпосле qмежду r иqпосле r доqrrqrrrqrrПример свойства, не выразимого наLTL• (p) может быть истинным после выполнениясистемой чётного числа шагов, но никогда не истиннопосле нечётного.• []X(p) не подходитtruep• p && [](p -> X!p) && [](!p -> Xp) – такжене подходит (здесь p всегда истинно послечётных шаговpСпасибо за внимание.