Abstraction from Graphs to Multisets Using Temporal Logic

使用时态逻辑从图到多重集的抽象

• 批准号: 18500003
• 负责人: HAGIYA Masami
• 金额: $ 2.55万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2006
• 资助国家: 日本
• 起止时间: 2006 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18500003/
• 关键词: shape analysis; static analysis; termination analysis; model checking; modal 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

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

项目成果

遷移関係の詳細化による正則モデル検査の再構成と拡張

通过阐述转移关系重构和扩展全纯模型检查

• 发表时间: 2006
• 期刊: 日本ソフトウェア科学会第23回大会 1
• 作者: 櫻田英樹;萩谷昌己
• 通讯作者: 萩谷昌己

Finite Approximation Analysis of One Dimensional Cellular Automata

一维元胞自动机的有限逼近分析

• 发表时间: 2006
• 期刊: Computer Software Vol.23, No.3
• 作者: Koichi Takahashi;Yoshinori Tanabe;Toshifusa Sekizawa
• 通讯作者: Toshifusa Sekizawa

min-plus代数N∞上の様相μ計算とその応用

最小加代数N∞的模态μ计算及其应用

• 发表时间: 2007
• 作者: 五十嵐大;田辺良則;西澤弘毅;萩谷昌己
• 通讯作者: 萩谷昌己

A Decision Procedure for the Alternation-free Two-way Modal mu-calculus

无交替双向模态 mu 演算的决策过程

• 发表时间: 2005
• 期刊: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX),LNCS 3702
• 作者: Yoshinori Tanabe;Koichi Takahashi;Mitsuharu Yamamoto;Akihiko Tozawa;Masami Hagiya
• 通讯作者: Masami Hagiya

BDDを用いた2方向CTL論理式充足可能性決定手続きの実装

使用 BDD 实现双向 CTL 公式可满足性确定过程

• 期刊: コンピュータソフトウェア (To appear)
• 作者: 田辺良則;山本光晴;萩谷昌己
• 通讯作者: 萩谷昌己