A symbolic model checking approach for real-time linear dynamic logic using testers
Guohao Li, Jun-Lin Lin, Xiangyu Luo · IET conference proceedings. · 2025
Ensuring the correctness of hardware and software systems through model checking is critically important, as errors in real-time systems may lead to catastrophic consequences. In industrial model checking, safety is a factor that must be considered in most cases, and safety-based model checking has been proven to be more efficient than traditional approaches. This paper proposes a discrete real-time linear dynamic logic (RTLDL) that combines propositional logic and regular expressions. Leveraging the property that safety detection can be reduced to invariance detection, we introduce a tester construction method for RTLDL and propose a symbolic model checking algorithm based on this tester. The proposed method was implemented on the model checker nuXmv using a translation approach. Experimental comparisons with the LDL model checker MCMAS-LDLK demonstrate that our method significantly outperforms MCMAS-LDLK in terms of efficiency for both LDL and RTLDL.