
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 -ambiguous B\"uchi automata to image-binary B\"uchi automata, leading to model-checking algorithms with optimal computational complexity.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
