In this paper we introduce a weighted LTL over product {\omega}-valuation monoids that satisfy specific properties. We also introduce weighted generalized B\"uchi automata with {\epsilon}-transitions, as well as weighted B\"uchi automata with {\epsilon}-transitions over product {\omega}-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted B\"uchi automata already introduced in the literature. We prove that every formula of a syntactic fragment of our logic can be effectively translated to a weighted generalized B\"uchi automaton with {\epsilon}-transitions. Finally, we prove that the number of states of the produced automaton is polynomial in the size of the corresponding formula.
翻译：在本文中,我们引入了对产品( yomega) 估价单体的加权LTL, 满足特定特性。 我们还引入了加权的B\ “ uchi automata with ~epsilon} - subsilon] 过渡, 以及加权的B\ “ uchi automatatomata with ~epsilon} - automata with ipsilon - successions 过渡, 并证明这两个模型与文献中已经引入的加权 B\ “ uchi automata ” 等同, 并证明这两个模型与文献中的加权的 B\ “ uchi automata ” 等同。 我们证明我们逻辑中每个组合法碎片的公式都可以有效地转换为加权的 B\ “ uchi automaton with yepsilon}- sultivervats。 最后, 我们证明所生产的自制型体的状态的数量与相应公式的大小是多元的。
相关内容
微信扫码咨询专知VIP会员