@inproceedings {gtvmt04_gsv,
	title = {Joint Optimization and Reachability Analysis in Graph Transformation Systems with Time},
	booktitle = {Proc. GT-VMT 2004, International Workshop on Graph Transformation and Visual Modelling Techniques},
	series = {ENTCS},
	volume = {109},
	year = {2004},
	pages = {137-147},
	publisher = {Elsevier},
	organization = {Elsevier},
	abstract = {The design of safety critical systems frequently necessitates to simultaneously fulfill several logical and numerical constraints as requirements in order to deliver a functionally correct and optimal target system. In the current paper, we present a combined optimization and reachability analysis approach using the \textsc{Spin} model checker for problems modeled with graph transformation systems with time. First, we encode graph transformation rules into transitions systems in Promela (the input language of \textsc{Spin}). Then we restrict valid execution paths to time-ordered transformation sequences by additional logical conditions. The desired reachability property (as logical condition) is used to potentially decrease the global \emph{best cost} variable whenever a new path satisfies the property. The optimal solution for the problem is found by a single exhaustive run of the model checker encoding the numerical constraints into a dynamic LTL formula to cut off suboptimal paths violating the Branch-and-Bound heuristics.},
	keywords = {graph transformation, model checking, optimization},
	url = {http://www.inf.mit.bme.hu/FTSRG/Publications/varro/2004/gtvmt04_gsv.pdf},
	author = {Szilvia Gyapay and {\'A}kos Schmidt and D{\'a}niel Varr{\'o}}
}
