A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology

Kaustuv Chaudhuri (1) , Joelle Despeyroux (2)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 Laboratoire d'Informatique, Signaux, et Systèmes de Sophia-Antipolis (I3S) / Equipe BIOINFO

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.

Mots clés: linear logic; hybrid logic; stochastic pi calculus; focusing; representational adequacy; molecular biology

Domaines: Logique en informatique [cs.LO]

Kaustuv Chaudhuri, Joelle Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology. [Research Report] 2013, pp.30. ⟨inria-00402942v5⟩