MicroRNA target validation by formal methods

MicroRNA, as one typical type of molecule in RNA interference mechanism, plays a significant role in carcinogenesis. The identification of the silencing targets is one critical task. The bioinformatics tools predict enormous number of targets so as to be considered that most of the results are false positive. Target validation represents a great challenge to microRNA studies. We develop a systematic way to address the above challenge. microRNA and its predicted targets are investigated in the context of biological pathways. The comparison of dynamical behaviours from the models with or without considering repression relations will determine the validity of the targets. Model-checking based formal method is introduced to facilitate this procedure. In case of lacking biological evidences, experimental design is proposed as well. The approach has been applied to mir-34a and its targets in apoptosis pathways.