# Set containment of MinimumBadPrefix and BadPrefix of a Safety Property

This question is related to formal model checking theory, but I cannot find a tag for it.

Let $P_{safe}$ be a safety property.

$BadPref(P_{safe})$ is the set of bad prefixes for $P_{safe}$

A Safety property $P_{safe}$ over Atomic Proposition $AP$ is regular if its set of bad prefixes is a regular language over $2^{AP}$

Is the following true?

1. If $L$ is a regular language with $MinBadPref(P_{safe}) \subset L \subset BadPref(P_{safe})$, then $P_{safe}$ is regular.

2. If $P_{safe}$ is regular, then any L for which $MinBadPref(P_{safe}) \subset L \subset BadPref(P_{safe})$ is regular.

My attempt to 2. is that it's true

$P_{safe}$ is regular then $MinBadPref(P_{safe})$ is regular and so is $BadPref(P_{safe})$. A NFA $N$ recognizing $BadPref(P_{safe})$ can be obtained by adding self loops on the final states of the NFA $M$ recognizing $MinBadPref(P_{safe})$. And $L$ is recognized by some NFA containing a subset of the self loops added to $M$. Therefore $L$ is regular.

And what about 1.?

• Can you explain what BadPref and MinBadPref are? Also, to anticipate my next question, explain what kind of object Psafe is. – Yuval Filmus Oct 6 '14 at 0:26
• @YuvalFilmus Sure, I completed my question with the missing info. – xiamx Oct 6 '14 at 0:40
• Note that this is exercise 4.4 from Baier&Katoen, Principles of Model Checking. As for your attempt to 2., you don't have $MinBadPref\subset BadPref$, since $bb$ is not contained. – Klaus Draeger Oct 6 '14 at 13:41
• @KlausDraeger does $MinBadPref(P_{safe})=\{ab, aabb\}$ work? – xiamx Oct 6 '14 at 16:04
• From the definition, $MinBadPref$ contains all those $w\in BadPref$ which do not have a proper prefix $u\in BadPref$ (so in particular, you cannot choose it - it is determined by $BadPref$). In this case ($BadPref=\{a^pb^q|p,q>0\}$) you get $MinBadPref=\{a^pb|p>0\}$, and then your $L$ won't work. – Klaus Draeger Oct 6 '14 at 19:37

$w\in BadPref$ if and only if $w$ has a prefix $u$ which is in $L$.