.png){kind=icon}
返回
Polychronous RSS in a Process-Algebraic Framework - A Case Study
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-031-94533-5_15.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
ABZ 2025会议案例研究聚焦于自主高速公路驾驶的安全控制器开发。在此背景下，我们提出一个交互智能体模型，该模型在特定时间点与全局状态同步。这些智能体遵循标准运动学的微分方程，在物理环境中运行。它们可以就加速能量做出非确定性决策，并遵循避免碰撞的策略。我们根据责任敏感安全（RSS）设置来实例化我们的模型。通过定义智能体属性，如扩展、循环时间和加速度限制，我们专注于案例研究需求文档中规定的单车道模型。我们还考虑了多时序设置，即我们证明了当智能体具有相互独立且未知的时钟时，安全不变量仍然成立。这增强了模型的真实性，并使其非常适合使用同步语言进行精化实现。
Keyword:
Process-Algebra
Semantics
Concurrency
Computational Models
Theorem Proving
Isabelle/HOL
期刊
R
IF:
0
论文数:
23
被引数:
0
机构
引用论文
.png){kind=icon}
Formally verified architectural patterns of hybrid systems using proof and refinement with Event-B通过Event-B进行证明和精化，正式验证的混合系统架构模式
OAAI
OAAI分享收藏分享收藏
查看更多内容