recursion - Model-checking with Mathematica. Comparison of recursive functions where argument is unknown function

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[0,a_]=0 
 S1[t_,a_]:=S1[t-1,a]+1/; a[t-1] 
 S1[t_,a_]:=0/; !a[t-1]

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


 S1[t,port]==2*S2[t,port]

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.