[sv-ac] Recursive properties of SVA 3.1a

All:

I have noticed that the current definition of recursive properties in
SVA 3.1a enables the declaration of properties that define non-regular
languages. This appears to be a major disadvantage because
non-regular languages cannot be represented by finite automata. This
means that under the current definition, we will not be able to use
the automata-theoretic approach for model checking SVA properties. It
also raises doubt that efficient implementation will be possible for
such property forms. [I suspect that the model checking problem
for recursive properties under the current definition of SVA 3.1a
may even be undecidable.]

I believe that this defect can be fixed fairly easily by adding some
further restrictions on recursive properties.

As an example I will show a property Q that accepts the language

  {w| w has a prefix of the form "a^n b^n c" for some n>0}

over the alphabet {a,b,c}. This language in known to be non-regular.
Here are the declarations:

sequence S(v);
  v ##1 b;
endsequence

property P(v)
  (a and 1 |=> P(S(v))) or (v ##1 c);
endproperty

property Q;
  (a and 1 |=>P(b)) and (a [*1:$] ##1 b);
endproperty

Intuitively, the argument "v" is a sequence that accumulates "b" for
every "a" in the prefix.

To illustrate how Q works, consider evaluation of Q on a word with
prefix "aaabbbc":

- Q checks that the first letter of the word is "a" and then
  applies property P on the suffix "aabbbc" with argument "b".
- Then P applies P recursively on the suffix "abbbc" with argument "bb".
- Then P applies P recursively on the suffix "bbbc" with argument "bbb".
- Finally, since the suffix "bbbc" matches the sequence "v ##1 c", the
  last application of P ends the recursion and accepts.

Best regards,

Doron Bustan
Freescale Semiconductor, Inc.
Received on Fri Oct 8 14:47:11 2004