首页/论文/2011.07630

arXiv 2011.076302020-11-27cs.FLcs.LG

Safety Synthesis Sans Specification

TU Graz（格拉茨技术大学）；King’s College London（伦敦国王学院）；Ben-Gurion University（本-古里安大学）；EPFL（洛桑联邦理工学院）

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Dana Fisman, Heinz Riener

英文摘要：

We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

基于大语言模型的自动安全合规线性时序逻辑生成：一种自监督框架

Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework

本文提出AutoSafeLTL框架，利用大语言模型自动生成符合安全限制的LTL规范，通过语言包含检查与自动反例引导修改机制确保逻辑一致性和语义准确性。

2026-04-27cs.FLcs.LO

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct oblivious online monitoring -- online monitoring conducted without revealing the private information of each party to the other -- against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring…

2022-06-03cs.CRcs.FLcs.LO

环境规范下可达性与安全性属性的LTLf合成

LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

Sapienza University of Rome（罗马第一大学）；University of Oxford（牛津大学）；ENS Rennes（雷恩高等师范学校）；The University of Sydney（悉尼大学）

本文系统研究了环境规范下LTLf合成问题，针对可达性和安全性属性提出完整算法框架，并证明各算法在复杂度上最优且正确。

2023-08-29cs.AIcs.FLcs.LO

信号时序逻辑规范下随机系统的安全性验证

Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications

研究随机系统在信号时序逻辑规范下的验证问题，提出STL侵蚀策略，将概率验证转化为更严格的确定性验证，可与现有算法无缝集成，数值实验验证了其有效性。

2025-02-11cs.FLcs.LOcs.SY

带有安全约束的反应合成学习规范

Learning specifications for reactive synthesis with safety constraints

Google LLC（谷歌公司）；MITRE Corporation（MITRE公司）；University of Colorado Boulder（科罗拉多大学波德分校）

本文提出了一种结合安全约束的反应合成学习方法，通过概率确定有限自动机建模任务规范，平衡用户偏好与机器人成本，生成最优解的帕累托前沿。

2026-01-09cs.FLcs.RO

Safety-Critical Learning of Robot Control with Temporal Logic Specifications

Lehigh University（里海大学）

Reinforcement learning (RL) is a promising approach. However, success is limited to real-world applications, because ensuring safe exploration and facilitating adequate exploitation is a challenge for controlling robotic systems with unknown models and measurement uncertainties. The learning problem becomes even more difficult for complex tasks over continuous state-action. In this paper, we propose a learning-based robotic control framework consisting of several aspects: (1) we leverage Linear Temporal Logic (LTL) to express complex tasks over infinite horizons that are translated to a novel …

2022-08-26cs.FLcs.LGcs.RO

更多相关论文收起更多论文

面向安全约束规划的语言模型联合验证与精化

Joint Verification and Refinement of Language Models for Safety-Constrained Planning

University of Texas at Austin（德克萨斯大学奥斯汀分校）

本文提出将机器人程序转为自动机表示并验证安全规范，利用组合定理降低验证复杂度，并通过仅训练安全子组件的自动微调方法，使规范合规程序生成概率提高30%，训练时间减半。

2025-11-06cs.AIcs.FLcs.RO

Monitoring Cyber-Physical Systems: From Design to Integration

Cyber-physical systems are inherently safety-critical. The deployment of a runtime monitor significantly increases confidence in their safety. The effectiveness of the monitor can be maximized by considering it an integral component during its development. Thus, in this paper, I given an overview over recent work regarding a development process for runtime monitors alongside a cyber-physical system. This process includes the transformation of desirable safety properties into the formal specification language RTLola. A compiler then generates an executable artifact for monitoring the specificat…

2020-12-15cs.FLcs.SE

Multiagent Transition Systems for Composing Fault-Resilient Protocol Stacks

We present a novel mathematical framework for the specification and analysis of fault-resilient distributed protocols and their implementations, with the following components: 1. Transition systems that allow the specification and analysis of computations with safety and liveness faults and their fault resilience. 2. Notions of safe, live and complete implementations among transition systems and their composition, with which the correctness (safety and liveness) and completeness of a protocol stack as a whole follows from each protocol implementing correctly and completely the protocol above i…

