计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2003年
11期
16-18
,共3页
有色Petri网%状态空间%标记迁移系统%等价类
有色Petri網%狀態空間%標記遷移繫統%等價類
유색Petri망%상태공간%표기천이계통%등개류
在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间.但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下.该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果.
在有色Petri網的狀態空間中,有時一些狀態具有相似的行為,這些狀態可以用定義在狀態空間上的一緻的等價關繫來錶達,對每箇等價狀態類隻研究它的一箇代錶狀態的行為,這極大地減小瞭有色Petri網的狀態空間.但是,通常對一箇給定的等價關繫是否為一緻的驗證都是通過用戶的經驗人工進行的,這不但容易產生錯誤,而且效率低下.該文依據普通狀態圖和等價類狀態圖的標記遷移繫統關繫,對狀態空間一緻性等價定義的計算機輔助驗證做瞭深入的討論,給齣瞭相應的結果.
재유색Petri망적상태공간중,유시일사상태구유상사적행위,저사상태가이용정의재상태공간상적일치적등개관계래표체,대매개등개상태류지연구타적일개대표상태적행위,저겁대지감소료유색Petri망적상태공간.단시,통상대일개급정적등개관계시부위일치적험증도시통과용호적경험인공진행적,저불단용역산생착오,이차효솔저하.해문의거보통상태도화등개류상태도적표기천이계통관계,대상태공간일치성등개정의적계산궤보조험증주료심입적토론,급출료상응적결과.
