Weighted picture automata and weighted logics (Q2429722)

The author introduces a weighted MSO logic for defining series of pictures; here a picture is a finite rectangular array of symbols from a given (finite) alphabet. The main results of the paper show that the picture series over any commutative semiring definable by this logic are the same as the series recognized by weighted two-dimensional on-line tessellation automata -- also a new notion introduced here by the author -- and that these series are precisely the series recognizable by the picture automata previously considered in the literature. To achieve this, the formulas of the logic are restricted in a suitable way. Furthermore, the author proves some negative decidability results concerning the new formalisms. For example, it is shown that it is undecidable whether the support of the series defined by a formula is empty, or whether two tessellation automata recognize the same series.