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

Improve this question
$\endgroup$
12
  • $\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, 2014 at 0:26
  • $\begingroup$ @YuvalFilmus Sure, I completed my question with the missing info. $\endgroup$
    – xiamx
    Oct 6, 2014 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, 2014 at 13:41
  • $\begingroup$ @KlausDraeger does $MinBadPref(P_{safe})=\{ab, aabb\}$ work? $\endgroup$
    – xiamx
    Oct 6, 2014 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, 2014 at 19:37

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
0

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.