DNA-computing-based methods for Model Checking Temporal Logics with Actions

Up to now, there is no method available for Model Checking (MC) some temporal actions via DNA computing. In this paper, we propose an approach which employees DNA molecules to address this problem. First, a temporal logic formula with actions can be rewritten into its normal form. Second, the existing DNA-computing-based algorithms are extended and employed to compute and return model checking results between this formula describing a property of a system and an automaton expressing a system. As a result, an approach for model checking temporal logics with actions via DNA computing is obtained. Our experiments demonstrate the effectiveness of the proposed method. In addition, an approach based on probe machine is also pioneered in this study.