A Nivat theorem for weighted picture automata and weighted MSO logics

摘要

Picture languages have been investigated by several research groups. Here, we define weighted two-dimensional on-line tessellation automata (w2oTA) taking weights from a new weight structure called picture valuation monoid. The behavior of this automaton model is a picture series mapping pictures to values. As our first main result, we prove a Nivat theorem for w2oTA. It shows a connection of mappings and recognizability of certain simple series. Then, we introduce a weighted MSO logic which models average density of pictures. In the second main result, we show that w2oTA and a fragment of our weighted MSO logics are expressively equivalent. (C) 2017 Elsevier Inc. All rights reserved.