BoundedModelCheckingforRegionAutomata——区域自动机的有界模型检验

BoundedModelCheckingforRegionAutomataFangYu,Bow-YawWang,Yaw-WenHuangInstituteofInformationScienceAcademiaSinica,TaiwanIntroductionSAT-basedmodelcheckingfromdiscretesystemstotimesystemsChallengeHowtohandleinfinitetimingbehavior?DiscreteclocksZonepredicatesRegionAutomataReal-TimeSystemDiscretevariablesplusdense-timeclocksRealdomainAuniformrateincreaseReset012X:Y:TimedAutomataT...