Saw Luca Cardelli give a talk about his research on abstract machines for characterizing signalling processes in biochemistry. Cool stuff. I still wonder, based on Kaustuv mentioning his ideas on the subject to me the other week, how closely it could be "logicalized" by something resembling linear logic. The main troubling thing is how linear logic's approach to state representation seems fundamentally constructive at some level regardless of the whether you're talking about the constructive or classical version of the logic itself: namely, there is a good notion of evidence for state transitions that do occur, but no evidence that transitions that do not or can not presently take place.
Yet if you want to bring timing into play, a reagent needs to have a witness for the absence of other reagents that it might react with during an interval of time in order for us to know that it persists across that interval.
I wonder if some species of focussing discipline would constrain proofs to consider all possible interactions between the current set of hypotheses, so that a reagent running through the whole gamut would indeed have sufficient evidence to conclude that it merely sticks around unreacted.