Joint Optimization and Reachability Analysis in Graph Transformation Systems with Time

TitleJoint Optimization and Reachability Analysis in Graph Transformation Systems with Time
Publication TypeConference Paper
Year of Publication2004
AuthorsGyapay, S., Schmidt, Á., and Varró, D.
Conference NameProc. GT-VMT 2004, International Workshop on Graph Transformation and Visual Modelling Techniques
PublisherElsevier
Keywordsgraph transformation, model checking, optimization
AbstractThe 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.
URLhttp://www.inf.mit.bme.hu/FTSRG/Publications/varro/2004/gtvmt04_gsv.pdf