Weighted automata and weighted MSO logics for average and long-time behaviors
Weighted automata and weighted MSO logics for average and long-time behaviors
复制标题
DOI：
10.1016/j.ic.2012.10.001
复制
发表时间：
2012-11-01
影响因子：
1
通讯作者：
Meinecke, Ingmar
中科院分区：
文献类型：
--
作者：
Droste, Manfred;Meinecke, Ingmar
加权自动机对内存或功耗等系统的量化方面进行建模。最近，Chatterjee、Doyen和Henzinger引入了一种新的加权自动机，它可以计算平均成本或长期峰值功耗等目标。在这些自动机中，像平均值、极限上界、极限下界、极限平均或折扣这样的操作被用来为有限或无限的词赋值。一般来说，这些加权自动机不再是半加权的。在这里，我们建立了这种新型加权自动机与加权逻辑之间的联系。我们证明了适当的加权MSO逻辑和这些新的加权自动机在表达上是等价的，对于有限词和无限词都是如此。所采用的结构是有效的，导致所考虑的加权逻辑公式的可判断性结果。(C)2012 Elsevier Inc.保留所有权利。
Weighted automata model quantitative aspects of systems like memory or power consumption. Recently, Chatterjee, Doyen, and Henzinger introduced a new kind of weighted automata which compute objectives like the average cost or the long-time peak power consumption. In these automata, operations like average, limit superior, limit inferior, limit average, or discounting are used to assign values to finite or infinite words. In general, these weighted automata are not semiring weighted anymore. Here, we establish a connection between such new kinds of weighted automata and weighted logics. We show that suitable weighted MSO logics and these new weighted automata are expressively equivalent, both for finite and infinite words. The constructions employed are effective, leading to decidability results for the weighted logic formulas considered. (C) 2012 Elsevier Inc. All rights reserved.