Linear Temporal Logic - XOR vs OR I am familiar with the **safety property** of critical sections, where two or more threads/processes cannot access the same shared resource at the same time. This is translated to LTL as $$\Box (\neg criti_1 \vee \neg criti_2)$$ It would be incorrect to describe it as $$\Box (\neg criti_1 \oplus \neg criti_2)$$ since it implies that one thread/process must always be in a critical section. There is a similar problem that I am having trouble translating into PTL. “It is always the case that once the machine accepts a coin followed by a selection, the machine will eventually provide coffee or tea” I am having a hard time deciding between the following two answers. $$1-\Box (coin \wedge \circ selection \rightarrow \lozenge(coffee \vee tea))$$ $$2- \Box (coin \wedge \circ selection \rightarrow \lozenge(coffee \oplus tea))$$ 1- would imply that you can either choose coffee or tea or both. 2- would imply only one between coffee and tea.

If you want to say that the vending machine dispenses one but not both beverages, then the exclusive or is the right choice.

However, it may be already known that the vending machine may never simultaneously produce different beverages, in which case, proving the property with the inclusive or may be all that is needed. This is often true, which is why you'll see the first formula at least as often as the second.

Note also that proving the property with the exclusive or does not rule out behaviors of the vending machine in which it outputs both coffee and tea for one coin, just not at the same time. For that, you'd need something like

$$ \Box((b \wedge \
eg c) \rightarrow \bigcirc \
eg b \,\mathsf{U}\, c) \enspace, $$

where $b$ stands for "either coffee or tea" and $c$ stands for "coin." In fact, a bit more complicated if you want to enforce the constraint that a coin must be deposited and a selection must be made before a new beverage is served.