计算机应用研究
計算機應用研究
계산궤응용연구
APPLICATION RESEARCH OF COMPUTERS
2012年
9期
3269-3273
,共5页
测试动作%动态时序逻辑%扩展%tableau算法%计算复杂性
測試動作%動態時序邏輯%擴展%tableau算法%計算複雜性
측시동작%동태시서라집%확전%tableau산법%계산복잡성
作为一种动态知识表示形式,动态时序逻辑( DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制.为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为20(n)的证明.分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值.
作為一種動態知識錶示形式,動態時序邏輯( DLTL)尤適用于正規程序驗證,然而它不直接支持測試動作,這使得其應用受到一定限製.為支持測試動作,提齣一箇DLTL擴展DLTL+和一箇判定DLTL+公式可滿足性的tableau算法,併給齣瞭算法的正確性以及其時間複雜度為20(n)的證明.分析錶明,DLTL+提供瞭一種直接的、有效的測試動作支持方式,該方式比已知的其他方式更具有實際應用價值.
작위일충동태지식표시형식,동태시서라집( DLTL)우괄용우정규정서험증,연이타불직접지지측시동작,저사득기응용수도일정한제.위지지측시동작,제출일개DLTL확전DLTL+화일개판정DLTL+공식가만족성적tableau산법,병급출료산법적정학성이급기시간복잡도위20(n)적증명.분석표명,DLTL+제공료일충직접적、유효적측시동작지지방식,해방식비이지적기타방식경구유실제응용개치.
