Anil Nerode的混合系统控制金宝博官方

卢克·穆罕沃斯： 在nerode（2007），你告诉混合系统控制的原点故事。金宝博官方Pacifica的1990年DARPA会议似乎是特别精明的。当你描述它时：

会议的目的是探讨如何清除一个主要的瓶颈，控制大型军事系统，如防空空间中的航空军。金宝博官方

您可以更详细地描述DARPA对该会议的长期目标似乎是什么？据推测，他们希望该会议将促使新的研究线允许他们在未来5 - 20年内解决特定的控制问题？金宝博娱乐

anil nerode.：DARPA计划域名特定软件倡议，COL ERIC METTALA的主任呼吁会议。我不知道这个词的意图是什么......我在那里，因为我是康奈尔的陆军赞助的数学科学研究所的陆军主任，并由ARO数学导演Jagdish Chandra发送。我发现第一次上午，Mettala认识到，1991年目前的控制软件行业不是实时控制陆海航空战国的实时控制软件。他邀请了控制软件行业，一些来自大公司的控制工程师（如狼·柯恩从波音），以及一些学术控制工程教授。我相信我只是那里的逻辑计算机科学人。（我在1950年代的控制系统设计和验证时，但除此之外，还没有工作。）金宝博官方

第一天的讨论很清楚，控制软件行业不知道如何编写基于逻辑的实时连续机器的数字控制程序，也绝对不知道如何验证这样的程序是正确的。我们被要求留下关于第二天要做什么的立场文件。我去我的房间,制定系统相互作用的连续和离散的概念(逻辑)设备,并明确表示,证明项目管理正常工作,您必金宝博官方须验证数字和连续的混合执行序列步骤总是会导致令人满意的性能规范。我没想到会有人注意到。

但是，第二天早上，经过一个完全混淆的讨论，观众的一些成员说：“为什么我们不使用NERODE对我们问题的定义教授。”令人惊讶的是，他们做到了。在当天晚些时候有一个讨论，在该讨论中，我非常强烈地支持了一个研究计划，而不是发展计划需要进行的。金宝博娱乐很多观众都没有看到它，他们希望数亿百万甚至更大的比例他们目前正在做的事情。从波音的狼kohn比我更清楚地表达了我的积分。在梅塔塔的终点中推出了RFP的研究计划，我让狼送给我他的论文。金宝博娱乐所以这是太平洋的会议，从我的角度来看。

卢基：Pacifica是否满足您在康奈尔组织1991年和1992年混合系统研讨会的启发？金宝博官方你知道是否出现了Mettala的RFP？

Anil.：我认识到这个问题的玛特拉斯，旨在为武装部队和商业和工业未来系统表示非常重要。金宝博官方我没有认为MettaLa足够明确地解决了能够为直接解决这个问题的DARPA RFP。

我在我的研究所获得了美国ARO的资金，以赞助新的研究。金宝博娱乐因此，我组织了在伊特卡的第一个混合体系，完全独立于Darpa授予金宝博官方那些我已经确定的世界各地的人提供。这些参与者来自AI和专家系统社区以及控制界。金宝博官方

伊萨卡的第一次会议是不是旨在产生一份卷或纸，而是建立一个聪明的人认为这是一个生产力的研究区域。金宝博娱乐我解释了我对混合系统的概念，他们买了它。金宝博官方我选择了“混合系统”作为该地区的金宝博官方名称。本集团选择作为后续第一个真正的混合系统研讨会和体积的组委会是该原始组的延伸。金宝博官方

Metalla在力量控制中的长期军事问题中提出了一般的RFP。金宝博娱乐我申请并获得了一些资金。其他人在他的RFP下获得了一些资金。

首席结果是混合系统理论的发展，仅仅因为我继续在这些葬奶和其他人下组织一个社区。金宝博官方一旦建立了这一点，该地区有很多资金来源。发展社区需要时间。在该领域筹备会议之后，我在该地金宝博娱乐区的实质性研究。

卢基：在那些早年，您采取了哪些行动 - 或者看到其他人采取 - 开发混合系统社区？金宝博官方回想起来，这是哪些行动对该领域的发展是最重要的？

Anil.：我的混合系统模型显示的是，要么提金宝博官方取或验证用连续设备互联的数字程序，程序验证（离散逻辑语言企业）和控制理论都需要专业知识（基于分析的连续数学）。

我在最初的三个混合系统批量会议上招募了最佳社区和他们的研究生。金宝博官方这混合是成功的关键。第一个参加参与的辉煌是在斯坦福，麻省理工学院和伯克利的控制和计划核查中的领导教授。许多其他人遵循这些机构的领导。他们通过他们的博士学位提供了大学和工业计算机科学与工程部门的许多教授和工程师。。

计算机科学家对计算机科学家的令人信服的吸引力是分析连续设备的数字工具，这是他们为数字世界开发的技术的新用途。

对照社区的令人信服的兴趣是，业界，商业和军队要求连续设备的数字控制。他们以前的技术是分段线性二次控制，具有高度非线性系统的断点，其中没有数学基础确保所得系统按要求执行。金宝博官方在线性二次控制的数学安全之后，他们在薄冰上滑冰。这是构建状态表的临时过程，然后进行仿真。

在许多情况下，嵌入式控制系统已经通过形式化(混合系统)方法进行了验证。金宝博官方(例如，奔驰汽车的嵌入式系统最初是由一位拥有麻省理工学院数理逻辑学位的科学家验证的金宝博官方。几年前，我在佛罗里达做了一个邀请演讲，之后他给我看了他的证明。)

我必须补充一点，对于存在生命安全风险的商业或军事系统，拥有这样的验证可以更容易地获得联金宝博官方邦认证或工业批准。

最后，一旦领先的世界数字已经订婚，融资机构遵循：他们还能做些什么？

卢基：这项研究计划的一些主要成功案例是什么？金宝博娱乐解决了行业或政府的实际问题，没有混合系统控制的情况无法解决？金宝博官方AndréPlatzer概述了单独的凯马拉的一些应用，这里;我希望你能提供一些早期的例子。

Anil.在Kohn和我把混合系统作为一个学科引入之前，已经有了高度发达的基于逻辑的技金宝博官方术来证明数字程序的执行序列总是满足它们的程序规范，或者找到反例。与此同时，有无数的嵌入式数字控制系统用于连续设备，也有许多尝试使程序可以作为，例如，一个辅助控制战场硬件。金宝博官方(这是ADA构建的目的之一。)

我们引入的混合系统的执行序列概念，我们引入了将程序验证范例扩展到混合数字连续系统。金宝博官方这不是任何特定的理论发展，是科学和工程的主要影响。至于计划验证，这是在许多行业进行的。我最喜欢的应用程序由MIT的PHD逻辑学家创建，是验证梅赛德斯豪华轿车的控制系统。金宝博官方

现在有技术组用于验证此类应用程序。

我和我的合作伙伴的主要兴趣是从系统描述和性能规范中提取连续系统的数字控制。金宝博官方我们在一些实用的情况下进行了商业化，而是整个整个数学背景所需的数学背景，所需计算的大小已经令人市解的领域的开发。它将在长期发生，因为它很有用且可能。

卢基：谢谢，anil！