Modular Verification of Interactive Systems with an Application to Biology

We propose an automata-based formalism for the description of biological systems that allows properties expressed in the universal fragment of CTL to be verified in a modular way. As an example we show the modelling of lac operon regulation and the modular verification of some properties.