All of the discussion is in the context of this paper.

I think that the whole procedure that the paper describes is not decidable, because if we can have an algorithm for it, then we can solve halting problem.

I begin with the definition of termination, which has not been expressed in the paper. First thing that comes to my mind as a suitable definition is this:

Definition (Termination): For all programs $\mathsf{P}$ and initial environments $\underline{\rho}$ it can be said that $ \mathsf{P} , \underline{\rho} $ terminates (shown by $ \mathsf{P} , \underline{\rho} \downarrow $) iff exists $\pi$ in $\mathcal{S^*} [\mathsf{P}]$ such that $\pi$ starts with $\langle l , \underline{\rho} \rangle$ (for an arbitrary label $l$) and contains state $\langle aft [\mathsf{P}] , \rho \rangle$ (for some arbitrary $\rho$).

I have no idea for a better definition, and I am going to continue based on this definition.

I think we can be sure that any trace, which exists in the set of prefix trace semantics of a program, is either infinite or it only has the $aft$ label of the program at its final state, such that it does not contain $aft$ if it is infinite. This claim can be proved by doing an inductive proof on the structures of our language.

So we can be sure that in our system the definition that I proposed here is equivalent to say that $\mathsf{P},\underline{\rho} \downarrow$ iff $\mathcal{S^*}[\mathsf{P}]$ does not contain any infinite trace.

In the paper we have this as "Definition 7":

Definition (Model Checking): If $\mathsf{P}$ is a program, $\mathsf{R}$ is a regular expression and $\underline{\rho}$ is an initial environment we define $\mathsf{P},\underline{\rho} \models \mathsf{R}$ as the model checking problem this way: $$\mathsf{P},\underline{\rho} \models \mathsf{R} \Leftrightarrow (\{\underline{\rho}\}\times \mathcal{S}^* [\mathsf{P}]) \subseteq \mathsf{prefix} (\mathcal{S}^r [\mathsf{R} \bullet (?:\mathfrak{tt})^*]) $$

As far as I could understand, in the paper it has been tried to give two other statements (equivalent to this one) for model checking problem, and at each time the definition has got more structural, thus easier to implement. But at the first place if we want to give an algorithm for computing something, first we need to be sure that it is computable (decidable). But I see a problem here in the matter of decidability of the inclusion relation in the above definition, which makes me doubt about the decidability of its two other equivalents statements as well. I think that if we replace the $\mathsf{R}$ with $\varepsilon$ what we get is $\mathsf{prefix} (\mathcal{S}^r [ \varepsilon \bullet (?:\mathfrak{tt})^*])$ which equals to $\mathcal{S}^r [ (?:\mathfrak{tt})^*]$ which contains all the finite traces and nothing more.

So if we have an algorithm which can decides about the inclusion relation, then we can decide if a program has an infinite trace in its semantics or not, which can actually be considered as an algorithm for halting problem, which we know that does not exist.

Did I get this right?!...

Edit: Well, I sent an email to Patrick Cousot himself, and he said:

Software model checking is not decidable, see comments at the end of the paper.



Your Answer

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