| %\halflineup | |
| \section{Conclusions and future work} | |
| \label{sec:conclusions} | |
| We have introduced an approach and a toolchain for instance-aware model checking of graph tranformation systems using \henshin and \mcrl, which increases the expressiveness of model checking for graph transformation systems by allowing to refer to specific instances and to quantify over node types. As future work, we plan to use \cadp as model checking back-end (since it supports counterexample extraction), and to investigate ways to accommodate for the increased state space sizes. | |
| %\halflineup | |
| % \paragraph{Notes on the \henshin Toolset} The graphical editor for rules in \henshin as shown in Figure~\ref{fig:railcab}, the state space generation and visualization as presented in Section~\ref{sec:statespaces} and the adapter for \mcrl and the other model checkers as presented in Section~\ref{sec:modelchecking-mcrl2} and~\ref{sec:modelchecking-other} was implemented by the first author of this paper. | |
| %\paragraph{Acknowledgments} The authors are grateful to the \mcrl development team for their support. |