Model Checking Temporal Logic Formulas Using Sticker Automata.

Area of Science:

• Biomolecular Computing
• Formal Verification
• Theoretical Computer Science

Background:

• Model checking temporal logic, particularly CTL, ITL, and PTL, remains a complex challenge in DNA computing.
• Existing approaches for DNA model checking are limited, hindering the application of temporal logic in this domain.

Purpose of the Study:

• To develop a DNA-based model checking method for basic formulas in CTL, ITL, and PTL.
• To address the lack of effective DNA model checking approaches for temporal logic.

Main Methods:

• Encoding Finite State Automaton (FSA) models of temporal logic formulas into sticker automata using single-stranded DNA molecules.
• Encoding system models into input strings for the sticker automaton using DNA molecules.
• Utilizing biochemical reactions between DNA molecules to perform model checking.

Main Results:

• A novel DNA-based approach for checking basic CTL, ITL, and PTL formulas has been successfully developed.
• Simulated results demonstrate the effectiveness and feasibility of the proposed DNA model checking method.

Conclusions:

• The developed DNA computing method provides a viable solution for model checking temporal logic formulas.
• This work advances the field of DNA computing by enabling formal verification of complex systems using temporal logic.