Paulo Tabuada关于网络物理系统的程序合成金宝博官方

||谈话

保罗塔布达肖像Paulo Tabuada出生于葡萄牙里斯本,一年后康乃馨革命。他于1998年从Instituto Superior Tecnico,Lisbon,Lisbon,Lisbon,1998年获得了“Licenciatura”学位,并在博士学位。2002年电气和计算机工程学位从系统和机器人研究所,私人研究所与Instituto Superior Tecnico相关联。金宝博娱乐金宝博官方2002年1月至2003年7月,他是宾夕法尼亚大学的博士后研究员。金宝博娱乐在圣母院大学花费三年后,作为助理教授,他加入了加州大学洛杉矶的电气工程系,他建立并指导了Cyber-Physical系金宝博官方统实验室

Paulo Tabuada对网络系统系统的贡献已被多个奖项所公认,包括2005年的NSF职业奖,金宝博官方2009年唐纳德P.Eckman奖和2011年的乔治S. Axelby奖。2009年他共同主持了国际会议混合系统:计算和控制金宝博官方(HSCC'09)和2012年,他是第三届IFAC研讨会的计划联合主席关于网络系统的分布式估计和控制(NECSYS'12)。金宝博官方他还在IEEE嵌入式系统字母和IEEE事务上担任了关于自动控制的IEEE交易的编辑委员会。金宝博官方他的最新2009年由施普林格出版的《混合动力系统的验证与控制》。金宝博官方

卢克·穆罕沃斯: 在 ”网络物理系统的抽象和精炼鲁棒性金宝博官方,“你和你的共同作者写道:

...我们提出了强大的网络物理系统(CPS)的设计方法[哪个] ......捕获了两种直观的旨在的设计目标:有界扰动具金宝博官方有界限后果,随着时间的推移,零星扰动的效果消失。

您使用“抽象和精炼”程序。在这种情况下,抽象和细化程序如何工作?


Paulo Tabuada:由于网络和物理组件之间的复杂相互金宝博官方作用,网络物理系统难以设计和验证。虽然控制理论家已经开发了用于设计和分析物理成分的强大技术,但是通过微分方程描述,计算机科学家已经开发了用于设计和分析网络组件的强大技术,例如由有限状态模型描述,这些技术是最不兼容的。后者依赖离散数学,而前者依靠连续数学。我们的方法是基于通过网络抽象替换所有物理组件,以便在网络世界中可以完成所有剩余的设计和验证任务。这些抽象的构造是基于严格的数值模拟,结合了微分方程模型的分析,以保证原始物理分量及其抽象等同于所需的精度。从技术上讲,“相当于期望的精度”意味着大致相似和直观地意味着两种模型产生相同的行为,直到所需的精度。


卢基上个夏天你给了四部分教程(p1p2p3p4关于网络物理系统的程序合成。金宝博官方对于不熟悉程序合成的人来说,您是否可以描述如何在网络物理系统的背景下完成,并展示已实现的这种系统的示例?金宝博官方


保罗程序合成对于只有软件的系统来说已经是一个具有挑战性的问题。金宝博官方在信息物理系统的背景下,它变得更具挑战性,因为目标是合成一个程序,金宝博官方使物理系统的行为如预期的那样。我目前正在从事两个与程序合成有关的项目。其中一个目标是控制两足机器人行为的合成程序。与丰田和福特合作的自适应巡航控制和车道偏离控制系统也在同一个项目中使用了同样的技术。金宝博官方为了让你们知道挑战在哪里,让我回顾一下这个项目是如何开始的。我在密歇根大学的同事Jessy Grizzle和德州农工大学的Aaron Ames来找我,分享了他们开发的控制机器人的程序所带来的沮丧。虽然他们很满意让他们的机器人在平坦和通畅的表面行走,但他们在不平坦的地形上面临着很大的问题。他们的方法是开发一套规则,即一个反应性程序,通过确定应该使用哪些驱动器以及如何使用,来响应传感器提供的刺激。尽管这些规则是基于常识制定的,但很快我们就发现,预测这些规则的执行将如何影响机器人的运动是不可能的。 Moreover, a small change in the rules would lead to completely different and unexpected behavior. Our approach is to construct a finite-state abstraction of the robot dynamics and then to synthesize a reactive program that forces this abstraction to satisfy a desired specification. The synthesis of these reactive programs is done via the solution of a two player game where the synthesized program plays against the robot’s environment and enforces the specification no matter which action the environment takes. In this way, rather than verifying a reactive program, we synthesize one that is guaranteed to be correct by construction.


卢基:机器人和其他AI系统在操作中越来越自主:金宝博官方自驾,机器人那个导航灾难站点HFT.快速交易股票的程序闪存崩溃“市场或几乎破产大型股票交易员等。

目前如何均衡AI安全方法(正式验证,程序综合,单纯X架构等)以满足在未知,连续,动态环境中运行的高度自主系统提出的安全挑战?金宝博官方我们是否会使系统更加自主和能力的能力来实现这些系统的金宝博官方自信安全保障?


保罗事实上,这就是到目前为止所发生的情况。我们创造大型复杂系统的能力远远超过了我们对确保其安全运行的基本科学原理的金宝博官方理解。在我看来,基于合成的方法最有可能扩展到现有应用程序的级别。这些系统的正式验证是非常困难的,因为设计空间非常非常大。金宝博官方没有任何正式的验证技术能够处理来自如此大的设计空间的各种各样的系统。金宝博官方然而,当使用综合时,我们可以减少设计空间,从而获得更结构化的设计,从而获得形式保证。反过来,我们失去的是找到所有设计解决方案的能力。这种权衡在工程的其他领域很好地理解,例如,砖和灰泥或木框架建筑结构。我相信用不了多久,我们就会发现一些能够保证高度自治系统的安全性和正确性的综合技术,即使这些技术会产生一些更加保守的解决方案。金宝博官方


卢基您写道:“它不会花很长时间,直到我们发现一些综合技术,保证安全性和高度自治系统的正确性,即使这些结果在某种程度上更加保守的解决方案。”金宝博官方你能把你的想法说清楚吗?例如,对于自动驾驶汽车的软件来说,一个“保守的解决方案”看起来会是什么样子的呢?(如果你喜欢,可以随便举一个不同的例子。)


保罗我所说的保守是指我们将不得不限制合成软件,使它属于一个可以使用合成技术的类。一个简单的例子是可以用时间自动机描述的软件。尽管基于几个计时器的泛型函数进行决策可能很方便,但在time -自动机类中,我们只允许将计时器与常量进行比较,或者比较计时器与常量之间的差异。对自动驾驶汽车来说,这可能意味着根据超过阈值的延迟做出决定,但不允许根据几次延迟的平均值做出决定。


卢基:谢谢,保罗!