手势交互设计中的形式化验证

75理论计算机科学电子笔记43（2001）网址：http://www.elsevier.nl/locate/entcs/volume43.html手势交互设计中的形式化验证G.J. 多尔蒂b，1克。Facontia，1 M.Massinka，1一个C.N.R. Ist. CNUCE，Via Moruzzi 1，I56100，Pisa（比萨），意大利bCLRC，Rutherford Appleton Laboratory，Oxfordshire，U.K.摘要本文展示了如何形式化建模可以用于设计一个动态的手势语言定义的姿势序列。它在不同的抽象层次上讨论了两个模型，处理语言的重要可用性问题，手势识别中的模糊性和重叠。 一种方法，使语言更有弹性的中间构成评估的基础上，定时扩展的模型。一种为混合自动机提供模型检测的工具被用来进行系统的和自动的分析。1介绍许多3D CAD和虚拟现实应用程序需要体现空间深度等概念的用户界面，以便于在三维虚拟空间中导航和操纵对象。传统的二维输入设备不直接支持这些类型的交互。为了更好地满足这些要求，人们开发了三维输入设备，如鼠标、太空球和数据手套。最近，已经开发了基于计算机视觉的技术，以从通过数码相机获取的图像的解释中提取3D信息[4]。对于这类应用程序，我们希望操作人员能够专注于手头的任务，而不是中间输入设备。这要求交互被认为是连续的，并且它根据用户的期望进行操作。旨在通过3D手势交互语言实现这一目标的应用程序在[3]中描述。然而，手势语言的设计提出了几个有趣的可用性问题。其中一些问题已经在[7]中讨论过，其中手势语言的分析是基于形式化的1由欧洲联盟TMR方案下的TACIT研究网络提供部分支助，ERB FMRX CT97 0133号合同。2001年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-N D链接。多赫尔蒂，法康蒂和马辛克76模态动作逻辑是认知理论相互作用认知子系统（ICS）的一部分[1]。该分析研究了反馈延迟、手势之间的相似性以及系统状态的不确定性如何使用户感到困惑。在本文中，我们讨论的手势语言，如[2，3]中所描述的，在三维虚拟空间中的交互。然而，我们提出的分析形式可以应用于更一般的问题，并且也独立于所使用的手势识别技术。事实上，在系统分析中遇到的问题可以在一个抽象层次上处理，这个抽象层次有效地隐藏了可能用于交互的任何特定技术的细节。[3]中提出的接口允许用户通过在动态手定位期间执行的静态姿势和利用静态手定位执行的动态手姿势的序列来执行手势。因此，根据[9]中描述的分类，手势属于SPDL类（静态手部姿势，动态手部位置）或DPSL类（动态手部姿势，静态手部位置）。手势语言的设计形成了形式化建模应用的一个有趣的例子，因为它的有限（但易于扩展）的复杂性和新的方面。我们不打算批评《公约》中提出的措辞。[3]，而是展示了一种可能在这一领域有所帮助的方法界面设计。 有很多问题需要解决设计一个合适的动态手势语言。其中一些纯粹是语言问题，另一些则源于人为因素。语言问题：- 模棱两可。手势语言的问题之一是，当只使用非正式推理时，要确保手势识别中没有歧义并不容易。在[7]中已经表明，在所提出的手势语言[3]中的一种中，存在这样的模糊性，即存在可能导致一次识别多于一个手势的可能的一系列姿势。然而，检测模糊性通常正式的模型和自动验证工具可能有助于发现关键情况。- 重叠。另一个问题是手势之间可能存在一些重叠。这可能导致在识别另一个手势期间对一个手势的部分识别。这样，手势跟随另一手势的识别可能比用户预期的更快地发生，从而导致混淆。人的性能问题：-- Resilience. 一般来说，人类无法以完全相同的方式重复姿势或手势。为了处理这种现象，识别过程允许用户在执行识别的方式上有一定的自由度。多赫尔蒂，法康蒂和马辛克77姿势很明显，当没有多少自由时，相对多的姿势会被解释为一种未定义的姿势。结果是用户难以执行预期功能所需的一系列姿势。另一方面，当存在较大自由度时，部分重叠姿势的概率增加，导致识别中的其它问题。- 准确及时的反馈。准确、清晰和及时的反馈在用户界面中起着重要的作用。特别是当用户和计算系统之间存在紧密耦合时，例如在基于手势识别的交互如[7]中所示，正在识别的手势部分的反馈延迟可能导致混淆和振荡行为。当计算系统的反应看起来不符合用户的期望时，也可能发生关于计算系统正在操作的模式的混淆- 偶然的失误。某些类别的姿势和手势可能比其他类别更容易形成错误或被错误识别。 应确保此类事故不会导致严重后果。这众多的因素可能会使开发一种令人愉快的手势语言变得相当困难。此外，基于手势的界面的可用性通常是后验验证的，即在所有实现工作已经完成并且原型可用之后。在那个阶段找到可用性问题的确切原因可能是非常困难的。首先，因为有很多因素可能导致了这个问题。其次，由于统计方法用于识别姿势和手势，因此重复的实验可能会为每次测试产生不同的结果。第三，因为人的表现有自然的差异如果能找到一种方法来分开分析这些因素，上述问题可能会得到更好的处理。其中一种方法是对手势接口的模型进行分析，集中于孤立的不同方面。其中两个方面是模糊性和重叠。这是我们将在本文中关注的部分。我们使用的建模技术是（混合）自动机，使用不同程度的模型检查工具HyTech [11，12]的功能。这种技术使我们能够描述一个相对简单的自动机模型的手势识别过程，并执行自动和系统的验证手势语言中的歧义和重叠。 我们展示了模型如何有助于手势语言的提高。作为下一步，我们将展示如何使用模型的定时扩展来检查效果当允许手势的指定姿势之间本文仅讨论手势交互的第一个初步模型。我们打算开发扩展的模型，可以考虑到用户和手势识别系统的统计性能，也定时方面的反馈。对这些模型的分析可能会给我们提供有用的线索多赫尔蒂，法康蒂和马辛克78关于系统可用性的问题。这类模型将需要定时和随机建模技术，这些技术最近已经成为协议验证研究的结果。目前的工作可以被看作是迈向更全面的手势交互模型的最终目标的必要的第一步，该模型可以在界面的设计阶段提供有关可用性和性能的信息，因此在构建完整的原型之前。在下一节中，我们将更详细地描述最初提出的手势语言。第3节显示了一个自动机模型和语言的一个子集的分析，说明通过可达性分析的歧义和重叠的检测。第4节讨论了对语言的改进，并给出了完整语言的模型和分析。第五、六节对人的因素的相关问题和进一步研究进行了探讨.第7节得出了一些结论。2动态手势语言在[3]中，描述了用于在3D虚拟空间中导航和操纵虚拟对象的手势语言。该接口使用数据-[15]指关节的位置以约60 Hz的速率记录。手的轨迹是通过随时间内插序列中每个捕获姿势的质心的位置而导出的。应当注意的是，如果手势识别必须实时完成，则手套数据的输入速率对计算机资源的要求特别高，大大超过了目前使用计算机视觉技术的标准设备的可记录速率，其通常不超过每秒14帧本文分析的应用程序允许定义与实际手势识别分离的初始化阶段中的手势语言。在这个阶段，用户向系统“展示”语言中出现的不同姿势。个人姿势的特征被捕捉和记忆。随后，所捕获的姿势可以被组成序列，每个序列定义一个姿势。在此初始化之后，应用程序准备好使用定义的语言进行手势交互用于调整姿势的典型特征是手的方向和手指关节的弯曲值。对于一些动态姿势，运动的轨迹也被指定。当手势语言被指定时，识别由手势识别机执行它的算法通过许多并行过程来运行，每个过程都专门用于识别其中一个手势，这些手势独立地使用传入的数据。当其中一个进程识别出手势时，这会通知应用程序，以便系统可以做出适当的反应多赫尔蒂，法康蒂和马辛克792.1语言所提出的语言包括用于导航、选择和查询对象、缩放、抓取（包括对象的旋转和移动）以及指示退出应用程序的手势。以下描述摘自[3]。导航当识别出“索引”姿势时，应用程序开始执行导航任务。手的旋转会更改3D场景的视点。当姿势被释放时，导航任务结束。“食指”姿势包括第一个只有食指伸展的姿势采摘。在导航过程中，当到达一个对象或一组对象时，可以通过执行姿势“手枪”来选择它们。“手枪式”是由食指和拇指伸展，拇指向上的第一个形成的询问。该任务也可以在导航期间执行。当到达对象时，可以通过执行“Qmark” 姿势 来访 问其 内容 ，该 姿势 也是 手势 的最终 姿势 。 The“Qmark” pose is similar to放大手势开始于手背朝向用户执行的“平坦”姿势。放大发生在手远离用户移动时，缩小发生在手朝向用户移动时。当识别出任何其他手势时，任务结束扣人心弦。当识别出“拳头”姿势时，该手势开始。物体被抓住，并且可以通过闭合的手的旋转或移动来旋转或移动。当“拳头”姿势不再被识别时退出. 离开的手势类似于意大利的告别手势。这包括打开和关闭的手，与手掌的用户的权利，重复两次。图1给出了三个手势的图形表示。缩放出现在图像的第一行，抓取出现在第二行，退出出现在最后一行。“任何”姿势指示手势的结束，并且可以与另一个手势的第一姿势一致。表2.1给出了手势特征的总结2.2反馈用户的手的图形图像被示出为对用户的“真实”手的移动的自然反馈。它反映了手的位置和形状。当手势被识别时，图形手会改变颜色或形状。特定的颜色和形状可能与每个任务相关联。多赫尔蒂，法康蒂和马辛克80图1.一、手势语言中的一些手势;缩放，抓握和退出。2.3手势识别手势识别通过将来自数据手套的输入数据与姿势和手势的指定模型进行匹配来进行。每个手势都有一个相关的过程，试图将数据与模型相匹配。当数据可以与第一个姿势匹配时，该过程变得“活跃”，并试图识别剩余的姿势。当识别出足够数量的姿势时，可以激活相关任务，直到来自手套的数据与姿势的最终姿势相匹配。这些过程跟踪并更新指向当前预期姿势的指针。参数设置被认为是可接受的连续不匹配姿势的最大数量。3歧义和重叠我们将考虑的第一个模型是手势语言的一个子集。我们使用图形化版本的语言HyTech作为单独的自动机模型的缩放，抓地力和退出手势识别过程有关此语言的语法和语义以及用于可达性检查的相关工具的详细信息，请参阅[11，12]。在本节中，我们将在开发手势语言模型时非正式地解释语义。所有这三个被考虑的手势都由两种类型的一系列手部姿势组成：手握和手握。所有其他的手的姿势都被认为是他者。这个简单的模型使我们能够形式化的问题的歧义和重叠，可能会出现在手势语言，以及如何这些问题可以自动检测到的模型检查技术。多赫尔蒂，法康蒂和马辛克81手势姿态模型取向轨迹导航索引;任何任何任何任何任何采摘索引;手枪;任何任何任何任何查询索引;Qmark任何任何任何任何放大平;任何BT、FU任何托乌斯尔任何缩小平;任何BT、FU任何弗罗姆乌斯尔任何夹持拳头;任何任何任何任何任何出口平 ;拳 ;平;拳头BR，FUBR，FUBR，FUBR、FU任何任何任何任何表1手势语言规范概述3.1自动机模型缩放手势在识别到缩放姿势时开始。此姿势可以根据需要持续很长时间，在此期间缩放保持激活状态。当识别出第一个或另一个姿势时，缩放结束如果我们假设这些姿势是由一个戴着数据手套的人生成的，数据手套可以生成关于位置的原始数据，如果所有手指关节以规则的速率（比如60 Hz）运动，并且姿势识别是实时执行的，没有明显的延迟，我们可以将姿势生成建模为一系列规则速率的姿势、第一姿势和其他姿势。随机序列这种类型的行为可以被建模为图2中的自动机手势的行为。这个自动机只有一个位置，这也是它的起始位置，和三个过多赫尔蒂，法康蒂和马辛克82渡。这些转换由姿势和警卫的名称以及对时钟变量t的赋值来标记。HyTech中的时钟以连续的方式自动递增。因此，每当变量t达到值1时，自动机就可以非确定地执行三个转换中的任何一个，生成第一个、第二个或其他姿势。当一个transi-多赫尔蒂，法康蒂和马辛克83出口OOe0Oe1e2e3平拳e4平坦拳头拳头O平平坦坦拳头平坦G3ooog1g2平拳拳抓握平平坦坦拳头Z3平拳平拳OOZ2Z1变焦OConfigvar t：： clock;分析varinit_reginit_reg，， fin_reg，reached：region; init_reg：= loc[Gesture]=h1&loc[Zoom]=z1loc[Grip]==g1loc[Exit]=e0;e0;fin_reg：=loc[Exit]=e4loc[Exit]=e4 loc[Grip]=g2;reachedreached：=reachforwardfrominit_reginit_regendreach;使用reached将trace打印到fin_reg;;执行该操作时，时钟被重置为0，并且自动机从其初始位置开始。转变之后的t的新值由t'指示图二. 手势识别缩放手势的模型由图2中的自动机Zoom给出。这个自动机有三个位置，z1是初始位置。缩放可以在初始位置接受许多第一和其他姿势，而不会变得活跃。然而，当识别出一个缩放姿势时，它会转到下一个位置并激活缩放。只要缩放保持在位置z2，即只要识别出缩放姿势，缩放就保持活动。识别出与自动机不同的姿势（第一个或其他）会导致缩放功能失效，并返回到自动机的初始位置抓握手势在识别出第一姿势时开始，并且在识别出手势或其他姿势之前一直处于活动状态。自动机模型在图2中表示为自动机Grip。退出手势识别的手势有点复杂。在有关手势语言的文献中，可以找到两种不同的版本手势t = 1fist tH1t=1平坦t=1o多赫尔蒂，法康蒂和马辛克84一个是一系列的三个姿势第一，第二，第一，如图1所示，另一个是一系列的四个姿势第二，第一，第二，第一。后者是由图中的自动机出口模拟的。二、3.2达性分析3.2.1歧义这个简单的模型允许我们使用HyTech工具进行第一次分析。由于姿势生成器的模型允许所有可能的姿势系列，包括第一个姿势、第二个姿势和其他姿势，我们可以自动检查在当前模型中是否有可能同时识别两个姿势。缩放在位置z2时被激活，抓握在位置g2时被激活，并且退出在退出自动机到达e4时执行。因此，检查模糊性导致检查是否可能达到以下状态：• z2中的缩放和g2中的夹点，或• zoom在z2，exit在e4，或者• 抓地力是在g2和出口是在e4此分析可通过前向可达性分析来执行，从其中每一自动机处于其初始位置中的状态开始，且检查是否可达到其中两个手势经辨识以由上文所列组合表征的状态。以上列表中的第三种组合的分析在HyTech分析语言中公式化如下：分析var init_reg，fin_reg，reached：region;init_reg：= loc[Gesture]=h1&loc[Zoom]=z1loc[Grip] = g1loc[Exit]=e0t=0;fin_reg：=loc[退出]=e4&int [int n]= nums;reached：= reach forward from init_reg endreach;使用reached将 trace打印到fin_reg该分析生成了一个示例轨迹，表明确实有可能同时识别退出和抓握。表2显示了用户手势的哪个（最短）组合可以导致这种情况。该表在第一列中列出了时间，在给定时间每个自动机的位置向量，时钟t的值以及在最后一列中为达到下一个情况而执行的动作。请注意，下一个情况也可以通过让一段时间过去或通过一个自动机的内部转换来达到。多赫尔蒂，法康蒂和马辛克85在表的最后一行（10）中，我们可以看到状态h1.z 3.g 2.e 4已经到达，这表明Grip位于位置g2，而Exit位于位置e4。还要注意，在轨迹中，缩放已经两次通过其位置z2，指示缩放手势已经被识别两次。这同样适用于夹持手势。步骤时间Loc值t经由00.00h1.z1.g1.e001.00时间单位11.00h1.z1.g1.e01拉瓦21.00h1.z2.g1.e101.00时间单位32.00h1.z2.g1.e11第一42.00h1.z3.g2.e20内部52.00h1.z1.g2.e201.00时间单位63.00h1.z1.g2.e21拉瓦73.00h1.z2.g3.e30内部83.00h1.z2.g1.e301.00时间单位94.00h1.z2.g1.e31第一104.00h1.z3.g2.e40端表2跟踪同时激活的夹持和退出操作3.2.2重叠当姿势具有部分重叠的一系列姿势时，可能发生另一个问题。在这种情况下，一个手势可能被“过早地”识别，这是由于在另一个手势活动的时间期间已经识别了它的一部分的事实。这个问题有点难以正式化。至少我们希望当一个手势完成或激活时，所有其他手势都在其初始位置。这需要为每个手势单独检查。例如，可以验证当Zoom位于位置z3时，其他进程（grip和exit）是否可以位于与其初始进程g1和e0不同的位置。下面的HyTech可达性分析表达式检查当抓握和退出手势都在同时被识别的过程中时，是否可以激活缩放，即缩放在z3中，而抓握或退出不在其初始位置。分析var init_reg，fin_reg，reached：region;init_reg：= loc[Gesture]=h1&多赫尔蒂，法康蒂和马辛克86loc[Zoom]=z1loc[Grip]=g1loc[Exit]= e0t=0;fin_reg：= loc[Zoom]=z3&（~loc[Grip]=g1|int [int n]= nums（int n）;reached：= reach forward from init_reg endreach;使用reached将 trace打印到fin_reg表3中的短迹线表明上述问题很容易发生。轨迹显示，当缩放处于位置z3时，抓握和退出手势都被部分识别。对于“夹点”手势，这不是真正的问题，因为当不再识别“缩放”姿势时，“缩放”操作将隐式结束。然而，对于退出手势，当用户认为他们正在执行一系列缩放和抓握手势时，这可能导致意外的识别。注意，仅仅不存在歧义不足以保证不存在重叠和手势的意外识别步骤时间Loc值t经由00.00h1.z1.g1.e001.00时间单位11.00h1.z1.g1.e01拉瓦21.00h1.z2.g1.e101.00时间单位32.00h1.z2.g1.e11第一42.00h1.z3.g2.e20端迹线表3重叠识别缩放、夹持和退出4改进语言基于上一节描述的简单模型的结果，我们可以得到一些关于如何改进语言的想法。我们在下文中处理歧义和重叠。4.1消除歧义第一个改进是消除Zoom和Exit之间的歧义。在简单的版本中，系统将开始缩放，每当一个摄像头的姿势被认可。原始手势识别器还能够在一定程度上区分手位置的方向。事实上，在手势语言的一个版本中[2]，缩放手势是用手背朝向用户做出的，而退出手势是用手背远离用户或用户右侧的手势多赫尔蒂，法康蒂和马辛克87分析varinit_reginit_reg，， fin_reg，reached：region; init_reg：= loc[Gesture]=h1&loc[Zoom]=z1loc[Grip]==g1loc[Exit]=e0loc[Nloc[Exit]=e0loc[NoZoom]=nzaloc[NooZoom]=nzaloc[NoGrip]=ngaloc[NoExGrip]=ngaloc[NoEx1]=n1a;1]=n1a;fin_reg：= loc[Exit]=e4 loc[Grip]=g2loc[NoZoom]=nzaloc[NoGrip]=ngaloc[NoEx1]=n1a;loc[NoEx1]=n1a;reached：：== reach forward from init_regendreach;使用reached将trace打印到fin_reg;;手势t = 1fist tH1t=1flatBTt=1flatBRt=1o在下面的模型中，如图3所示，我们将用户可以执行的站立姿势细化为站立BT（背对用户的站立姿势）和站立BR（背对右侧的站立姿势）。为了避免具有太多过渡的图片，我们还将姿势识别模型与暗示姿势识别重新开始的姿势集合分开。例如，对于Grip手势，该集合在小型自动机NoGrip中建模，并通过动作ng与Grip同步，该动作ng被迫在遇到意外姿势后立即（尽快）发生。变焦NZZ1NoZoom拳头flatBRflatBTZ2NZNZOflatBTZ3NZaASASAPAPNZNZBASAP抓握ngG1拳头G2拳头ngASAPG3NoGripngangaflatBTflatBRO吴亚亚萨萨NGBConfigvarvart：： clock;出口NE1e0e0拳头拳头ne1ne1flatBRe1NE1flatBR拳头e2flatBR拳头NE1e3flatBR拳头ASAPe4NoEx1flatBTON1N1aaASAPNE1N1N1bb图三. 改进的手势语言：介绍了手势BT和手势BR可以执行如前一部分中所解释的类似分析以检查在该新模型中是否可能同时识别两个手势。不幸的是，情况又是这样。 一个可能的轨迹，说明g2的抓地力和e4的出口可以在同一时间达到的位置是martatBR，第一，martatBR，第一。详见表4.1。当最后一个第一姿势出现时，退出和抓握都会对此姿势做出反应，分别达到e4和g2，从而导致两个姿势都被识别。解决这个问题的一种方法是缩短退出手势，让它由一个退出BR、一个第一和一个最终退出BR组成。模型检验证实，g2和e3确实不能再同时到达。多赫尔蒂，法康蒂和马辛克88步骤时间Loc值t经由00.00h1.z1.g1.e0.nza.nga.n1a01.00时间单位11.00h1.z1.g1.e0.nza.nga.n1a1公司简介21.00h1.z1.g1.e1.nzb.ngb.n1a0NZ31.00h1.z1.g1.e1.nza.ngb.n1a0ng41.00h1.z1.g1.e1.nza.nga.n1a01.00时间单位52.00h1.z1.g1.e1.nza.nga.n1a1第一62.00h1.z1.g2.e2.nzb.nga.n1a0NZ72.00h1.z1.g2.e2.nza.nga.n1a01.00时间单位83.00h1.z1.g2.e2.nza.nga.n1a1公司简介93.00h1.z1.g2.e3.nzb.ngb.n1a0ng103.00h1.z1.g3.e3.nzb.nga.n1a0113.00h1.z1.g1.e3.nzb.nga.n1a0NZ123.00h1.z1.g1.e3.nza.nga.n1a01.00时间单位134.00h1.z1.g1.e3.nza.nga.n1a1第一144.00h1.z1.g2.e4.nzb.nga.n1a0NZ154.00h1.z1.g2.e4.nza.nga.n1a0跟踪结束表4跟踪到最终区域4.2消除重叠和操作意外仍然存在重叠的问题。每次用户想要做出退出手势时，抓握手势也会被识别，并且在完成退出手势之前，他们发现自己正在通过抓握模式。这个问题可以通过要求，如选择和查询，抓取对象只能在导航过程中执行来解决。这在图4中的Grip模型中示出。通过模型检查进行的验证表明，规范现在没有模糊性和重叠。显然，我们还应该检查在消除歧义和重叠之后，仍然可以识别所有手势这可以通过简单的前向可达性搜索来验证，该搜索表明，对于每个手势，可以到达表示手势激活的位置。多赫尔蒂，法康蒂和马辛克89分析varinit_reginit_reg，， fin_reg，reached：region; init_reg：= loc[Gesture]=h1&loc[Zoom]=z1loc[Grip]== g0loc[Exit]=e0loc[NoZe0loc[NoZoom]=nzaloc[NoGrioom]=nzaloc[NoGrip]=ngaloc[NoEx1]=p]=ngaloc[NoEx1]=n1a;n1a;fin_reg：= loc[Grip]=g2&（（~loc[~loc[退出退出]=e0|]=e0|~loc[Zoom]=z1）&loc[NoZoom]=nzaloc[NoZoom]=nza&loc[NoGrip]=nga&lloc[NoEx1]=n1a;oc[NoEx1]=n1a;reached：：== reach forward from init_reg endreach;使用reached将trace打印到fin_reg;;手势t = 1拳头tH1H1t=1 t=1flatBRflatBRflatBTt’=0t=1t=1t=1O指数t’=0Configvar t：： clock;变焦NZZ1flatBTz2NZZ3flatBTASAPNoZoom拳头指数指数平台BROOASAPASAPnzanz抓握ngng指数indexg1fistg2ngffiigggssg0tt00indexg3拳头ASAPNoGripflatBTflatBRO雅雅亚萨湾ng出口ne1ne1asape0e0ne1e1e2e3NE1flatBRflatBRfistflatBR flatBRfist拳拳平BRNoEx1flatBT指数ON1aN1aASAPN1BN1BNE1NE1NE1图四、改进的手势语言：没有重叠和歧义4.3完成模型原始的手势语言也有用于导航、选择和查询的手势。我们可以将他们的手势模型添加到规范中。由于查询和选择都只需要在导航期间发生，因此它们的模型可以合并为一个。必须将两个新姿势添加到用户可以执行的姿势集合中，并且必须调整其他模型，以便它们正确地处理这些新姿势。完整的模型如图所示。五、用于检测歧义和重叠手势的相同分析可以如在先前部分中那样执行。表5中的结果表明，图5中所示的规范中没有留下歧义。括号中的数字表示HyTech产生结果所用的时间。时间以秒为单位报告。表6显示缩放和导航可能存在重叠在第一种情况下，（a）当缩放被激活时，夹持可以在位置g3，但这意味着只有缩放是激活的，夹持已经完成并将毫无延迟地到达其初始位置。表7中显示了说明这一点的轨迹。在第二种情况（b）中，每当识别出索引姿势时，导航开始，但它也形成抓握姿势的第一个姿势。在这种情况下，不存在意外行为的风险，因为Grip与查询一样，多赫尔蒂，法康蒂和马辛克90NoGrip手枪qmarkqmarkflatBTflatBRflatBROOnganga吴亚亚NGBNZB分析varinit_reginit_reg，， fin_reg，reached：region; init_reg：= loc[Gesture]=h1&loc[Zoom]=z1loc[Grip]== g0loc[Exit]=e0loc[Navie0loc[Navigate]=n1loc[NoZoogate]=n1loc[NoZoom]=nzaloc[NoGrip]=m]=nzaloc[NoGrip]=ngaloc[NoEx1]=n1angaloc[NoEx1]=n1aloc[NoNav]=nn1;loc[NoNav]=nn1;fin_reg ： =loc[Zoom]=z2loc[Navigate]=n3loc[NoZoom]=nzaloc[NoGrip]=ngaloc[loc[NoGrip]=ngaloc[NoEx1]=n1aloc[NoNav]=nn1;NoEx1]=n1aloc[NoNav]=nn1;reached：：== reach forwardfromfrom init_reg endreach;使用reached将trace打印到fin_reg;;手势t=1手枪t=1flatflatBRBRt=1t=1t = 1fist tHH11t=1flatBTt=1O指数t’=0t=1Configvar t：： clock;变焦NZZ1flatBTZ2NZflatBTASAPZ3NoZoomqmarkqmarkqmark手枪手枪拳指数指数flatBRflatBRoASAPASAP恩扎新兹抓握ngffiigggssg0tt00ng指数ASAPG1首索引G2拳头ng指数G3出口NE1e0e0NENE11e1e2e2ASAPe3NE1flatBR拳flatBRflatBR拳拳拳flatBRNoEx1N1N1aa手 枪手 枪qmarkqmarkflat指数指数OASAPN1N1bb尽快导航nn指数指数NN手枪手枪N1N1指数N2N2qmarkASAPNoNav拳头flatBRflatBTO亚洲新闻社qmarkqmarkN3N3手枪手枪N4N4NNNN11NN2NN2图五. 完整的手势语言选择是应该在导航期间发生的操作。表8中显示了说明这一点的轨迹。缩放z2G2手柄E3出口查询n3选择n4缩放z2–否（4.92）否（4.83）否（4.97）否（4.97）G2手柄–否（4.95）否（4.98）否（4.97）E3出口–否（5.01）否（5.03）查询n3–否（4.96）选择n4–表5多赫尔蒂，法康蒂和马辛克91分析检测歧义此外，对于完整的语言，可以示出每个手势可以是多赫尔蒂，法康蒂和马辛克92变焦抓握出口 查询选择缩放z2–g3（a）e0N1N1G2手柄Z1–e0N1N1E3出口Z1G0–N1N1查询n3Z1G0e0––选择n4Z1G0e0––导航n2Z1g1（b）e0––表6分析检测重叠时间Loc值t经由0.00h1.z1.g0.e0.nza.nga.n1a.n1.nn11指数0.00h1.z1.g1.e0.nzb.nga.n1b.n2.nn10NZ0.00h1.z1.g1.e0.nza.nga.n1b.n2.nn10NE10.00h1.z1.g1.e0.nza.nga.n1a.n2.nn101.00时间单位1.00h1.z1.g1.e0.nza.nga.n1a.n2.nn11第一1.00h1.z1.g2.e0.nzb.nga.n1a.n2.nn20NZ1.00h1.z1.g2.e0.nza.nga.n1a.n2.nn20NN1.00h1.z1.g2.e0.nza.nga.n1a.n1.nn101.00时间单位2.00h1.z1.g2.e0.nza.nga.n1a.n1.nn11公司简介2.00h1.z2.g2.e0.nza.ngb.n1b.n1.nn20NE12.00h1.z2.g2.e0.nza.ngb.n1a.n1.nn20NN2.00h1.z2.g2.e0.nza.ngb.n1a.n1.nn10ng2.00h1.z2.g3.e0.nza.nga.n1a.n1.nn10端迹线表7显示缩放重叠的迹线（表6中的使用前向可达性分析激活。通过将Grip与Navigate自动机相结合，可以进一步改进语言模型，以便更清楚地表明，抓取、选择和查询这三个操作只能在导航期间执行。多赫尔蒂，法康蒂和马辛克93时间Loc值t经由0.00h1.z1.g0.e0.nza.nga.n1a.n1.nn11指数0.00h1.z1.g1.e0.nzb.nga.n1b.n2.nn10NZ0.00h1.z1.g1.e0.nza.nga.n1b.n2.nn10NE10.00h1.z1.g1.e0.nza.nga.n1a.n2.nn10端迹线表8显示Grip和导航之间重叠的轨迹（表6中的5人为因素在前面的部分中，我们已经展示了如何使用简单的自动机模型来检测语言相关的属性，例如歧义和重叠识别。在本节中，我们将更多地关注人的因素方面及其对语言可用性的影响5.1恢复到中间姿势一般来说，人类无法以完全相同的方式表演一个姿势超过一次。为了处理这种现象，以允许用户在形成姿势时具有一定自由度的方式来识别姿势。很明显，当这个自由度非常小时，相对多的姿势将被解释为“其他”，即被解释为未识别的姿势。结果是用户难以执行预期功能所需的一系列姿势。这可以通过添加由人类做出的典型姿势的模型来说明，该模型由一些可识别的姿势和许多“其他”姿势组成。在图1中示出了对执行抓握手势6在标有“用户”的框可达性分析表明，即使满足了语言相关的要求，人类在原始语言中做出建模手势也不会获得预期的结果。处理这个问题的一种方法是使语言对中间姿势更具弹性。但在这样做的时候，我们想知道这种变化对语言识别可靠性的影响。这对于获得有关不同识别策略的性能的第一个指标特别有用。我们可以做的一个假设是，大多数非预期的姿势不会保持很长时间，因此几乎总是会导致识别出“其他”姿势，即与语言的任何预定义的内涵姿势不一致的姿势。如果这是关于用户行为和姿势识别的有效假设，那么我们可以通过在每两个“真实”姿势之间允许“其他”姿势一定量的时间来放松对姿势识别的要求如果该系列多赫尔蒂，法康蒂和马辛克94当在图6中，给出了可以如何对姿势中的一系列“其他”姿势的接受进行建模的示例在用户姿势的模型中使用时钟d来对用户执行的中间“其他”姿势的持续时间进行时钟w定义了手势识别过程可以接受“其他”姿势的最大时间量。 如果我们将该时钟约束为最大5个时间单位，则由图6中所示的自动机User建模的用户手势导致对抓握手势的识别。如果时间约束减少到一个时间单位，则不再识别夹持手势。这可以通过从初始状态开始的可达性分析来自动验证，并寻找其中识别抓握手势的状态（即，处于状态g2的抓握）。抓握ngffiigggssg0tt000ng指数ASAPG1首索引指数g2ngG3拳头NoGrip手枪qmarkqmarkflatBTflatBTw 1flatBRow=1w=1阿萨普阿萨普岛岛ngangangw '= 0NGBww =1=1用户指数DD =2=2u1u1d=2oODD =2=2u2索引d=2d=2o拳头拳头u3u3d=2图六、抓握手势接受当然，应该表明，修改后的语言不包含歧义或重叠问题。这一点可以用与我们对图1所示的版本所做的五、6进一步分析还有许多其他的问题，可以回答以下基于模型的设计手势交互。我们在下文中提到其中一些，但本文不作详细这是未来工作的主题。行动失误的后果。在某些情况下，当识别手势时，可以接受一些连续的相似但错误的姿势。这可以在退出手势的情况下工作，避免意外进入缩放模式。在导航和查询的情况下，这将是不太合适的，因为意外的Qmark姿势不太可能只持续很短的时间。另一方面，查询功能不会导致严重的模式意外，用户可以轻松地恢复