With non-commutative linear logic (cf. Retoré 1997, for pomset logic), you can model the sequentiality of checking resources and avoid having the resource checking occur within the scope of whatever choice operator you want to use.
For example, you could model your query so:
$$(r; a \vee b) \multimap (c; r)$$
You might interpret this as saying: if I can take $r$ and then consume $a \vee b$, then I can provide $c$ and then free $r$. Is that the semantics you want?
It looks, unfortunately, like you can't combine non-commutative linear logic with usual linear logic in the sequent calculus and maintain the needed proof-theoretic properties to model planning via proof search. You can do this is the Calculus of Structures, see (Strassburger, 2003), which has been used for planning (Kahramanogullari 2009).
If you want to go the route of having a modality decorating just $t$, well that might be tricky because you essentially want to be able to look at $r$ without consuming it, and without having it available for unlimited use, which is not a propositional attitude of regular linear logic. You can try to see if
$$((?r \otimes a) \vee (?r \otimes b)) \multimap c$$
works for you, but it probably won't, because $?r$ is cheaper than $r$ — it is a bit like having a reference ro $r$; and so does not actually ensure that you can put your hands on $r$. $?!r$ might work better, and is the basis for the two encodings used to model classical logic in linear logic, but to have $r$ doesn't mean you can provide $?!r$. Looking at one of the various weak exponentials for linear logic might help here.
- Retoré 1997, Pomset logic: a non-commutative extension of classical linear logic
- Strassburger 2003, Linear Logic and Noncommutativity in the Calculus of Structures
- Kahramanogullari 2009, On Linear Logic Planning and Concurrency,
Information and Computation 207:1229 - 1258.