Infinite-state graph transformation systems under adverse conditions

Abstract

We present an approach for modeling adverse conditions by graph transformation systems. To this end, 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 present notions of correctness under adverse conditions. Some instances of correctness are expressible in LTL (linear temporal logic), or in CTL (computation tree logic), respectively. In these cases, verification of joint graph transformation systems is reduced to temporal model checking. To handle infinite state spaces, we incorporate the concept of well-structuredness. We discuss ideas for the verification of joint graph transformation systems using results based on well-structuredness.