黄润华 张晋津 张君瑶
摘 要：
Gerald Lüttgen和Walter Vogler将接口自动机的输入输出行为引入到模态转换系统的模态逻辑中，从而可以隐式允许输入表达，称为模态接口自动机。但他们的工作并没有考虑量化信息，而实际应用中这类量化信息是必要的。本文通过将权重与转换关系相关联，来表达量化信息，建立了加权模态接口自动机，并重新定义了带有权重区间的精化关系。在这个框架中，我们研究了合取、析取和并发等系统算子，并证明了精化关系是关于这些算子的同余关系。
关键词：
模态接口自动机；
量化信息；
精化关系；
系统算子
中图分类号：TP301 文献标识码：A 文章编号：1006-8228（2023）05-20-05
Modal interface automata with weight intervals
Huang Runhua1，2， Zhang Jinjin1，2， Zhang Junyao1，2
（1. College of Information Engineering， Nanjing Audit University， Nanjing， Jiangsu 211815， China;
2. Jiangsu Key Laboratory of Public Project Audit）
Abstract：
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.
Key words：
modal interface automata; quantitative information; refinement relationship; system operator
0 引言
De Alfaro和Henzinger T提出了接口自動机（Interface Automata）来解决软件和系统工程之间的组件组合问题[1]。Larsen的模态转换系统（Modal Transformation System）通过一系列改进将规范转化为实现，并且提供必须转换和可能转换的两种转换关系[2]。在文献[3]中，Gerald Lüttgen和Walter Vogler将接口自动机嵌入模态转换系统，提出了模态接口自动机（Modal Interface Automaton），它既能满足输入的一致性，又可以表达强制性输出，他们还修复了文献[4]中的缺陷，即精化关系不是关于并行运算具有同余性的。
近年来，一些接口理论[5-7]也研究了接口自动机和模态转换系统的结合，还有一些学者对模态接口自动机做了一些改进，比如Bujtor F和Vogler W在模态接口自动机中添加了时态逻辑，称为时态MIA，时态MIA允许对各种操作和逻辑连接进行异构规范[8]。但还没发现有学者对模态接口自动机进行量化信息的研究，而在实际系统中，存在着资源的消耗比如价格，燃料，时间等。在定量系统方面的研究也有很多，比如在自动机的定量研究中，Droste M和GastinP引入了一种带权重的逻辑关系，并分析了加权有限自动机的行为恰好是加权一元二阶逻辑中可定义序列的条件[9]。Line Juhl和Kim G. Larsen提出了一种新的模态转换系统扩展，称为加权模态转换系统[10]，它允许表达其预期实现的必须和可能行为，并给出了如何计算一组有限确定性规范的最大公共精化问题的算法。
本文提出了一种加权模态接口自动机（Weighted Modal Interface Automata），作为模态接口自动机的扩展。它用一系列权重区间来修饰每个转换关系，这些区间可以描述资源约束，如时间、资源、价格、燃料等消耗。我们还重新定义了加权模态接口自动机的精化关系，并且定义了三个系统操作符：合取、析取和并发。同时，我们给出精化关系是关于这些算子的同余性的定理。
本文第1节介绍加权模态接口自动机及相关概念，定义新的精化关系。在此基础上，第2节引入第一个系统算子——合取操作，并给出精化关系在合取操作上的同余性定理。第3节定义了另外两种系统算子——析取和并发，也给出精化关系在这两种系统算子上的同余性定理。最后第4节总结全文并指出未来研究方向。
1 加权模态接口自动机
1.1 基本定义
我们首先扩展模态接口自动机的概念，为其每个转换关系添加一个权重区间，这个权重区间表示对资源成本的量化限制，即一个行为（转换）上附加一个权重区间，表示该行为（转换）消耗的资源应在此区间范围内[11，12]。类似于文献[10]的方法，我们将该权重区用一个集合表示，并且可以在实现中将其细化为特定值。对于任意的[m，n∈Z∪-∞，+∞]，如果[m≤n，]则[m，n={a∈Z：m≤a≤n}]（即[m]与[n]之间的闭区间）称为权重区间。本文使用[I]表示所有此类非空区间的集合，用[W]、[V]等符号表示权重区间，用[W*]、[V*]等符号表示权重区间的集合。
定义1 一个加權模态接口自动机（WMIA）是一个六元组[M=Q，I，O，→，?，δ]，其中：
⑴ [Q]是一个状态集合；
⑵ [I，O]分别是输入和输出字母表，二者不相交且不含内部动作[τ]；
⑶ [→?Q×（I∪O）×（Q＼?））]表示必须转换关系；
⑷ [??Q×（I∪O∪{τ}）×Q）]表示可能转换关系；
⑸ [δ]是一个由[→∪?]到权重区间集[I]的函数。
我们用[A]表示[I∪O]，并将[A]和[A∪{τ}]中的元素分别表示为[a，b，c，d…]和[α， β， γ…]等。为了表述方便，在加权模态接口自动机中，我们规定：
● 如果[p， a， p"∈→]并且[δp， a， p"=W]，则记作[pa，Wp"]；
● 如果[p， a， p∈→]，我们写作[pap"]；
如果[?p"， pap"]，我们写作[pa]；
相反，如果不存在[p"]，使得[p， a， p∈→]，则记作[p?a]；
● 如果[pa]，我们写作[pa，W*P"]，其中，[P"={p"：pap"}]，[W*={W：pa，Wp"，p"∈P"}]；
● 令[W*]和[V*]是权重区间集合，如果对于任意的[W∈W*]，都存在[V∈V*]使得[W?V]，我们记作[W*≤V*]；
● 令[W*]和[V*]是权重区间集合，我们定义：
[W*∩V*={W∩V| W∩V≠?， W∈W*， V∈V*}]，
[W*∪V*={W∪V| W∈W*， V∈V*}]。
可能转换[?]的相关标记可以类似定义。
为了满足一致性，我们规定（a）如果[pa，W*P"]，则[?W∈W*，p"∈P"]，都有[p--→a，Wp"]；
（b）[?i∈I]，如果[p--→i，Wp"]则[?P"，pi，W*P"]并且[W∈W*]，[p"∈P"]；
（c）[?i∈I]，如果[pi，W*P"]并且[pi，W*P""]，则[P"=P""]。（b）和（c）的要求既加入了权重区间，又不改变文献[3]中关于模态接口自动机中的输入一致性。具体而言，（b）表示如果模态接口自动机中的一个状态可以进行一个可能转换到达一个后继状态，那么这个状态就可以进行必须转换，这能够保证模态接口自动机可以接受所有规定的输入；
（c）表示对于一个相同的输入而言，必须转换能够到达相同的后继状态集合。
因为转换过程内部动作的不可观测性，类似于文献[10]，本文不区分内部动作[τ]并且不考虑[τ]的量化信息。与通常定义类似，引入以下标记：（i）如果[qτ*q"]则记作[qεq"]；
（ii）对于[o∈O]，如果[qεq""oq"]，记作[qoq"]，其中这个公式中的输出动作[o]不含内部动作[τ]。进一步，我们定义如果[α=τ]，则[α=ε]，否则[α=α]。
1.2 精化关系
为了描述规范间和实现与规范间的精化关系，引入以下定义。我们现在可以定义WMIA的精化关系，这是MIA上精化关系的自然扩展。从现在起，当使用术语精化关系时，我们总是指下面定义的两个WMIA之间的模态精化关系。
定义2（WMIA精化关系） 假设[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是两个具有相同输入输出集合的WMIA，则[R?P×Q]是一个[WMIA]精化关系当且仅当对于任意的[p，q?R]，有
⑴ 若[qa，V*Q"]，则[?P"，pa，W*P"，W*≤V*]且[?p"∈P"，?q"∈Q"，p"，q"∈R]；
⑵ 若[p--→α，Wp"]且[α∈O∪{τ}]，则[?q"，q==?α，Vq"，]
[W?V]，且[p"，q"∈R]。
如果存在[WMIA]精化关系[R]使得[p，q∈R]，则称[p] WMIA-精化了[q]，写作[p?WMIAq]。进一步，如果[p?WMIAq]且[q?WMIAp]，我们称[p]和[q]是互精化的，记作[p=WMIAq]。
受文献[13]中关系定义的启发，本文在WMIA允许输入确定性的基础上，添加了条件[W?V]来优化精化关系的权重区间。因为一个状态进行相同动作的转换不一定只有一个后继状态，所以我们引入权重区间集合[W*]，[V*]的概念表示到达所有后继所需权重的集合，并使用“[≤]”表示区间集合之间的包含关系。如果可以用[P]来模拟[Q]的必须转换，并且可以[Q]来模拟[P]的可能转换，我们称[P]精化了[Q]。从直观上讲，如果[P]精化了[Q]，那么[Q]所消耗的资源量应包含[P]所消耗的资源量。
2 三种系统算子——合取
我们通过删除与MIA类似的不一致状态来定义WMIA的连接。区别在于，文献[3]中只考虑了MIA中动作的匹配，而我们还需要考虑WMIA中权重间隔的匹配。我们使用区间集之间的交集[W*∩V*]来表示转换关系所消耗的权重。因此，我们需要先引入合取积的定义。
定义3（WMIA的合取积） 假设[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是两个具有相同输入输出集合的WMIA，我们定义合取积[PQ]为：[PQ=defP×Q∪P∪Q，I，O，→，?，T]。它继承了[P]和[Q]的所有转换关系，并且对于所有的[i∈I]，[o∈O]，[α∈O∪{τ}]有以下规则：
（IMust1） 如果[pi，W*PP"]且[q?iQ]，
则[p，qi，W*P"]；
（IMust2） 如果[qi，V*QQ"]且[p?iP]，
则[p，qi，V*Q"]；
（IMust3） 如果[pi，W*PP"]且[qi，V*QQ"]，
则[p，qi，T*P"×Q"]，[T*=W*∩V*]；
（IMay1） 如果[p--→i，WPp"]且[q--→iQ]，
则[p，q--→i，Wp"]；
（IMay2） 如果[q--→i，VQq"]且[p--→iP]，
则[p，q--→i，Vq"]；
（IMay3） 如果[p--→i，WPp"]且[q--→i，VQq"]，
则[p，qi，Tp"，q"]，[T=W∩V]；
（OMust1） 如果[po，W*PP"]且[q==?o，VQ]，
则[p，qo，T*{p"，q"|p"∈P"，q==?o，VQq"}]，
[T*=W*∩V]；
（OMust2） 如果[qo，V*QQ"]且[p==?o，WP]，
则[p，qo，T*{p"，q"|q"∈Q"，p==?o，WPp"}]，
[T*=W∩V*]；
（May1） 如果[p==?τPp"]，
则[p，q--→τ（p"，q）]；
（May2） 如果[q==?τQq"]，
则[p，q--→τp，q"]；
（May3） 如果[p==?α，WPp"]且[q==?α，VQq"]，
则[p，q--→α，Tp"，q"]，[T=W∩V]。
因此，当WMIA中的[p]和[q]同时满足转换关系时，我们只需要考虑权重。我们使用所需权重区间的公共区间来表示合取积[（p，q）]的权重区间。当[W*∩V*=?]时，我们将其添加到不一致状态中。因此接下来我们由不一致状态引入WMIA的合取操作的定义。
定义4（WMIA的合取） 给定一个合取积[PQ]，则其不一致状态[F]定义为满足下面要求的最小集合：
（F1）[po，W*P]，[q=?oQ]，[o∈O]， 则[p，q∈F]；
（F2）[qo，V*Q]，[p=?oP]，[o∈O]， 则[p，q∈F]；
（F3）[po，W*P]，[qo，V*Q]，[o∈O]，但[W*∩V*=?]，则[p，q∈F]；
（F4）[p，qa，T*F"]，[F"?F]， 则[p，q∈F]；
合取操作[P∧Q]通过删除所有合取积[PQ]中属于不一致状态[F]的状态[p，q]，以确保[P∧Q]具有公共的输入和输出字母。我们定义[P∧Q]中的元素[p，q]为[p∧q]，其中所有的状态都是已定义的且一致的。
定理1 假设[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是两个具有相同输入输出集合的WMIA，[p∈P，q∈Q]，我们有以下结论：
（i） 如果[?WMIA R]，[r∈R]，则[r?WMIAp]且[r?WMIAq]当且仅当[p∧q]是已定义的；
（ii） 如果[p∧q]是已定义的并且对于所有的WMIA[ R]，[r∈R]，则[r?WMIAp]且[r?WMIAq]当且仅当[r?WMIAp∧q]。
上述定理表明，如果两个规范[p]和[q]没有共同的精化，那么它们在逻辑上是不一致的。此外，这个定理在（ii）中指出，WMIA的合取操作[∧]是关于精化关系[?WMIA]的最大的下界。因此，WMIA精化关系[?WMIA]与合取操作[∧]是具有同余性的。
3 三种系统算子——析取和并发
3.1 析取算子
在本节我们继续在WMIA上定义第二种系统算子——析取算子，并讨论它的性质；
特别是，对应于合取操作，这个运算符应该对应精化关系的最小的上界。
定义5（WMIA的析取） 假設[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是两个具有相同输入输出集合的WMIA，则析取算子[P∨Q]定义为
[P∨Q=def{p∨q|p∈P，q∈Q}∪P∪Q，I，O，→，?，T]其中[→]和[?]是满足[→P?→]，[→Q?→]，[?P??]，[?Q??]的最小集合并且满足下列转换关系：
（Must） 如果[pa，W*PP"]且[qa，V*QQ"]，
则[p∨qa，T*P"∪Q"]，[T*=W*∪V*]；
（May1） 如果[p--→α，WPp"]，则[p∨q--→α，Wp"]；
此外，如果[α∈I]，[q--→α，VQ]也成立；
（May2） 如果[q--→α，VQq"]， 则[p∨q--→α，Vq"]；
此外，如果[α∈I]，[p--→α，WP]也成立。
类似于合取，我们取[W*]和[V*]的并集作为[p∨q]的权重区间，（May1）和（May2）的规则是为了保证WMIA的输入确定性，即当[α∈I]时，我们规定状态[p]，[q]都可以做可能的[α]转换。那么到目前为止，我们已经为WMIA的析取算子增加了权重，并且应满足以下定理。
定理2 假设[P]、[Q]、[R]是WMIA，[p∈P]，[q∈Q]，[r∈R]。那么[p∨q?WMIAr]当且仅当[p?WMIAr]且[q?WMIAr]。
通过这个定理我们可以看出WMIA的析取操作[∨]是关于精化关系[?WMIA]的最小上界，并且WMIA精化关系[?WMIA]与析取操作[∨]是具有同余性的。
3.2 并发算子
在本节中我们定义WMIA的第三种系统算子——并发算子，并发运算对于系统和规范的组成非常重要。我们在WMIA上提供了一个并行运算符。如同定义合取运算符一样，这里采用的方法也是将所有的不一致状态识别出来并删除，并且在某些实现中不可避免地会出现错误的所有状态也都被删除。因此，同样我们需要先定义WMIA的并发积。
定义6（WMIA的并发积） 若[P1]和[P2]是WMIA，[P1]的[I1∪O1]记为[A1]，[P2]的[I2∪O2]记为[A2]，如果[A1∩A2=（I1∩O2）∪（O1∩I2）]，则我们称[P1]和[P2]是可结合的。对于这些可结合的WMIA，我们给出并发积[P1?P2]的定义为：[P1?P2=defP1×P2，I，O，→，?，T]，其中[I1∪I2＼O1∪O2]，[O1∪O2＼I1∪I2]，并且转换关系[→]和[?]满足以下条件：
（Must1） 如果[p1a，W*P"1]且[a?A2]，
则[p1，p2a，W*P"1×{p2}]；
（Must2） 如果[p2a，V*P"2]且[a?A1]，
则[p1，p2a，V*{p1}×P"2]；
（May1） 如果[p1--→α，Wp"1]且[α?A2]，
则[p1，p2--→α，Wp"1，p2]；
（May2） 如果[p2--→α，Vp"2]且[α?A1]，
则[p1，p2--→α，Vp1，p"2]；
（May3） 如果[p1--→α，Wp"1]，[p2--→α，Vp"2]且[W∩V≠?]，
则[p1，p2--→τp"1，p"2]。
可以看出，在[p1，p2--→τ]的情况下，我们需要权重间隔[W∩V]不能为空，否则它们不能交互。因此，对于[p1--→α，Wp"1]，[p2--→α，Vp"2]但[W∩V=?]的情况，我们认为它是（May1）和（May2）在[α∈A1]且[α∈A2]时的特殊情况，这种情况下的[p1]和[p2]虽然是不能交互的，即不能产生内部动作[τ]，但却仍能进行并发操作，因此我们以为此种情况不属于不一致状态。现在我们删除不一致状态得到WMIA的定义。
定义7（WMIA的并发） 给定一个并发积[P1?P2]，对于[a∈A1∩A2]，那么[p1，p2]被认为是一个错误状态应当满足下列几种情况之一：
⑴ 如果[a∈O1]，[p1--→a]且[p2?a]；
⑵ 如果[a∈O2]，[p2--→a]且[p1?a]。
进一步，我们定义并发积[P1?P2]的不一致状态[E]为满足以下条件之一的[p1，p2∈E]的最小集合：
（i） [p1，p2]是一个错误状态；
（ii） 对于[α∈O∪τ]，[p1，p2--→αp"1，p"2]，且[p"1，p"2∈E]。
[P1]和[P2]的并發操作[P1|P2]是通过删除[P1?P2]中的所有的不一致状态[E]得到的。其中的所有的不一致状态包括转换关系都需要删除，并且所有必须转换下的可能转换也都要删除。此时，如果[p1，p2∈P1|P2]，我们称[p1]和[p2]是协调的，写作[p1|p2]。
在WMIA的并发算子定义中，我们没有考虑[τ]动作的必须转换关系，因为它与精化关系无关。类似于合取算子和析取算子的同余性定理，对于并发的同余性，我们也应有以下定理。
定理3 令[P1]，[P2]和[Q1]是WMIA，[p1∈P1]，[p2∈P2]，[q1∈Q1]并且[p1?WMIAq1]。如果[P2]和[Q1]是可结合的，那么：
⑴ [P1]和[P2]是可结合的；
⑵ 如果[p2]和[q1]是协调的，那么[p1]和[p2]也是协调的并且[p1|p2?WMIAq1|p2]。
4 结束语
为了对转换系统进行定量研究，本文提出了一种加权模态接口自动机，给出了加权模态接口自动机的定义和精化关系。并且针对合取、析取、并发等逻辑与操作算子给出了SOS语义，并探讨了这些算子关于精化关系的同余性定理，由于篇幅的限制，我们并没有给出证明过程，因此在未来的工作中，我们将给出这些证明过程以及加权模态接口自动机的逻辑特征。
在实际系统中，资源消耗并不局限于权重区间的包含关系，限于篇幅，本文也并未讨论一般情况下的权重区间。在未来的工作中，我们将用近似等价理论来考虑一般情况下的权重区间，并进一步给出相关操作语义，并探讨这些算子关于近似等价关系的同余性问题。
参考文献（References）：
[1] Alfaro L D， Henzinger T A. Interface automata[J]. ACM
SIGSOFT Software Engineering Notes， 2001，26（5）：109-120
[2] Larsen K G， Legay A. Quantitative modal transition systems
[C]//International Workshop on Algebraic Development Techniques. Springer， Berlin， Heidelberg，2012：50-58
[3] G L ?uttgen， Vogler W. Modal Interface Automata. Logical
Methods in Computerence，2012，9（3）
[4] Bujtor F， Fendrich S， Lüttgen G， et al. Nondeterministic
modal interfaces[J]. Theoretical Computer Science，2016，642：24-53
[5] Raclet J B， Badouel E， Benveniste A， et al. A modal
interface theory for component-based design[J]. FundamentaInformaticae，2011，108（1-2）：119-149
[6] Bauer S S， Mayer P， Schroeder A， et al. On weak modal
compatibility， refinement， and the MIO Workbench[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer， Berlin， Heidelberg，2010：175-189
[7] Larsen K G， Nyman U， Wsowski A. Modal I/O automata
for interface and product line theories[C]//European Symposium on Programming.Springer，Berlin，Heidelberg，2007
[8] Bujtor F， Vogler W. ACTL for modal interface automata.
Theoretical ComputerScience，2017，693
[9] Manfred Droste， Paul Gastin， Manfred Droste， et al.
Weighted Automata andWeighted Logics. Handbook of Weighted Automata：175-211（2007）
[10] Juhl L， Larsen K G， Srba J. Modal Transition Systems
with Weight Intervals. TheJournal of Logic and Algebraic Programming，2012，81（4）：408-421
[11] Antonik A， Huth M， Larsen K， et al. 20 Years of Mixed
and Modal Specifications[J]. 2008
[12] K.G. Larsen， B. Thomsen， A modal process logic， in：
Proceedings of the 3rd Annual Symposium on Logic in Computer Science （LICS88）， IEEE Computer Society，1988：203-210
[13] Buchholz P. Bisimulation relations for weighted
automata.Theoretical ComputerScience，2008，393（1-3）：109-123
