《表1 时间自动机常用符号》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《拟态防御系统的时间自动机模型和验证》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

时间自动机可以被视为一个六元组（L，L0，M，X，I，E），其中L:状态集合；L0:初始状态集，L0L；M:事件集合；X:时钟变量集合；I:状态不变式；E:状态转移函数．EL×M×（X）×2X×L为带时间约束的转移关系，包含自动机中的所有边．规则转换（l，m，x，z，l'）表示处于状态位置l的时，时钟满足约束条件x，系统可以发生事件m，从状态l转移到状态l'并完成z中的时间重置为0．表1介绍了利用PAT建模过程中需要用到的符号．