Modeling Adverse Conditions in the Framework of Graph Transformation Systems

TL;DR

This paper introduces a novel approach to modeling adverse conditions in systems using graph transformation systems, defining correctness notions under adverse interactions, and demonstrating their expressibility in temporal logics.

Contribution

It presents joint graph transformation systems with correctness notions under adverse conditions and shows their expressibility in LTL and CTL, advancing formal modeling of interacting systems.

Findings

Correctness notions under adverse conditions are formalized.

k-step and last-minute correctness are expressible in LTL.

A weaker k-step correctness is expressible in CTL.

Abstract

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).