在图转换系统框架中建模不利条件

不利条件这一概念关注与对抗环境交互的系统，并在新技术开发中得以应用。我们提出一种通过图转换系统建模不利条件的方法。与其他图转换交互系统方法不同，所呈现的主要构造是图转换系统。我们引入联合图转换系统，其包含一个系统、一个干扰环境以及一个建模二者交互的自动机。对于联合图转换系统，我们引入不利条件下（部分）正确性的概念，其包含系统的正确性与一个恢复条件。作为主要结果，我们证明两类正确性实例，即 k 步正确性（环境干预后至多 k 步内恢复）与最后一刻正确性（直至下一次环境干预前恢复），可在 LTL（线性时序逻辑）中表达，且一种较弱的 k 步正确性概念可在 CTL（计算树逻辑）中表达。