Anil Nerode的混合系统控制亚博体育苹果app官方下载

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

会议的目的是探讨如何清除主要瓶颈，控制大型军事系统，如防空空间中的航空军部队。亚博体育苹果app官方下载

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

anil nerode.：DARPA计划域名特定软件倡议主任COL ERIC METTALA召集会议。我不知道这个词的意图是什么......我在那里，因为我是康奈尔的陆军赞助的数学科学研究所的陆军总监，并由ARO数学导演Jagdish Chandra发送。我的第一次早上发现，Mettaala认识到，1991年目前的控制软件行业并不是实时陆海航空公司将军的实时控制软件。他邀请了控制软件行业，来自大公司的一些控制工程师（如狼·柯恩，来自波音的狼，以及一些学术控制工程教授。我相信我只是那里的逻辑计算机科学人。（我在20世纪50年代的控制系统设计和验证时工作，而不是这样做。）亚博体育苹果app官方下载

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

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

卢克：Pacifica是否满足您在康奈尔组织1991年和1992年的混合系统研讨会的灵感？亚博体育苹果app官方下载你知道什么是Mettala的RFPS吗？

Anil.：我认识到这个问题的玛丽拉，为武装部队和商业和工业未来系统提出非常重要。亚博体育苹果app官方下载我没有认为Mettala足够清楚的问题是能够制定一个将直接解决这个问题的DARPA RFP。

我在我的研究所获得了美国ARO的资金，以赞助新的研究。亚博体育官网因此，我组织了在伊特卡的第一个混合体系，完全独立于Darpa授予亚博体育苹果app官方下载那些我被确定为有东西提供的世界宽度。这些参与者来自AI和专家系统社区和控制界。亚博体育苹果app官方下载

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

Metalla在长期军事问题控制中阐明了普通RFP，用于控制力量和机亚博体育官网器的长期军事问题。我申请并获得了一些资金。其他人在他的RFP下获得了一些资金。

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

卢克：在那些早年，你采取了什么行动 - 或者看到其他人采取 - 制定混合系统社区？亚博体育苹果app官方下载回想起来，这是哪些行动是对该领域的开发最重要的？

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

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

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

控制社区的令人信服的兴趣是，业内，业务和军队要求连续设备的数字控制。他们以前的技术是分段线性二次控制，具有用于高度非线性系统的断点，在那里没有数学基础确保所得到的系统会根据要求执行。亚博体育苹果app官方下载在线性二次控制的数学安全之后，他们在薄冰上滑冰。这是构建状态表的临时过程，然后进行仿真。

在许多情况下，嵌入式控制系统已经通过正式的(混合系统)方法进行了验证。亚博体育苹果app官方下载(例如，奔驰汽车的嵌入式系统首先是由一位拥有麻省理工学院数学逻辑学位的科学家验证的亚博体育苹果app官方下载。几年前，我应邀在佛罗里达州做了一场讲座，他向我展示了他的证明。)

我必须补充一点，对于有生命安全风险的商业或军事系统，有这样的验证可以使其更容易获得联邦亚博体育苹果app官方下载认证或工业批准。

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

卢克：这项研究计划的一些主要成功案例是什么？亚博体育官网解决了行业或政府的实际问题，没有混合系统控制的情况无法解决？亚博体育苹果app官方下载AndréPlatzer概述了Keymaera的一些应用，这里;我希望你能提供一些早期的例子。

Anil.在Kohn和我将混合系统作为一门学科引入之前，已经有了高度发达的基于逻辑的技亚博体育苹果app官方下载术来证明数字程序的执行序列总是满足其程序规格，或者寻找反例。与此同时，有无数用于连续设备的嵌入式数字控制系统，也有许多人试图编写程序，例如，作为控制战场硬件的辅助程序。亚博体育苹果app官方下载(这也是《美国残疾人法》的宗旨之一。)

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

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

我和我的合作伙伴的主要兴趣是从系统描述和性能规范中提取连续系统的数字控制。亚博体育苹果app官方下载我们在一些实用的案例中完成了这些商业，但作为整个所需的数学背景，所需计算的大小已经阻止了该领域的开发。它将在长期发生，因为它很有用，可能。

卢克：谢谢，anil！