CAJ | 학술논문

时间自动机系统中常含有多个时钟，通常都以相同的速率增长，若所有时钟都不复位，那么系统中任意两个时钟之间的约束关系将始终保持不变；然而实际的时间自动机系统中随着状态转移的发生，会有时钟复位，从而导致系统中任意两个时钟之间的约束关系发生变化，文中提出了如何使用DBM矩阵计算时间自动机中每个状态的时钟约束关系，并进行了正确性分析。为简化时间自动机系统中状态可达性分析提供了一定的依据。
시간자동궤계통중상함유다개시종，통상도이상동적속솔증장，약소유시종도불복위，나요계통중임의량개시종지간적약속관계장시종보지불변；연이실제적시간자동궤계통중수착상태전이적발생，회유시종복위，종이도치계통중임의량개시종지간적약속관계발생변화，문중제출료여하사용DBM구진계산시간자동궤중매개상태적시종약속관계，병진행료정학성분석。위간화시간자동궤계통중상태가체성분석제공료일정적의거。