2023-02-20cs.DCcs.FLcs.MA

Verified Rust Monitors for Lola Specifications

The safety of cyber-physical systems rests on the correctness of their monitoring mechanisms. This is problematic if the specification of the monitor is implemented manually or interpreted by unreliable software. We present a verifying compiler that translates specifications given in the stream-based monitoring language Lola to implementations in Rust. The generated code contains verification annotations that enable the Viper toolkit to automatically prove functional correctness, absence of memory faults, and guaranteed termination. The compiler parallelizes the evaluation of different streams…

2020-12-15cs.FLcs.SE

Automatic Trajectory Synthesis for Real-Time Temporal Logic

University of Notre Dame（圣母大学）

Many safety-critical systems must achieve high-level task specifications with guaranteed safety and correctness. Much recent progress towards this goal has been made through controller synthesis from temporal logic specifications. Existing approaches, however, have been limited to relatively short and simple specifications. Furthermore, existing methods either consider some prior discretization of the state-space, deal only with a convex fragment of temporal logic, or are not provably complete. We propose a scalable, provably complete algorithm that synthesizes continuous trajectories to satis…

2020-09-14cs.FLcs.ROcs.SY

Bounded Synthesis and Reinforcement Learning of Supervisors for Stochastic Discrete Event Systems with LTL Specifications

In this paper, we consider supervisory control of stochastic discrete event systems (SDESs) under linear temporal logic specifications. Applying the bounded synthesis, we reduce the supervisor synthesis into a problem of satisfying a safety condition. First, we consider a synthesis problem of a directed controller using the safety condition. We assign a negative reward to the unsafe states and introduce an expected return with a state-dependent discount factor. We compute a winning region and a directed controller with the maximum satisfaction probability using a dynamic programming method, wh…

2022-04-09cs.FLcs.SYeess.SY

Formal Test Synthesis for Safety-Critical Autonomous Systems based on Control Barrier Functions

California Institute of Technology（加州理工学院）

The prolific rise in autonomous systems has led to questions regarding their safe instantiation in real-world scenarios. Failures in safety-critical contexts such as human-robot interactions or even autonomous driving can ultimately lead to loss of life. In this context, this paper aims to provide a method by which one can algorithmically test and evaluate an autonomous system. Given a black-box autonomous system with some operational specifications, we construct a minimax problem based on control barrier functions to generate a family of test parameters designed to optimally evaluate whether …

2020-04-08cs.FLcs.ROcs.SY

具有线性时序逻辑规范的风险感知自主驾驶

Risk-Aware Autonomous Driving with Linear Temporal Logic Specifications

Department of Electrical Engineering, Eindhoven University of Technology（电子工程系，埃因霍温理工大学）；College of Engineering, Peking University（工程学院，北京大学）

本文提出一种基于线性时序逻辑规范的风险感知自动驾驶方法，通过扩展风险度量方法以涵盖更复杂的驾驶场景，结合线性规划解决控制合成问题，从而平衡碰撞风险和交通违规风险。

2026-03-05cs.FLcs.ROcs.SY

Reactive Synthesis from Extended Bounded Response LTL Specifications

Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades. It consists in the synthesis of a controller that reacts to environment's inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability. In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (\LTLEBR), that allows one to combine bounded and universal unbounded temporal operators…

2020-08-12cs.FLcs.LOcs.SE

基于信号时间逻辑规范的模型预测控制

Model Predictive Control for Signal Temporal Logic Specification

California Institute of Technology（加州理工学院）；UC Berkeley（加州大学伯克利分校）；C3 Energy Inc.（C3能源公司）

本文提出一种基于数学规划的模型预测控制方法，用于满足信号时间逻辑规范的物理系统。通过将STL规范编码为混合整数线性约束，实现系统变量的优化控制，实验展示了建筑能源和气候控制的控制器合成效果。

2017-03-28cs.FLcs.LOcs.SY