保罗Tabuada“康乃馨革命”后一年，他在葡萄牙的里斯本出生。他于1998年获得葡萄牙里斯本的Instituto Superior Tecnico的航空航天工程“许可”学位，并于2002年获得系统和机器人研究所(与Instituto Superior Tecnico相关的私人研究机构)的电子和计算机工程博士学位。亚博体育官网亚博体育苹果app官方下载2002年1月至2003年7月，他在宾夕法尼亚大学(University of Pennsylvania)担任博士亚博体育官网后研究员。在诺特丹大学(University of Notre Dame)担任助理教授3年后，他加入了加州大学洛杉矶分校(University of California, Los Angeles)的电气工程系，在那里他建立并指导了电气工程系Cyber-Physical系亚博体育苹果app官方下载统实验室。
Paulo Tabuada对信息物理系统的贡献获得了多个奖项的认可，包括2005年的NSF职业奖亚博体育苹果app官方下载、2009年的Donald P. Eckman奖和2011年的George S. Axelby奖。2009年，他共同主持国际会议混合系统:计算与控制亚博体育苹果app官方下载(HSCC ' 09)， 2012年，他是第三届IFAC网络系统分布式估计和控制研讨会(NecSys ' 12)的项目联席主席。亚博体育苹果app官方下载他还担任IEEE嵌入式系统通讯和IEEE自动控制汇刊的编委会成员。亚博体育苹果app官方下载他的最新书2009年由施普林格出版的《混合动力系统的验证与控制》。亚博体育苹果app官方下载
路加福音Muehlhauser:在“信息物理系统的鲁棒性提取与精炼亚博体育苹果app官方下载，你和你的合著者写道:
我们提出了一种鲁棒信息物理系统(CPS)的设计方法，[该方法]抓住了鲁棒设计的两个直观目标:有界干扰产生有限的结果，而亚博体育苹果app官方下载零星干扰的影响随着时间的推移而消失。
您可以为此使用“抽象和细化”过程。在这种情况下，抽象和细化过程是如何工作的?
保罗Tabuada网络物理系统的设计和验证是出了名的亚博体育苹果app官方下载困难，因为网络和物理部件之间的交互非常复杂。虽然控制理论家已经开发了设计和分析物理部件的强大技术，比如用微分方程来描述，计算机科学家也开发了设计和分析网络部件的强大技术，比如用有限状态模型来描述，但这些技术在大多数情况下是不兼容的。后者依赖于离散数学，而前者依赖于连续数学。我们的方法是将所有的物理组件替换为网络抽象，这样所有剩余的设计和验证任务都可以在网络世界中完成。这些抽象的构造是基于严格的数值模拟，并结合微分方程模型的分析，以保证原始的物理部件及其抽象等效达到所需的精度。从技术上讲，“等效于所需的精度”意味着近似的双相似，从直观上讲，这意味着两个模型生成相同的行为集，达到所需的精度。
路加福音:去年夏天你给出了一个四部分的教程(p1,p2,p3,p4)，研究信息物理系统的程序合成。亚博体育苹果app官方下载对于那些不熟悉程序合成的人，你能描述一下它是如何在信息物理系统的环境中完成的，并给出一个已经实现的这样一个系统的例子吗?亚博体育苹果app官方下载
保罗程序合成对于只有软件的系统来说已经是一个具有挑战性的问题。亚博体育苹果app官方下载在信息物理系统的背景下，它变得更具挑战性，因为目标是合成一个程序，亚博体育苹果app官方下载使物理系统的行为如预期的那样。我目前正在从事两个与程序合成有关的项目。其中一个目标是控制两足机器人行为的合成程序。与丰田和福特合作的自适应巡航控制和车道偏离控制系统也在同一个项目中使用了同样的技术。亚博体育苹果app官方下载为了让你们知道挑战在哪里，让我回顾一下这个项目是如何开始的。我在密歇根大学的同事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.
路加福音机器人和其他人工智能系统在操作上越来越自动化亚博体育苹果app官方下载:自动驾驶汽车,机器人,在灾难现场,高频交易快速交易股票的程序闪电崩盘"市场或几乎破产大型股票交易商等。
当前的人工智能安全方法(形式验证、程序合成、单一架构等)如何扩大规模，以应对在未知、连续、动态环境中运行的高度自治系统提出的安全挑战?亚博体育苹果app官方下载我们使系统更自治和更有能力的能力，是否会超过我们为这亚博体育苹果app官方下载些系统实现有信心的安全保证的能力?
保罗事实上，这就是到目前为止所发生的情况。我们创造大型复杂系统的能力远远超过了我们对确保其安全运行的基本科学原理的亚博体育苹果app官方下载理解。在我看来，基于合成的方法最有可能扩展到现有应用程序的级别。这些系统的正式验证是非常困难的，因为设计空间非常非常大。亚博体育苹果app官方下载没有任何正式的验证技术能够处理来自如此大的设计空间的各种各样的系统。亚博体育苹果app官方下载然而，当使用综合时，我们可以减少设计空间，从而获得更结构化的设计，从而获得形式保证。反过来，我们失去的是找到所有设计解决方案的能力。这种权衡在工程的其他领域很好地理解，例如，砖和灰泥或木框架建筑结构。我相信用不了多久，我们就会发现一些能够保证高度自治系统的安全性和正确性的综合技术，即使这些技术会产生一些更加保守的解决方案。亚博体育苹果app官方下载
路加福音您写道:“它不会花很长时间，直到我们发现一些综合技术，保证安全性和高度自治系统的正确性，即使这些结果在某种程度上更加保守的解决方案。”亚博体育苹果app官方下载你能把你的想法说清楚吗?例如，对于自动驾驶汽车的软件来说，一个“保守的解决方案”看起来会是什么样子的呢?(如果你喜欢，可以随便举一个不同的例子。)
保罗我所说的保守是指我们将不得不限制合成软件，使它属于一个可以使用合成技术的类。一个简单的例子是可以用时间自动机描述的软件。尽管基于几个计时器的泛型函数进行决策可能很方便，但在time -自动机类中，我们只允许将计时器与常量进行比较，或者比较计时器与常量之间的差异。对自动驾驶汽车来说，这可能意味着根据超过阈值的延迟做出决定，但不允许根据几次延迟的平均值做出决定。
路加福音:谢谢你,保罗!
你喜欢这个帖子吗?你可以享受我们的另一个对话的帖子,包括:
