Verifying a Behavioural Logic for Graph Transformation Systems
Reference
Paolo Baldan, Andrea Corradini, Barbara König, and Bernhard König. Verifying a behavioural logic for graph transformation systems. In Proc. of COMETA '03, volume 104 of ENTCS, pages 5–24. Elsevier, 2004.
Abstract
We propose a framework for the verification of behavioural properties of systems modelled as graph transformation systems. The properties can be expressed in a temporal logic which is basically a
-calculus where the state predicates are formulae of a monadic second order logic, describing graph properties. The verification technique relies on an algorithm for the construction of finite over-approximations of the unfolding of a graph transformation system.
Suggested BibTeX entry:
@inproceedings{BCKK03,
author = {Paolo Baldan and Andrea Corradini and Barbara K{\"o}nig and Bernhard K{\"o}nig},
booktitle = {Proc. of COMETA '03},
pages = {5--24},
publisher = {Elsevier},
series = {ENTCS},
title = {Verifying a Behavioural Logic for Graph Transformation Systems},
volume = {104},
year = {2004}
}
