  Linear implication can represent state transitions, but real transition
systems operate under temporal, stochastic or probabilistic constraints that
are not directly representable in ordinary linear logic. We propose a general
modal extension of intuitionistic linear logic where logical truth is indexed
by constraints and hybrid connectives combine constraint reasoning with logical
reasoning. The logic has a focused cut-free sequent calculus that can be used
to internalize the rules of particular constrained transition systems; we
illustrate this with an adequate encoding of the synchronous stochastic
pi-calculus. We also present some preliminary experiments of direct encoding of
biological systems in the logic.
