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.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Peter Drábik, Andrea Maggiolo-Schettini, Paolo Milazzo
• Keywords: Automata-based Formalism, ENTCS 2010, Lac Operon Regulation, Modular Way, Software Engineering