理论计算机科学电子笔记253（2009）87-99www.elsevier.com/locate/entcs用DNNF图安妮卡·舒曼1马丁·萨肯巴赫2InstitutfuürIformatikTechnischeeUniversittaütMuünchen85748Garching，Germany黄金波3澳大利亚国家信息通信技术大学和澳大利亚国立大学堪培拉，澳大利亚摘要测试的目标是通过应用输入模式并根据观察到的输出验证或证伪假设，来区分关于系统的许多假设（例如，不同的故障诊断）。最佳区分测试（ODTs）是那些最有可能区分非确定性系统假设的输入模式。 找到ODT实际上是重要的，但它通常相当于确定模型计数的比率，因此计算非常昂贵。在本文中，我们提出了一种新的方法来解决这个问题，它使用系统的结构特性来限制计算ODTs的复杂性。 我们首先通过编译成可分解的否定范式来构建测试问题的紧凑图形表示。基于此编译表示，我们展示了如何在线性时间内评估区分测试，这使我们能够有效地确定ODT。从一个真实世界的应用程序的实验结果表明，我们的方法可以计算的实例，以前的方法是棘手的ODT。保留字：测试，DNNF图，模型计数。1引言测试询问是否可以用输入模式刺激系统，以便可以根据观察到的1电子邮件：anika. in.tum.de2电子邮件：sachenba@in.tum.de3电子邮件：jinbo. nicta.com.au1571-0661© 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.05388A. Schumann等人/理论计算机科学电子笔记253（2009）87输出模式。应用包括基于模型的技术系统故障分析，自主控制（获取传感器输入以区分竞争状态估计）和生物信息学（设计实验，帮助区分生物现象的不同可能解释）。在许多真实世界的测试应用中，底层模型是不确定的;应用一个输入可能会导致几个可能的输出。不同的概念，测试与这种非确定性的模型已经推出。在诊断领域，[11]为作为约束建模的系统引入了明确的和可能的区分测试（DDT和PDT）。对于DDT，可能的输出的集合是不相交的，因此它将必然在假设之间进行区分，而对于PDT，集合部分重叠，因此它可以或可以不在假设之间进行区分。在自动机理论中，[1]研究了非确定有限状态的强弱可区别序列机器;对于长度至多为k∈N的序列，这可以归结为问题[16]《明史》：“德者，德也，德也。 [7]引入了最佳区分测试（ODTs），其通过最大化区分与非区分可能结果的比率来概括DDT和PDT。找到ODT非常重要，因为它减少了要执行的测试数量和测试过程的总体成本。[7]提出并分析了一种简单的近似ODTs的贪婪型算法，该算法在实际应用中产生的测试输入的区分比接近ODTs。在本文中，我们提出了一种新的搜索算法来计算ODTs（从而DDTs和PDT），它利用模型的结构特性来限制最佳测试生成的复杂性。它的主要特征是一个精心构造的图-通过操作逻辑理论和编译成可分解的否定范式（DNNF）[5]-允许有效计算模型计数比率这些上界用于以最近的规划算法[8]激励的方式修剪我们表明，我们的方法可以计算ODTs的实例是棘手的以前的方法。2背景遵循[7，10，11]中的框架，我们假设系统可以建模为约束满足问题（CSP），它是一个三元组M=（V，D，C），其中D=D（v1）×... ×D（v n）是有限个变量v j∈ V的有限域，j= 1，.，n，并且C={C1，.，Cm}是约束的有限集合，其中C i≠ D，i =1，. ，m. 我们用X表示所有解的集合，也就是说，变量，以满足所有约束条件。也就是说，X ={x|x∈D，C（x）}，其中C（x）d∈x∈Ci，对于所有i=1， . . ，m.此外，所研究的系统定义了一组可控（输入）变量I和一组可观测（输出）变量O。形式上，一个系统的假设M是一个CSP，它的变量被划分为V = I <$O<$L，使得I和O是系统的输入和输出变量，并且对于所有对I的赋值，CSP是满意的。其余变量L=V\（I O）A. Schumann等人/理论计算机科学电子笔记253（2009）8789称为内部状态变量。 我们用D（I）和D（O）表示输入和输出两个变量之间的正交积，即D（I）=×v∈ID（v）和D（O）=×v∈OD（v）.测试的目标是找到输入变量I的赋值，对于不同的假设，导致输出变量O的不同分配。 在在非确定性系统的一般情况下，一个输入分配可以产生多个可能的输出分配。这种情况在实践中很常见;一个原因是为了减小模型的大小，通常将系统变量的域聚合成诸如“低”、“中”和“高”之类的小值集合另一个原因是测试情况本身：即使在汽车测试台这样的刚性环境中，在测试设备时也不可避免地存在无法完全控制的变量或参数。为了捕获输出集，对于给定的假设M和输入变量的赋值t∈ D（I），我们定义输出函数X：D（I）→2D（O）w itt→{y|y∈D（O），nx∈X：x[I]=tnx[O]=y}，其中2D（O）d不表示D（O）的幂次，且x[I]，x[O]d不表示向量x分别对输入变量I和输出变量O的幂次. 注意，由于M总是产生输出，因此X（t）是非空的。2.1鉴别试验非确定性模型已经引起了所谓的可能和明确区分测试的引入，分别简称PDT和DDT[11]。 第一种类型的检验（PDT）可能会区分假设，因为可能的输出集部分重叠，而第二种类型（DDT）必须这样做，因为可能的输出集是分离的：定义2.1（区分检验）考虑k ∈ N个假设M1，. ，Mk，其中输入变量I和输出变量O。设Xi是假设M i的输出函数，其中i∈{1，.，k}。 一个赋值t∈D（I）到I是一个可能可区别检验（PDT），如果存在i∈{1，.，k}，使得Xi（t）| j/=iXj（t）=iA∈D（I）是一个可定义的离散元test（DDT），如果对于所有i∈ {1，...，k}，则Xi（t）\jiXj（t）= Xi（t）。对于使用非确定性自动机模型而不是逻辑理论或CSP进行测试，存在所谓的弱区分和强区分的类似概念。ing序列[1，3]。 求长度为某个k∈N的序列通过展开自动机，使用自动机的转换和观察关系的k个因此，在本文中，我们将自己限制为有限域约束网络的模型。90A. Schumann等人/理论计算机科学电子笔记253（2009）87A2H：i1i2o1AJ：i1i2o12小时L L L LL LL H H L HH L H H H H H H HNOT：i1uAUL：uo1o2AJ：uo1o2ULLHLLLLLLHLLHLLHLHLLHLLHLHHHLHHHFig. 1. 有两个可能出错的加法器的电路：AJ和AJ。2.2最佳区分测验2H UL由于有限的可观察性或高度的非决定性，假设的DDT不存在，人们只能找到PDT，这并不罕见。这激发了一种定量测量方法，用于对先前的PDT和DDT概念进行细化和概括。直觉是，如果我们假设可能的结果（对输出变量的可行分配）是（大致）相等的可能性，则与另一个PDT相比，PDT将更有可能区分两个给定的假设，如果假设唯一的可能结果与所有可能结果的比率更高。在[7]中引入的最佳区分检验的概念正式确定了这个目标，即找到尽可能好地区分两个假设的定义2.2（区分比）给定两个假设M1，M2的测试输入t∈ D（I），输入变量为I，输出变量为O，我们将Γ（t）定义为区分假设与所有假设的可行输出之比。可行产出：r（t）：= |X1（t）X2（t）|− |X1（t）X2（t）||X1 (t) ∪ X2 (t)|Γ是测试质量的度量，它细化了PDT和DDT的概念：如果Γ 为0，则检验根本不区分，因为两个假设导致相同的观察结果（输出模式）。如果该值为1，则检验是DDT，因为假设总是导致不同的观察结果。如果该值介于0和1之间，则该测试是PDT（可能的观测值中存在一些非重叠注意，Γ是良好定义的，因为对于任何选定的t∈ D（I），集合X1（t）和X2（t）非空。最佳区分测验是具有最大区分率的测验.图1显示了一个由三个组件组成的示例：一个非组件和两个加法器：A2H和AUL。前者在接收输入i2=H时是高主导的，而后者在接收输入u=L时是低主导的。在这里，我们考虑的假设，要么两个加法器功能正常，即。M1={NOT，A2H，AUL}或两个加法器都有故障，即M2={NOT，AJ，AJ}.2H UL这个例子有两个PDT：[−i1，i2]和[−i1，−i2]，它们具有以下特性：A. Schumann等人/理论计算机科学电子笔记253（2009）8791区分比例：Γ（[−i1，i2]）=|{o1，o2}，{o1，−o2}，{−o1，o2}|=3and|4|4Γ（[−i1，−i2]）=|{−o1，o2}|=1。|2|2因此，输入[−i1，i2]在本例中是一个ODT。2.3确定性DNNF我们简要回顾了命题理论的基于图的表示一个命题理论f是否定范式（NNF）[5]，如果它只使用合取（and，（或，或变量一个NNF是可分解的（DNNF），如果每个合取的合取没有共享变量。DNNF是确定性的（d-DNNF），如果每个析取的析取是成对逻辑不一致的。一个d-DNNF是光滑的，如果每个或节点的析取提到相同的变量集在本文的其余部分，我们还假设逻辑理论的每个变量都出现在光滑的d-DNNF图中（这总是可以在多项式时间内确保[5]）。图2示出了表示图1所示示例的PDT集合的平滑d-DNNF图。d-DNNF图可以使用公开可用的C2 D编译器[4]以合取范式（CNF）为命题理论生成。这个操作的复杂性是多项式的变量的数量和指数的最坏情况下，只有在树的系统的宽度。此外，给定DNNF图G，可以在线性时间内计算其在变量集上的投影。因此，在不影响计算时间的情况下，我们假设M1和M2仅定义在输入和输出变量上。基于光滑的d-DNNF图G，可以在线性时间内计算与对d-DNNF变量的部分分配X一致的模型的数量。这是因为G中的每个模型都由满足以下性质的子图Gs表示：（i）Gs中的每个OR节点都恰好有一个孩子，（ii）Gs中的每个AND节点都有与G中相同的孩子，（iii）Gs与G具有相同的根。FIG。 二、最小化d-DNNFgaphrenting<$i1n（i2n<$i2）。“A“和“O“分别表示一个n A n d和一个n O r节点。非叶子节点中的数字是它们的标识符。例如，对于图2中的图，模型[−i1，−i2]由具有节点A1，O 2，−i1，−i2的子图表示。尽管如此，我们将用这些性质作为m-子图。我们将只满足前两个性质的图记为s-子图。进一步我们说一个子图GS被标号为文字l，如果GS有一个叶节点l。然后，关于X的模型计数包括计算92A. Schumann等人/理论计算机科学电子笔记253（2009）87我：算法1关于实例化X的模型计数8> 如果N是与X一致的叶节点，则为1><0，如果N是与XΛ（N）=PW>Λ（N）ifN =N>>QiViiΛ（Ni）如果N=INim-子图，由X中的文字标记。这通过如算法1所示的图的自底向上遍历来完成。每个节点N的Λ（N）值表示以N为根的s-子图的数目，其标签与X一致。因此，图的根的Λ（N）值表示一致模型的总数。3使用DNNF进行在本节中，我们将展示如何将ODT问题表示为单个DNNF图，从而获得直接利用系统结构实现紧凑性的表示。此外，我们描述了如何修改第2.3节中描述的模型计数算法，以确定任何完整实例化测试向量（CITV）的精确后者允许对ODT的有效搜索，而无需计算所有测试向量的Γ值。在某些情况下，根据DNNF图的结构，可以直接确定ODT而无需搜索。3.1将ODT问题编码为单个DNNF我们现在描述如何将ODT问题表示为单个d-DNNF图GJ。 由于该图的大小影响ODT计算的效率，因此我们还将展示如何通过考虑以下因素来减小GJ的大小：我们只对测试向量的模型计数感兴趣，而不是实际的意见。我们将证明，如果我们在模型通过投影丢失之前计算模型的数量，则GJ一个图，在其基础上可以计算区分比Γ，需要表示假设M1和M2。 这两个假设可以用一个形式为M1<$M2的图来编码。此外，我们还需要区分现代的观点认为，这一点是不可能实现的，即，则P D T O <$=（M1< $M2）<$$>（M1<$M2），以及不满足P D T O <$=（M1 <$M2）的情况。 我们通过引入一个额外的变量d和标记表示模型的每个m-子图来做到这一点与带有文字-d的分子一致，并将文字d添加到剩余的m-子图中。因此，GJ的定义如下：GJ=（fP DTO<$$>d）（M1<$M2<$d）如第2.3小节所述，可以使用可用的C2 D编译器基于M1和M2图3描绘>我A. Schumann等人/理论计算机科学电子笔记253（2009）87932对于我们的例子，这个图Gj，基于它我们可以计算任何CITV的区分率。例如，为了计算Γ（[−i1，−i2]），我们计算由−i1，−i2和−d标记的m-子图的数量以获得Γ的分子在这个例子中，只有一个这样的m-子图由额外的节点组成：A1，O 2，A 4，O 6，A 8，−o1和o2。 为了得到Γ的分母，我们需要计算符合M1<$M2的模型的个数（见定义2.2），也就是说，模型的分母等于fPDTO<$（M1<$M2）。他说，“我的心是空的，由−i1，−i2和−d标记的m-子图的个数以及由-i1，-i2和d。对于我们的例子，只有一个子图被标记为后者，即由附加节点组成的子图：A1，O 2，A 4，O 6，A 9，-o1，和-O2。因此，我们得到Γ（[−i1，−i2]）=1，如2.2节所示。请注意，由于图G形式上，基于G'的Γ（t）|GJ (t ∧ ¬d)|r（t）：= |GJ（td）|+的|GJ（td）|为|GJ(t ∧¬d)||GJ(t)|哪里|G J（X）|表示实例化X下的模型计数。因此，我们可以使用算法1计算任何CITV的区分比。G1GJG2图三.图1所示示例的曲线图G节点N的底标号是指它的局部值：αN/βN。 IgraphG1thebottomlabel表示Algorithm2在t=[−i1，−i2]运行时所生成的估计值，并且在G2中，该估计值表示Algorithm3在实例化为 真时所生成的估计值。我们现在描述如何从GJ中提取非输入变量，而不会丢失与ODT问题相关的这是通过首先计算节点94A. Schumann等人/理论计算机科学电子笔记253（2009）87Ni的最小值G=NI（GJ），并通过计算G j中的最小值而不是G中的最小值，得到了Ni的最小值. 节点集NI由具有输入变量作为后代的那些节点组成。对于图3中的图G形式上，一个节点N∈N在NIi中：• N是由输入变量标记的叶子，或者• N在NI中有一个孩子。为了计数在GJ中但不在G中的s-子图，我们将GJ中每个OR和AN D节点的子图的集合划分为属于NI的子图，即，NJ={Ni|Ni∈NI}和所有的这些都不存在，i. e. ，NH={Ni|Ni∈/NI}。对于这些节点，算法1的计数过程可以被细化如下：⎧ΣΣhΛ（Nh）+ jΛ（Nj），如果N=INiΛ（N）=⎩hΛ（Nh）·jΛ（Nj），如果N=INi其中，对于y={h，j}和N，Y=N，我们定义yΛ（Ny）= 1。Σ关键在于，局部计数值γN=hΛ（Nh）（resp.γN=hΛ（Nh））在计算不同t的模型计数时不会改变。这是因为以Nh为根的s-子图没有被任何输入变量标记，因此与任何测试向量一致。因此，对每个节点只计算一次这些值就更精确地说，我们用αN（分别）标记每个非叶节点NβN），表示分子的局部计数值（分别（1）、（2）、（3）。 通过运行算法1的改进版本获得αN，到实例化<$d并且对于βN，我们相对于实例化真来计数模型，即，对于所有叶子，Λ（N）= 1。图3中的图G3.2基于DNNF图G的Γ（t）计算为了计算区分比，我们使用G中OR节点的αN和βN值必然为0的事实。这是因为GJ是光滑的，这意味着所有以N为根的s-子图都用相同的变量标记因此，这些变量中的任一个是输入变量，在这种情况下，对于N的所有子节点，局部计数为0，或者这些变量中没有一个是输入变量，在这种情况下，OR节点本身不在G中。 因此，区分比率可以是如算法2所示计算。 它是从根的值获得的，在定理3.1中正式表述。图3的G1的底部标签示出了t= [−i1，−i2]的Λα和Λβ定理3.1（测试评估）设G是光滑DNNF图G的根节点。则对于输入变量的任何完全实例化t，Γ（t）= Γ（G，t）。⎪⎪A. Schumann等人/理论计算机科学电子笔记253（2009）8795算法2关于实例化t的对于与t一致的叶N，我们设置对于与t不一致的叶N，我们设置Λα（N）= Λβ（N）= 1Λ α（N）= Λ β（N）= 0。对于剩余的节点，我们计算：8个P（Λα（N），Λβ（N））=> （iΛα（Ni），> PQWINi> （αN·：iΛα（Ni），Q VβNiΛβ（Ni））如果N=iNi然后我们计算每个节点的区分比：（Γ（N，t）=0，如果Λβ（N）= 0Λα（N）Λβ（N） 否则3.3部分测试向量虽然区分比的计算也可以基于两个单独的DNNF图来完成，但我们现在展示这个单一的图对于我们的新方法是如何必不可少的，该新方法用于基于a PITVtp.我们首先指出，算法2也准确地检索G的与t一致的子图。4因此，Γ（t现在我们将展示如何计算PITV t p的子图，其Γ值必然是tp的每个完成的上界。这个子图GS是由一组s-子图组成的，其中哪些应该包含在GS中的问题转化为OR节点的哪些孩子应该包含的问题。对于这样的节点N，儿童N1，... Nj定义为：Γ（N，t）= Λ α（N1）+ Λ α（N2）·· ·+ Λ α（Nj）.pΛβ（N1）+ Λβ（N2）···+ Λβ（Nj）因此，Γ（N，tp）不能大于其“最佳”子节点的Γ值，即，具有最高区分率的孩子。这是因为，对于x=a1+b1anda1≤b1 且a1≤a2·b1我们有a2+B2a2b2a2·b1+b1B2a2·b1+b1·b2b1·（a2+b2）b1x≤b2=a2+B2b2·（a2+b2）==。b2·（a2+b2）b2因为如果x的分子和分母有更多的[4]这个图由根和所有节点N组成，其中Λ β（N）>0，并且至少有一个父节点NP满足Λ β（NP）> 0。>>96A. Schumann等人/理论计算机科学电子笔记253（2009）87p我βip><比两个被加数，我们有Γ（N，t）≤ max Λα（Ni）.iΛβ（Ni）因此，我们可以通过将每个OR节点的值设置为其“最佳”子节点的值并通过计算其他节点的值来获得Γ（N，tp自然，上界越紧，对ODT的搜索将越有效。 为此，我们在子图中只包括那些形式上，节点N由tp设置，即，set（N，tp）= 1，i• N是一个叶节点，其变量由tp或• N是AND或OR节点，使得对于所有子节点N i，我们设置（N i，t p）= 1。例如，对于图3所示的图G1的节点O2，我们设置（O2， [−i2]）= 1和设置（O2，[−i1]）= 0。由tp设置的OR节点的每个子节点必然是与TP的完整实例化一致或不一致，而不管TP如何完成。因此，我们可以像算法2中那样计算这些OR节点的区分比，并且仍然保证Γ（N，tp）是每个节点N的上界。注意，由于G是光滑的，OR节点的所有一致子节点都必须具有相同的集合值，因此它们的Λα和Λβ值要么都是最大化的结果，要么都是求和的结果。算法3关于实例化tp的上界W对于OR节点，N=我们计算：8个P> （iΛα（Ni），>PΛ（N）），如果set（N，t）= 1（Λα（N），Λβ（N））=>（Λα（Nm））的情况下，如果set（N，tp）= 0且>： Λ（N））Γ（N，t）= max Γ（N，t）βmm第一节p对于其余节点，计算与算法2中相同。区分比Γ（N，tp）也如算法2中那样计算。进一步注意，我们对值函数使用了与算法2中相同的名称。原因是算法2现在可以被视为算法3的特殊情况，其中t是测试向量的完整实例化，因此对于所有OR节点，set函数返回true。 正是在这种情况下，计算的值被保证是精确的，如以下定理中正式陈述的：定理3.2（上界）设tp是PITV，G是光滑DNNF图G的根结点.则对于tp中自由变量的任意完全实例t，Γ（t）≤ Γ（G，tp）.>A. Schumann等人/理论计算机科学电子笔记253（2009）87973.4ODT计算利用DNNF图G和线性时间算法计算CITV的精确区分率和PITV的上界，我们得到了我们的ODT搜索方法的基础。这包括一个分支定界搜索，输入变量。我们迭代地设置输入变量，直到所有变量都被设置并且获得精确的区分比，或者直到PITV的上限低于先前计算的CITV的Γ值。有趣的是，如果G具有一定的结构，我们可以在不搜索的情况下获得ODT通过利用以下事实：（i）我们可以通过相对于实例化真运行算法3来计算ODT的区分比的上界ΓUB，以及（ii）恰好存在一个与所得子图GS一致的测试向量t。后者是由于图G是可分解的。现在，由于我们可以使用算法2计算Γ（t），我们可以确定一个线性时间内的ODT，如以下定理所述：定理3.3设t是与子图GS一致的测试向量，该子图GS是通过计算关于实例真的区分比而得到的。t是可以在线性时间内计算的ODT，如果Γ（t）= Γ（GS）。对于我们的例子，这个定理的条件成立，因此我们可以不需要搜索就得到ODTt= [−i1，i2]（参见图3的G2）。注意，如果G是确定性的，则该定理的条件总是成立。不幸的是，只有图G从可观察变量中抽象出来，并不能保持决定论。为了确保确定性，我们需要重新编译G，但这可能会改变它的结构完整。这将导致局部计数值的丢失，从而导致我们从该图计算区分比率的能力。4实验评价我们在汽车发动机试验台的模型上评估了基于DNNF的测试方法[9]，该试验台由三个主要部件组成：发动机、管道和节气门。目标是通过分配三到四个可控变量和观察三到四个可测量变量来找到管道中的泄漏通过对原始混合离散-连续模型应用不同的抽象，并使用从CSP到SAT的直接编码，该问题已被转化为不同大小的离散实例集[12]。表1显示了计算ODT和DDT的实验结果。对于每个实例，我们报告计算的DNNF图的大小（节点数），以及在具有1GB RAM的Linux双核PC上的计算时间（以秒为单位）。对于具有DDT的实例，我们将我们的方法与基于量化布尔公式和QBF求解器sKizzo [2]的最新专业DDT方法[10]进行了比较。 这种方法能够解决实例1b-3b，剩下的记忆。相比之下，我们的ODT方法也可以解决实例4 b-6 b。98A. Schumann等人/理论计算机科学电子笔记253（2009）87Inst.节点数时间1a580.042a1030.063a1610.094a2050.105a3290.206a2450.217a3620.408a47665.419a265436.610a65063414Inst.节点数时间1b660.062b1240.073b1910.104b486514.75b482383966b10281715667b––8b––9b––10b––表1ODT（左）和DDT（右）计算结果我们的方法是第一个计算精确ODT的方法;因此我们无法比较它直接与以前的方法。然而，我们使用[7]的贪婪算法来计算相同问题实例的近似解。该算法只能解决实例1a-7a;也就是说，对于实例8a-10a，5结论和未来工作最优区分测试推广并细化了非确定性系统的可能和确定区分以及强和弱测试由于计算ODT在计算上可能非常昂贵，因此先前的工作集中在近似解决方案上。我们提出了一种新的方法来计算精确的ODT的基础上编译的ODT问题到DNNF和计算上限修剪系统搜索的创新方法。实验结果表明，该方法能够计算的实例，太大的以前的方法的ODTs和DDTs。未来的工作可能包括扩展这种方法，以找到最小成本的测试，或可能的输出模式不能被假设为同样可能的情况。引用[1] R. 巴尔角 Courcoubetis和M. 扬纳卡基斯非确定性和概率性机器的区分测试。 在procACM Symposium on Theory of Computing，第363-372页， 1995 年 。[2] M.贝内德蒂 skizzo：用于评估和认证QBF的套件。 在Proc. CADE-05，2005中。A. Schumann等人/理论计算机科学电子笔记253（2009）8799[3] S. Boroday，A. Petrenko和R.格罗兹模型检查器可以为非确定性系统生成测试吗？电机股份注意Theor。比较科学，190：3[4] A.达维奇c2d编译器用户手册。技术报告，Comp. Sci.加州大学洛杉矶分校，2005年。[5] A. Darwiche和P. Marquis。知识汇总图。《人工智能研究杂志》，17：229[6] M. Esser和P. Struss。基于故障模型的嵌入式软件测试生成。在Proc. IJCAI-07，第342-347页[7] S. Heinz和M.萨肯巴赫使用模型计数来寻找最佳区分测试。ZIB Report 08-32，Zuse Institute Berlin，2008。[8] J. Huang.结合知识编译与搜寻之符合机率规划。在Proc. ICAPS-06，第253-262页[9] J. Luo，K.帕蒂帕蒂湖Qiao和S.千草汽车发动机控制系统的综合诊断开发过程。IEEE Trans. on Systems，Man，and Cybernetics，37（6）：1163-1173，2007.[10] M. Sachenbacher和S.施温使用量化的CSP进行基于模型的测试。 在ECAI-08基于模型的系统研讨会，2008年。[11]P. Struss测试物理系统。AAAI-94，第251-256页[12] T.沃尔什SAT与CSP。在CP-00的Proc.，441-456页
我的内容管理
展开
