Презентация 18 (Лекции), страница 8
Описание файла
Файл "Презентация 18" внутри архива находится в папке "Лекции". PDF-файл из архива "Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 6 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 8 страницы из PDF
Раскрашиваем вершины системыGϕ1 ,M{p, ¬q}- ?ys1's2's1'- i{p, ¬q,6ϕ1 , Xϕ1 }s0{p, ¬q}s0y{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }is3&- i{p, ¬q} 6s4?i{p, ¬q}- ys3%{p, ¬q}ϕ1 , Xϕ1 }&{¬p, q}yϕ1 , Xϕ1 }s4?{p, ¬q}y%Алгоритм model checking для LTL4.
Выделяем радужные компонентысильнойсвязности{p, ¬q}- ?ys1's2's1'- i{p, ¬q,6ϕ1 , Xϕ1 }s0{p, ¬q}s0y{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }is3&- i{p, ¬q} 6s4?i{p, ¬q}- ys3%{p, ¬q}ϕ1 , Xϕ1 }&{¬p, q}yϕ1 , Xϕ1 }s4?{p, ¬q}y%Алгоритм model checking для LTL5. Выделяем вершины из которыхдостижимырадужные компонент{p, ¬q}- ?is1's2's1'- y{p, ¬q,6ϕ1 , Xϕ1 }s0{p, ¬q}s0y{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }ys3&- i{p, ¬q} 6s4?i{p, ¬q}- ys3%{p, ¬q}ϕ1 , Xϕ1 }&{¬p, q}yϕ1 , Xϕ1 }s4?{p, ¬q}y%Алгоритм model checking для LTL6. Ищем вершину (s0 , B) на которойопровергаетсяϕ1{p, ¬q}- ?is1's2's1'- y{p, ¬q,6ϕ1 , Xϕ1 }{¬p, q}y6%s2?y$${¬p, q}ϕ1 , Xϕ1 }s0s0yy{p, ¬q}{p, ¬q,ϕ1 , Xϕ1 }s3&- i{p, ¬q} 6s4?i{p, ¬q}ϕ1 , Xϕ1 }&{p, ¬q}- ys3%ϕ1 , Xϕ1 }s4?{p, ¬q}y%Алгоритм model checking для LTLИ в заключение несколько вопросовАлгоритм model checking для LTLИ в заключение несколько вопросов1. Как сложность описанного алгоритма model checkingзависит от размеров формулы и LTS?Алгоритм model checking для LTLИ в заключение несколько вопросов1.
Как сложность описанного алгоритма model checkingзависит от размеров формулы и LTS?2. Можно ли видоизменить описанный алгоритм modelchecking так, чтобы при раскраске вершин системыХинтикки можно было ограничиться только одним цветом?Алгоритм model checking для LTLИ в заключение несколько вопросов1. Как сложность описанного алгоритма model checkingзависит от размеров формулы и LTS?2. Можно ли видоизменить описанный алгоритм modelchecking так, чтобы при раскраске вершин системыХинтикки можно было ограничиться только одним цветом?3. Можно ли видоизменить описанный алгоритм modelchecking так, чтобы не строить всю систему Хинтиккицеликом?Алгоритм model checking для LTLИ в заключение несколько вопросов1. Как сложность описанного алгоритма model checkingзависит от размеров формулы и LTS?2.
Можно ли видоизменить описанный алгоритм modelchecking так, чтобы при раскраске вершин системыХинтикки можно было ограничиться только одним цветом?3. Можно ли видоизменить описанный алгоритм modelchecking так, чтобы не строить всю систему Хинтиккицеликом?А если захотите использовать model checking для LTL:SPIN и NuSMV — два самых известных программных средства,умеющих это делатьКонец лекции 18.