I am reading an article called The temporal semantics of concurrent programs .

On page $9$, there is a small section (numbered as $2$) called "clean behavior".

I think that there is a problem with this part, what does Pnueli meant by "Let $\lambda_i$ be the leagality condition for the statement departing from $m^i$" ?

I have marked the word "the" in bold since, as I see it, there can be more than one edge departing from $m^i$, an example can be seen on page $11$, at the beginning of part $5$.

Did I missunderstood something , or is there actually a mistake in the article by not addressing the fact that there can be more than one statement that can be exectuded after $m^i$, and that this expression for clean behavior need to be corrected accordingly ?


It would seem that in (1) (still page 9) he refers to a sequential program, so there is no concurrency. I think this assumption holds for the rest of the articles. So the "the" is ok there.

| cite | improve this answer | |

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.