Презентация 18 (1131946), страница 8

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

Текст из файла (страница 8)

Раскрашиваем вершины системы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.

Характеристики

Список файлов лекций