Abstraction from Graphs to Multisets Using Temporal Logic
| Project/Area Number |
18500003
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
HAGIYA Masami The University of Tokyo, Graduate School of Information Science and Technology, Professor (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKAHASHI Koichi National Institute of Advanced Industrial Science and Technology, Research Center for Verification and Semantics, Vice-Director (40357372)
|
|---|
| Project Period (FY) |
2006 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥3,980,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥480,000)
Fiscal Year 2007: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2006: ¥1,900,000 (Direct Cost: ¥1,900,000)
|
|---|
| Keywords | shape analysis / static analysis / termination analysis / model checking / modal logic |
|---|
| Research Abstract |
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
|
Report
(3 results)
Research Products
(42 results)
-
-
-
-
-
[Journal Article] 関数部分知識と匿名性検証2007
Author(s)
川本裕輔, 真野健, 櫻田英樹, 萩谷昌己
-
Journal Title
日本応用数理学会論文誌 Vol.17,No.4
Pages: 559-576
Description
「研究成果報告書概要(和文)」より
Related Report
Peer Reviewed
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
