| Title | Joint Optimization and Reachability Analysis in Graph Transformation Systems with Time |
| Publication Type | Conference Paper |
| Year of Publication | 2004 |
| Authors | Gyapay, S., Schmidt, Á., and Varró, D. |
| Conference Name | Proc. GT-VMT 2004, International Workshop on Graph Transformation and Visual Modelling Techniques |
| Publisher | Elsevier |
| Keywords | graph transformation, model checking, optimization |
| 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. |
| URL | http://www.inf.mit.bme.hu/FTSRG/Publications/varro/2004/gtvmt04_gsv.pdf |
