Building on \'Esik and Kuich's completeness result for finitely weighted Kleene algebra, we establish relational and language completeness results for finitely weighted Kleene algebra with tests. Similarly as \'Esik and Kuich, we assume that the finite semiring of weights is commutative, partially ordered and zero-bounded, but we also assume that it is integral. We argue that finitely weighted Kleene algebra with tests is a natural framework for equational reasoning about weighted programs in cases where an upper bound on admissible weights is assumed.
翻译:基于Ésik与Kuich关于有限加权Kleene代数的完备性结果,本文建立了有限加权Kleene测试代数的关系完备性与语言完备性结果。与Ésik和Kuich的研究类似,我们假设权重的有限半环是交换、偏序且零有界的,但进一步要求其满足整性条件。我们认为,在假定可容许权重存在上界的情形下,有限加权Kleene测试代数为加权程序的等式推理提供了自然的形式化框架。