Portal de Periódicos da CAPES

Determinization of weighted finite automata over strong bimonoids

2010; Elsevier BV; Volume: 180; Issue: 18 Linguagem: Inglês

10.1016/j.ins.2010.05.020

1872-6291

Miroslav Ćirić, Manfred Droste, Jelena Ignjatović, Heiko Vogler,

Formal Methods in Verification

We consider weighted finite automata over strong bimonoids, where these weight structures can be considered as semirings which might lack distributivity. Then, in general, the well-known run semantics, initial algebra semantics, and transition semantics of an automaton are different. We prove an algebraic characterization for the initial algebra semantics in terms of stable finitely generated submonoids. Moreover, for a given weighted finite automaton we construct the Nerode automaton and Myhill automaton, both being crisp-deterministic, which are equivalent to the original automaton with respect to the initial algebra semantics, respectively, the transition semantics. We prove necessary and sufficient conditions under which the Nerode automaton and the Myhill automaton are finite, and we provide efficient algorithms for their construction. Also, for a given weighted finite automaton, we show sufficient conditions under which a given weighted finite automaton can be determinized preserving its run semantics.