Проверка модели: свойства безопасности и живучести

Я знаю, что такое свойства «Безопасность» и «Живучесть», а также связь между префиксами «Безопасность» и «Плохой» свойства LT. Я хотел понять свойства закрытия и почему закрытие свойства безопасности является самим свойством. Изображение для справки. Может ли кто-нибудь объяснить мне концепции, которые можно использовать, чтобы я мог ответить на вопросы, это было бы действительно полезно.

введите здесь описание изображения


person Gopal Krishna    schedule 14.02.2020    source источник


Ответы (1)


Мы рассматриваем языки бесконечных следов.

Как вы намекнули, язык L определяется как свойство безопасности, если для каждой трассы, не принадлежащей L, существует плохой префикс, то есть конечный префикс, такой, что все бесконечные продолжения префикса не находятся в L. Итак, интуитивно понятно, что a Свойство безопасности говорит о том, что какое-то плохое событие не происходит.

Для данного языка L замыкание языка (L) определяется как состоящее из всех следов, где каждый конечный префикс также является префиксом следа в L.

Стандартный пример замыкания: L = a * b ^ omega = {bbb ..., abbb ..., aabbb ..., aaabbb ...}. Язык L содержит все следы с конечным префиксом a, а затем бесконечным числом b. Тогда замыкание (L) = a * b ^ omega + a ^ omega = L U {aaa ...}. След бесконечного числа а не содержится в L, но каждый конечный префикс ^ омеги также является префиксом следа в L. Следовательно, ^ омега содержится в замыкании L.

Теперь ваш вопрос: почему для свойства безопасности L верно, что L = замыкание (L).

Пусть L - свойство безопасности. Мы должны показать, что каждый след в L содержится в замыкании (L) и наоборот, что каждый след в замыкании (L) содержится в L.

  1. Каждый след в L содержится в замыкании (L): Рассмотрим сигму следа в L. Тогда каждый конечный префикс сигмы является префиксом сигмы. Следовательно, каждый конечный префикс сигмы является префиксом следа в L. Из определения замыкания (L) следует, что сигма находится в замыкании (L).

  2. Каждый след в замыкании (L) содержится в L: пусть сигма находится в замыкании (L). Предположим, что сигма не находится в L. По определению свойств безопасности сигма имеет конечный префикс w, такой, что никакое бесконечное продолжение w не находится в L. Но тогда w не может быть префиксом слова в L. Но по определению замыкания ( L), каждый конечный префикс сигмы должен находиться в L. Противоречие. Поскольку предположение, что сигма не принадлежит L, приводит к противоречию, отсюда следует, что сигма находится в L.

Примечание A: Обратите внимание, что для 1. мы не использовали L как свойство безопасности. Свойство, что L является подмножеством замыкания (L), выполняется в целом, а не только для свойств безопасности.

Примечание B: В примере для замыкания мы отметили, что для L = a * b ^ omega у нас есть замыкание (L) = a * b ^ omega + a ^ omega. Следовательно, L не равно замыканию (L), поэтому L не может быть свойством безопасности. Мы можем видеть это по следу a ^ omega, которого нет в L, но у него нет плохого префикса, поскольку каждый конечный префикс a ^ omega имеет форму a * и может быть продолжен до следа формы a * b ^ omega в L.

Примечание C: Мы могли бы также задать обратный вопрос: когда L = закрытие (L), является ли L свойством безопасности? Ответ положительный. Пусть L - язык с L = closure (L). Рассмотрим трассировку сигмы, которой нет в L. Мы должны показать, что сигма имеет плохой префикс. По L = замыкание (L) сигма не находится в замыкании (L). По определению замыкания (L), если все конечные префиксы сигмы находятся в L, у нас будет сигма в замыкании (L). Таким образом, из sigma not in closure (L) следует, что существует некоторый конечный префикс w сигмы, такой, что все следы sigma 'в L не имеют префикса w. Другими словами, любое бесконечное продолжение w не может быть следом в L. Следовательно, w - плохой префикс. В заключение, каждая сигма трассировки, которая не входит в L, имеет плохой префикс, поэтому L является свойством безопасности.

Боковое примечание D: Из вашего исходного вопроса и бокового примечания C мы можем сделать вывод, что L является свойством безопасности тогда и только тогда, когда L = закрытие (L). Это улучшает наше понимание того, что означает замыкание L: добавление всех трассировок, не имеющих плохого префикса. Кроме того, вы можете проверить, что замыкание замыкания не добавляет никаких новых трассировок, поэтому для любого L выполняется замыкание (L) = замыкание (замыкание (L)). Следовательно, для любого L замыкание (L) является свойством безопасности.

Боковое примечание E: Чтобы ответить на ваш вопрос с комментарием для примера языка, который равен его закрытию: Основываясь на примечании D, мы могли бы взять любое свойство безопасности: рассмотрим язык L над алфавитом {a, b, c}, который является L = {сигма в {a, b, c} ^ omega | сигма не имеет c}. Таким образом, плохими префиксами будут все конечные слова с буквой c (если вы думаете о трассировке как о моделировании выполнения некоторой программы, возможно, c может означать «сбой программы» и после этого совершает случайные действия). Мы можем проверить, что L = замыкание (L): мы уже знаем, что L подмножество замыкания (L) на основании 1. выше. Для другого направления рассмотрим сигму следа в замыкании (L). По определению замыкания (L) каждый конечный префикс w сигмы должен быть префиксом следовой сигмы 'в L. Поскольку по определению L сигма' не может содержать c, отсюда следует, что w не может содержать c. Когда каждый конечный префикс w сигмы не может содержать c, отсюда следует, что сигма не может содержать c. Следовательно, сигма находится в L. Мы заключаем, что L = замыкание (L).

person f9c69e9781fa194211448473495534    schedule 14.02.2020
comment
Спасибо за ответ. Вы можете привести пример, в котором замыкание (L) = L? - person Gopal Krishna; 15.02.2020
comment
Есть ли у вас какие-либо веб-ресурсы (MOOC, pdf), посвященные этой теме? Эта тема доставляет мне неприятности. - person Gopal Krishna; 15.02.2020
comment
Я добавил дополнительные примечания относительно закрытия (L) = L к своему ответу. Что касается ресурсов, я прочитал печатную копию Принципов проверки моделей Байера / Катоена. Может быть, вы могли бы проверить свою библиотеку на наличие копии. Также есть видеозапись лекции профессора Катоена (я могу получить к ней доступ без аутентификации, но я не уверен, что она может быть заблокирована по региону. Также она, конечно, не включает сеансы упражнений): video.fsmpi.rwth-aachen.de/11ws-modelchecking. Набор слайдов также можно найти в Интернете: move.rwth-aachen.de/teaching/ws-19-20/ - person f9c69e9781fa194211448473495534; 15.02.2020
comment
Привет, не могли бы вы изучить этот вопрос: stackoverflow.com/questions/60386048/ - person Gopala Krishna; 26.02.2020