Проверка модели: свойства безопасности и живучести - PullRequest
1 голос
/ 14 февраля 2020

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

enter image description here

1 Ответ

1 голос
/ 15 февраля 2020

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

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

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

Стандартный пример взятия замыкания будет для L = a * b ^ omega = {bbb ..., abbb ..., aabbb ..., aaabbb ...}. Язык L содержит все трассы с конечным префиксом a и затем бесконечным числом b. Тогда замыкание (L) = a * b ^ omega + a ^ omega = LU {aaa ...}. След бесконечного числа а не содержится в L, но каждый конечный префикс ^ omega также является префиксом следа в 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) в целом, а не только для свойств безопасности.

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

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

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

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

...