We propose a bio-inspired automata-based formalism for the description of biological systems that allows properties of the system to be verified in a modular way. The properties expressed in the universal fragment of temporal logic CTL can be verified on a portion of the model, rather than on the whole model. We show an application to a case study from systems biology. We discuss further extensions of the approach, including dynamicity an reasoning with instances. Finally, we sketch the implementation and efficiency of the method.