基于权重区间的模态接口自动机

Modal interface automata with weight intervals

Gerald Lüttgen和Walter Vogler将接口自动机的输入输出行为引入到模态转换系统的模态逻辑中,从而可以隐式允许输入表达,称为模态接口自动机。但他们的工作并没有考虑量化信息,而实际应用中这类量化信息是必要的。本文通过将权重与转换关系相关联,来表达量化信息,建立了加权模态接口自动机,并重新定义了带有权重区间的精化关系。在这个框架中,我们研究了合取、析取和并发等系统算子,并证明了精化关系是关于这些算子的同余关系。

Gerald Lüttgen and Walter Vogler introduced the input and output behavior of interface automata into the modal logic of the modal transformation system so that the input expressions can be implicitly allowed,which is called a modal interface automaton.However,their work does not consider the quantitative information,which is necessary in practical applications.In this paper,by associating weights with transformation relations to express quantitative information,we establish a weighted modal interface automaton and define a new refinement relation with weight intervals.In this framework,we study the system operators such as conjunction,disjunction and concurrency,and prove that the refinement relation is a congruence relation on these operators.