CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWe propose a technique for the analysis of infinite-state graph transformation systems, based on the construction of finite structures approximating their behaviour. Following a classical approach, one can construct a chain of finite under-approximations (k-truncations) of the Winskel style unfolding of a graph grammar. More interestingly, also a chain of finite over-approximations (k-coverings) of the unfolding can be constructed. The fact that k-truncations and k-coverings approximate the unfolding with arbitrary accuracy is formalised by showing that both chains converge (in a categorical sense) to the full unfolding. We discuss how the finite over- and under-approximations can be used to check properties of systems modelled by graph transformation systems, illustrating this with some small examples. We also describe the Augur tool, which provides a partial implementation of the proposed constructions, and has been used for the verification of larger case studies.
| Autori interni: | ||
| Autori: | BALDAN PAOLO; CORRADINI A; KOENIG BARBARA | |
| Titolo: | A Framework for the Verification of Infinite-State Graph Transformation Systems | |
| Anno del prodotto: | 2008 | |
| Digital Object Identifier (DOI): | 10.1016/j.ic.2008.04.002 | |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
http://hdl.handle.net/11568/126285
Copyright © 2022