CAJ | 학술논문

在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质。为此，该文使用一个离散时间区间时序逻辑公式建立实时系统模型，使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质，在此基础上，离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题。该文证明了新方法的有效性以及正确性，为区间实时逻辑这一类的模型检测问题提供了方法。
재동일개라집광가내무법자동험증실시구간모형적실시구간성질。위차，해문사용일개리산시간구간시서라집공식건립실시계통모형，사용령일개리산시간구간시서라집공식묘술실시계통수요만족적성질，재차기출상，리산시간구간시서라집통일모형검측문제즉가귀약위목전이해결적리산시간구간시서라집가만족성판정문제。해문증명료신방법적유효성이급정학성，위구간실시라집저일류적모형검측문제제공료방법。
There is no method for model checking real-time systems within the same real-time interval logic. To this end, we restrict a real-time logic, called Timed Interval Temporal Logic (TITL), on discrete time domain. And then, we use a TITL formula to construct an interval model and another TITL formula to describe an interval property. On the basis of this, we formalize a novel approach for model checking within the same logical framework based on TITL. The validity and correctness of the method are proved at last.