图变换系统框架下的逆向条件建模
Modeling Adverse Conditions in the Framework of Graph Transformation Systems
摘要：
不利条件的概念涉及与敌对环境相互作用的系统，也可用于新技术的开发。我们提出了一种建模不利条件的图转换系统的方法。与图变换交互系统的其他方法相比，所提出的主要结构是图变换系统。我们介绍联合图变换系统，其中涉及一个系统，干扰环境，和一个自动机建模他们的相互作用。对于联合图变换系统，我们引入的概念（部分）正确性在不利的条件下，其中包含系统的正确性和恢复条件。作为主要结果，我们表明，两个实例的正确性，即k步正确性（恢复在最多k步后的环境干预）和最后一分钟的正确性（恢复，直到下一个环境干预）是可表达的线性时序逻辑（LTL），和一个较弱的概念k步正确性是可表达的CTL（计算树逻辑）。
英文摘要：
The concept of adverse conditions addresses systems interacting with an adversary environment and finds use also in the development of new technologies. We present an approach for modeling adverse conditions by graph transformation systems. In contrast to other approaches for graph-transformational interacting systems, the presented main constructs are graph transformation systems. We introduce joint graph transformation systems which involve a system, an interfering environment, and an automaton modeling their interaction. For joint graph transformation systems, we introduce notions of (partial) correctness under adverse conditions, which contain the correctness of the system and a recovery condition. As main result, we show that two instances of correctness, namely k-step correctness (recovery in at most k steps after an environment intervention) and last-minute correctness (recovery until next environment intervention) are expressible in LTL (linear temporal logic), and that a weaker notion of k-step correctness is expressible in CTL (computation tree logic).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
