A fully abstract model for graph-interpreted temporal logic

Graph-interpreted temporal logic is an extension of propositional temporal logic for specifying graph transition systems (i.e., transition systems whose states are graphs). Recently, this logic has been used for the specification and compositional verification of safety and liveness properties of rule-based graph transformation systems. However, no calculus or decision procedure for this logic has been provided, which is the purpose of this paper. First we show that any sound and complete deduction calculus for propositional temporal logic is also sound and complete when interpreted on graph transition systems, that is, they have the same discriminating power like general transition systems. Then, structural properties of the state graphs are expressed by graphical constraints which interpret the propositional variables in the temporal formulas. For any such interpretation we construct a graph transition system which is typical and fully abstract. Typical here means that the constructed system satisfies a temporal formula if and only if the formula is true for all transition systems with this interpretation. By fully abstract we mean that any two states of the system that can not be distinguished by graphical constraints are equal. Thus, for a finite set of constraints we end up with a finite state transition system which is suitable for model checking.