CAJ | 학술논문

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reachability checker),该工具能够沿指定路径(组)对单个线性混成自动机、多个线性混成自动机的组合进行可达性检验,并且在此基础上结合路径遍历技术完成对所有路径的有界可达性检验.实验数据显示,BACH不仅在面向路径可达性检验方面性能优异,可以适用于足够长度的路径,而且在针对所有路径的有界可达性检验时,BACH可以解决的问题规模也远远超过同类工具,已接近工业界应用的要求.
혼성자동궤적모형검험문제비상곤난,즉사시기중상대간단적일개자류--선성혼성자동궤,타적가체성문제잉연시불가판정적.현유적상관공구대도사용다면체계산래판정선성혼성자동궤상태공간적가체집,복잡도고、효솔저,무법해결실제응용규모적문제.묘술료일개면향선성혼성계통유계가체성모형검험공구--BACH(bounded reachability checker),해공구능구연지정로경(조)대단개선성혼성자동궤、다개선성혼성자동궤적조합진행가체성검험,병차재차기출상결합로경편력기술완성대소유로경적유계가체성검험.실험수거현시,BACH불부재면향로경가체성검험방면성능우이,가이괄용우족구장도적로경,이차재침대소유로경적유계가체성검험시,BACH가이해결적문제규모야원원초과동류공구,이접근공업계응용적요구.