lect08 (1158549), страница 2
Текст из файла (страница 2)
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[](!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всегда !prrqqqперед rпосле qrrqrrrqrмежду r и qпосле r до qrСпасибо за внимание!Вопросы?.