Abstraction from Graphs to Multisets Using Temporal Logic

为了分析图变换的过程，研究了一种基于节点抽象的多集逼近图的方法——基数分析法，并分析了图变换的每次操作对每一类抽象节点所对应的具体节点数的变化（增减）。首先，我们给出了图变换的每个操作和每个模态公式的最弱前提条件，并给出了满足公式的节点数因执行一个操作而减少的充分条件，从而验证了一个具体的列表操作程序的终止性。其次，为了推广基数分析，我们研究了对自然数集加无穷大得到的最小加代数上模态公式的语义解释。在这种语义下，满足某一公式的节点数用全局模态解释某一模态公式来表示。使用这种语义，不仅可以表示满足公式的节点数量，还可以表示各种数值度量，例如从阳极到另一个节点的最短路径的长度。为了证明这种语义的有效性，我们发明并实现了一种最小加代数上模态模微积分的模型检验算法。然后重新定义了运算的最弱前提和公式，使运算前的最小+代数上的最弱前提的解释等于运算后的公式的解释，并给出了运算前最弱前提的解释小于公式的充分条件。由于最小加代数是有充分根据的，因此可以用各种度量来分析终止性和活动性。除了这些结果之外，我们还改进了转换谓词抽象，这是终止和活性分析的一般方法，在效率和准确性方面。为了增加图结构和转换操作的表达性，我们还制定了分层模态逻辑。少

In order to analyze processes of graph transformation, we investigateda method, called cardinality analysis, which approximates graphs by multisets based on abstraction of nodes, and analyzes how the number of concrete nodes corresponding to each kind of abstract node changes (increases or decreases) by each operation of graph transformation. First, we formulated the weakest precondition for each operation of graph transformation and each modal formula, and by giving sufficient conditions for the number of nodes satisfying a formula to decrease by the execution of an operation, we verified termination of a concrete program that manipulates lists. Next, in order to generalize cardinality analysis, we investigated the semantics which interprets modal formulas on min-plus algebra obtained by adding infinity to the set of natural numbers. Under this semantics, the number of nodes satisfying a formula is represented by the interpretation of a certain modal formula with global modality. Usin … More g this semantics, one can express not only the number of nodes satisfying a formula, but also various numerical measures such as the length of the shortest path from anode to another node. To show the effectiveness of this semantics, we invented and implemented an algorithm for model checking of modal mu-calculus on min plus algebra. We then redefined the weakest precondition of an operation and a formula so that the interpretation of the weakest precondition on min-plus algebra before executing the operation is equal to that of the formula after the operation, and formulated sufficient conditions for the interpretation of the weakest precondition to be less than that of the formula. Since min-plus algebra is well-founded, one can analyze termination and liveness with various measures. In addition to these results, we improved transition predicate abstraction, which is a general method for termination and liveness analysis, with respect to efficiency and accuracy. We also formulated hierarchical modal logic in order to increase expressiveness of graph structures and transformation operations. Less