计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2008年
6期
979-988
,共10页
空性检测%基于迁移的扩展Büchi自动机%可接受条件
空性檢測%基于遷移的擴展Büchi自動機%可接受條件
공성검측%기우천이적확전Büchi자동궤%가접수조건
对Couvreur提出的基于强连通图的空性检测算法进行改进,使基于嵌套的深度优先搜索与基于强连通图搜索算法的优势结合起来,在对基于迁移的扩展(具有多个可接受条件)Büchi自动机进行空性检测过程中,使用一个布尔变量标识一个状态,不仅节省了内存消耗,而且一般情况下的性能明显优于已有的算法,最坏情况等同于Couvreur的算法.同时反例寻找过程等同于基于强连通图的检测算法.
對Couvreur提齣的基于彊連通圖的空性檢測算法進行改進,使基于嵌套的深度優先搜索與基于彊連通圖搜索算法的優勢結閤起來,在對基于遷移的擴展(具有多箇可接受條件)Büchi自動機進行空性檢測過程中,使用一箇佈爾變量標識一箇狀態,不僅節省瞭內存消耗,而且一般情況下的性能明顯優于已有的算法,最壞情況等同于Couvreur的算法.同時反例尋找過程等同于基于彊連通圖的檢測算法.
대Couvreur제출적기우강련통도적공성검측산법진행개진,사기우감투적심도우선수색여기우강련통도수색산법적우세결합기래,재대기우천이적확전(구유다개가접수조건)Büchi자동궤진행공성검측과정중,사용일개포이변량표식일개상태,불부절성료내존소모,이차일반정황하적성능명현우우이유적산법,최배정황등동우Couvreur적산법.동시반례심조과정등동우기우강련통도적검측산법.
