计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2003年
11期
1424-1434
,共11页
反应系统%公平转换系统%时序逻辑%性质验证%可判定性
反應繫統%公平轉換繫統%時序邏輯%性質驗證%可判定性
반응계통%공평전환계통%시서라집%성질험증%가판정성
引进一个称为LTLC的连续时间时序逻辑,用来对反应系统进行规范与验证.LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质,这样就可将系统与性质间的满足关系转化为逻辑公式间的蕴涵关系.同时,采用非负实数集作为时间域还使我们可以利用标准的存在量词来表示变量隐藏,并可用逻辑蕴涵来表示反应系统间的求精关系.该文首先给出了LTLC的一个简单介绍,然后讨论了如何使用LTLC对反应系统进行表示与推理,最后证明了一个关于LTLC的可判定性结果.此结果可用于有穷状态反应系统的自动验证.
引進一箇稱為LTLC的連續時間時序邏輯,用來對反應繫統進行規範與驗證.LTLC的一箇重要特點是它能在統一的邏輯框架下錶示反應繫統及其性質,這樣就可將繫統與性質間的滿足關繫轉化為邏輯公式間的蘊涵關繫.同時,採用非負實數集作為時間域還使我們可以利用標準的存在量詞來錶示變量隱藏,併可用邏輯蘊涵來錶示反應繫統間的求精關繫.該文首先給齣瞭LTLC的一箇簡單介紹,然後討論瞭如何使用LTLC對反應繫統進行錶示與推理,最後證明瞭一箇關于LTLC的可判定性結果.此結果可用于有窮狀態反應繫統的自動驗證.
인진일개칭위LTLC적련속시간시서라집,용래대반응계통진행규범여험증.LTLC적일개중요특점시타능재통일적라집광가하표시반응계통급기성질,저양취가장계통여성질간적만족관계전화위라집공식간적온함관계.동시,채용비부실수집작위시간역환사아문가이이용표준적존재량사래표시변량은장,병가용라집온함래표시반응계통간적구정관계.해문수선급출료LTLC적일개간단개소,연후토론료여하사용LTLC대반응계통진행표시여추리,최후증명료일개관우LTLC적가판정성결과.차결과가용우유궁상태반응계통적자동험증.
