Zeitschriftenartikel
Infinite-state graph transformation systems under adverse conditions
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Journal Article
Zusatzinformation
Datum
2021
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
De Gruyter
Zusammenfassung
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.