发帖
雷达卡
摘要翻译：
本文提出了一种离散时间随机系统的时序逻辑验证方法。我们的目标是找到系统的有限迹满足复杂时间性质的概率的下界。系统所需的时间特性用线性时间逻辑片断表示，称为有限迹上的安全LTL。我们建议使用障碍证书来计算这种下界，这比现有的基于离散化的方法在计算上更有效。该方法是无离散化的，不受状态集离散化带来的维数诅咒。所提出的方法依赖于将规范的否定分解为序列可达性的并集，然后使用障碍证书计算这些可达性概率的上界。我们在线性和多项式动力学的案例研究中证明了所提方法的有效性。
---
英文标题：
《Temporal Logic Verification of Stochastic Systems Using Barrier
Certificates》
---
作者：
Pushpak Jagtap and Sadegh Soudjani and Majid Zamani
---
最新提交年份：
2018
---
分类信息：
一级分类：Computer Science 计算机科学
二级分类：Systems and Control 系统与控制
分类描述：cs.SY is an alias for eess.SY. This section includes theoretical and experimental research covering all facets of automatic control systems. The section is focused on methods of control system analysis and design using tools of modeling, simulation and optimization. Specific areas of research include nonlinear, distributed, adaptive, stochastic and robust control in addition to hybrid and discrete event systems. Application areas include automotive and aerospace control systems, network control, biological systems, multiagent and cooperative control, robotics, reinforcement learning, sensor networks, control of cyber-physical and energy-related systems, and control of computing systems.
cs.sy是eess.sy的别名。本部分包括理论和实验研究，涵盖了自动控制系统的各个方面。本节主要介绍利用建模、仿真和优化工具进行控制系统分析和设计的方法。具体研究领域包括非线性、分布式、自适应、随机和鲁棒控制，以及混合和离散事件系统。应用领域包括汽车和航空航天控制系统、网络控制、生物系统、多智能体和协作控制、机器人学、强化学习、传感器网络、信息物理和能源相关系统的控制以及计算系统的控制。
--
一级分类：Electrical Engineering and Systems Science 电气工程与系统科学
二级分类：Systems and Control 系统与控制
分类描述：This section includes theoretical and experimental research covering all facets of automatic control systems. The section is focused on methods of control system analysis and design using tools of modeling, simulation and optimization. Specific areas of research include nonlinear, distributed, adaptive, stochastic and robust control in addition to hybrid and discrete event systems. Application areas include automotive and aerospace control systems, network control, biological systems, multiagent and cooperative control, robotics, reinforcement learning, sensor networks, control of cyber-physical and energy-related systems, and control of computing systems.
本部分包括理论和实验研究，涵盖了自动控制系统的各个方面。本节主要介绍利用建模、仿真和优化工具进行控制系统分析和设计的方法。具体研究领域包括非线性、分布式、自适应、随机和鲁棒控制，以及混合和离散事件系统。应用领域包括汽车和航空航天控制系统、网络控制、生物系统、多智能体和协作控制、机器人学、强化学习、传感器网络、信息物理和能源相关系统的控制以及计算系统的控制。
--
---
英文摘要：
This paper presents a methodology for temporal logic verification of discrete-time stochastic systems. Our goal is to find a lower bound on the probability that a complex temporal property is satisfied by finite traces of the system. Desired temporal properties of the system are expressed using a fragment of linear temporal logic, called safe LTL over finite traces. We propose to use barrier certificates for computations of such lower bounds, which is computationally much more efficient than the existing discretization-based approaches. The new approach is discretization-free and does not suffer from the curse of dimensionality caused by discretizing state sets. The proposed approach relies on decomposing the negation of the specification into a union of sequential reachabilities and then using barrier certificates to compute upper bounds for these reachability probabilities. We demonstrate the effectiveness of the proposed approach on case studies with linear and polynomial dynamics.
---
PDF链接：
https://arxiv.org/pdf/1807.00064
京公网安备 11010802022788号
