概率分布度量区间时态逻辑的策略综合
Policy Synthesis for Metric Interval Temporal Logic with Probabilistic Distributions
摘要：
度量时序逻辑可以表达实时系统中具有时间关键约束或时间触发约束的时序演化特性。本文扩展了度量区间时序逻辑与分布的可能性运营商表示时间敏感的任务与动态的，概率性的环境中的系统交互。这种形式主义使我们能够描述的随机外部事件的概率发生的一部分，任务规范和事件触发的时间约束的预期系统的行为。本文的主要贡献是两个折叠：首先，我们提出了一个过程，将一个规格到一个随机时间自动机。其次，我们开发了一个近似最优的概率规划问题，用于合成控制策略，最大限度地提高规划代理实现任务的概率，只要外部事件满足规范。规划算法采用截断的时钟的时间自动机减少规划在一个可数无限的状态空间到一个有限的状态空间有界误差保证。我们说明了一个机器人运动规划的例子的方法。
英文摘要：
Metric Temporal Logic can express temporally evolving properties with time-critical constraints or time-triggered constraints for real-time systems. This paper extends the Metric Interval Temporal Logic with a distribution eventuality operator to express time-sensitive missions for a system interacting with a dynamic, probabilistic environment. This formalism enables us to describe the probabilistic occurrences of random external events as part of the task specification and event-triggered temporal constraints for the intended system's behavior. The main contributions of this paper are two folds: First, we propose a procedure to translate a specification into a stochastic timed automaton. Second, we develop an approximate-optimal probabilistic planning problem for synthesizing the control policy that maximizes the probability for the planning agent to achieve the task, provided that the external events satisfy the specification. The planning algorithm employs a truncation in the clocks for the timed automaton to reduce the planning in a countably infinite state space to a finite state space with a bounded error guarantee. We illustrate the method with a robot motion planning example.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
