共同利用

Formalisation of Wang tiles for texture synthesis


種別 短期研究員
研究計画題目 Formalisation of Wang tiles for texture synthesis
研究代表者 Alexandre Derouet-Jourdan(OLM Digital Inc. / JST, CREST・Researcher / R&D Member)
研究実施期間 平成28年6月6日(月)~ 平成28年6月10日(金)
研究分野のキーワード Wang tiles, Planar polygon tiling, texture generation, formal verification of proof, Coq implementation
目的と期待される成果 The purpose of this research project is to continue a research work started with Associate Professor Mizoguchi about the use of Wang tiles in Computer Graphics. Wang tiles are a class of formal systems whose mathematical properties such as decidability and aperiodicity are the objects of active research. Recently, Wang tiles applied in computer graphics to create natural texture patterns. In a paper presented at MEIS 2015, we introduced a class of Wang tiles in collaboration with another member of R&D at OLM Digital Inc. We used these tiles to create stochastic wall patterns. The core of this paper was to prove that it was always possible to tile a rectangle with a border constraint, as soon as the rectangle contained a 2x2 square.
This result was then formally verified and implemented in Coq. This new result has been accepted at SCSS 2016.
We plan on formalising a generalisation of the MEIS 2015 paper to the tiling of planar connected polygons. We are currently working on the proof of this result as well as the corresponding algorithm and plan to submit it in February for publication. Our aim during this visit is to formally verify the validity of the proof using the proof assistant Coq and to extract from this proof a formally verified program.
This work will involve the formalisation of planar connected polygons with the related properties and functions, in particular the existence of a spanning tree and its construction algorithm. This work will also involve the formalisation of Wang tiles as a generalisation of the work that will be presented at SCSS 2016. By developing such a formalisation in Coq, we expect in the future to be able to formally check other proofs related to Wang tiles, that will allow for the development of robust texture generation algorithm in computer graphics.
組織委員(研究集会)
参加者(短期共同利用)
Alexandre Derouet-Jourdan(OLM Digital Inc. / JST, CREST・Researcher / R&D Member)