Reference:
, "K-Inductive Invariant Checking for Graph Transformation Systems", in Juan de Lara, Detlef Plump, Eds., Graph Transformation, vol. 10373 of LNCS, pp. 142-158, Cham: Springer, 2017.
Abstract:
While offering significant expressive power, graph transformation systems often come with rather limited capabilities for automated analysis, particularly if systems with many possible initial graphs and large or infinite state spaces are concerned. One approach that tries to overcome these limitations is inductive invariant checking. However, the verification of inductive invariants often requires extensive knowledge about the system in question and faces the approach-inherent challenges of locality and lack of context. To address that, this paper discusses $k$-inductive invariant checking for graph transformation systems as a generalization of inductive invariants. The additional context acquired by taking multiple (k) steps into account is the key difference to inductive invariant checking and is often enough to establish the desired invariants without requiring the iterative development of additional properties. To analyze possibly infinite systems in a finite fashion, we introduce a symbolic encoding for transformation traces using a restricted form of nested application conditions. As its central contribution, this paper then presents a formal approach and algorithm to verify graph constraints as k-inductive invariants. We prove the approach's correctness and demonstrate its applicability by means of several examples evaluated with a prototypical implementation of our algorithm.
Links:
@InProceedings{DG17,
AUTHOR = {Dyck, Johannes and Giese, Holger},
TITLE = {{K-Inductive Invariant Checking for Graph Transformation Systems}},
YEAR = {2017},
BOOKTITLE = {Graph Transformation},
VOLUME = {10373},
PAGES = {142-158},
EDITOR = {de Lara, Juan and Plump, Detlef},
SERIES = {LNCS},
ADDRESS = {Cham},
PUBLISHER = {Springer},
URL = {https://link.springer.com/chapter/10.1007/978-3-319-61470-0_9},
OPTacc_url = {},
PDF = {uploads/pdf/DG17_submission.pdf},
OPTacc_pdf = {},
ABSTRACT = {While offering significant expressive power, graph transformation systems often come with rather limited capabilities for automated analysis, particularly if systems with many possible initial graphs and large or infinite state spaces are concerned. One approach that tries to overcome these limitations is inductive invariant checking. However, the verification of inductive invariants often requires extensive knowledge about the system in question and faces the approach-inherent challenges of locality and lack of context.
To address that, this paper discusses $k$-inductive invariant checking for graph transformation systems as a generalization of inductive invariants. The additional context acquired by taking multiple (k) steps into account is the key difference to inductive invariant checking and is often enough to establish the desired invariants without requiring the iterative development of additional properties.
To analyze possibly infinite systems in a finite fashion, we introduce a symbolic encoding for transformation traces using a restricted form of nested application conditions. As its central contribution, this paper then presents a formal approach and algorithm to verify graph constraints as k-inductive invariants. We prove the approach's correctness and demonstrate its applicability by means of several examples evaluated with a prototypical implementation of our algorithm.}
}Copyright notice: This material is presented to ensure timely dissemination of
scholarly and technical work. Copyright and all rights therein are retained by
authors or by other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each author's copyright.
In most cases, these works may not be reposted without the explicit permission of
the copyright holder.
Powered by
bibtexbrowser