0
$\begingroup$

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.?

$\endgroup$
  • $\begingroup$ Can you explain what BadPref and MinBadPref are? Also, to anticipate my next question, explain what kind of object Psafe is. $\endgroup$ – Yuval Filmus Oct 6 '14 at 0:26
  • $\begingroup$ @YuvalFilmus Sure, I completed my question with the missing info. $\endgroup$ – xiamx Oct 6 '14 at 0:40
  • $\begingroup$ 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. $\endgroup$ – Klaus Draeger Oct 6 '14 at 13:41
  • $\begingroup$ @KlausDraeger does $MinBadPref(P_{safe})=\{ab, aabb\}$ work? $\endgroup$ – xiamx Oct 6 '14 at 16:04
  • $\begingroup$ 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. $\endgroup$ – Klaus Draeger Oct 6 '14 at 19:37
1
$\begingroup$

For (1), I will only give a sketch at first, in case you want to work it out yourself; I can add some details later if you want. Try proving the following:

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

(2) is already covered quite well by David's comments.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.