I would like to try some model-checking with recursive functions. The way it can be programmed with Mathematica (from my perspective) is following:

 S1[t_,a_]:=S1[t-1,a]+1/; a[t-1] 
 S1[t_,a_]:=0/; !a[t-1]

 S2[t_,a_]:=S2[t-1,a]+2/; a[t-1] 
 S2[t_,a_]:=0/; !a[t-1]  


Functions S1 and S2 get two arguments; time -- integer value and port function -- a function that takes time and returns a Boolean value.

Note, that function port[t], that returns Boolean value, is not known beforehand. But the value of S1 and S2 depend on the port value from the previous moment of time (a[t-1]). I guess that comparison must be done symbolically after unfolding the S1[t] and S2[t] functions.

Since what I have so far is a pretty much pseudo code, I would like to ask what would be the best way to do so, if it is possible at all with Mathematica.

Every tip is highly appreciated. Thanks very much in advance.

  • $\begingroup$ Do you wish to check that S1 and S2 have equivalent definitions? Or that they take the same value at a finite set of times? You obviously can't check that they take the same values at an infinite set of times. $\endgroup$
    – mikado
    Commented Oct 2, 2016 at 5:55
  • $\begingroup$ @mikado Thanks for the comment. So you think in this case it is not possible to write something like this: ForAll[x, x>=0, S1[x]==2*S2[x]] $\endgroup$ Commented Oct 3, 2016 at 8:34


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.