Extending Nuxmv With Timed Transition Systems And Timed Temporal Properties
COMPUTER AIDED VERIFICATION, CAV 2019, PT I(2019)
摘要
NUXMV is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include MTL0,infinity formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing NuXmv with other verification tools for timed automata and MTL0,infinity,( )considering different benchmarks from the literature. The results show that NuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for MTL0,infinity.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络