Image-Binary Automata

TL;DR

This paper introduces image-binary automata, a restricted class of weighted automata that accept regular languages efficiently, support polynomial operations, and are suitable for probabilistic model checking, offering advantages over unambiguous automata.

Contribution

The paper defines image-binary automata, demonstrates their succinctness and closure properties, and develops translation algorithms for probabilistic model checking.

Findings

Accept all regular languages

More succinct than NFAs

Support polynomial complementation, union, and intersection

Abstract

We introduce a certain restriction of weighted automata over the rationals, called image-binary automata. We show that such automata accept the regular languages, can be exponentially more succinct than corresponding NFAs, and allow for polynomial complementation, union, and intersection. This compares favourably with unambiguous automata whose complementation requires a superpolynomial state blowup. We also study an infinite-word version, image-binary B\"uchi automata. We show that such automata are amenable to probabilistic model checking, similarly to unambiguous B\"uchi automata. We provide algorithms to translate $k$-ambiguous B\"uchi automata to image-binary B\"uchi automata, leading to model-checking algorithms with optimal computational complexity.