[billytetrud]

It seems to me that your specification language (formal logic?) sucks. If you can't specify parameters, then you can't compose. That's all you seem to be saying. You define the concept of states, but then you complain that you can't differentiate between timing of states between x and y. Well that's your own fault for not having a powerful enough definition of how states work. This has nothing to do with specifications at a fundamental level.