.png){kind=icon}
.png){kind=icon}
Return
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}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
The ABZ 2025 conference case study focuses on developing a safety controller for autonomous highway driving. Within this context, we present a model of interacting agents that synchronize with a global state at specific points in time. These agents follow the differential equations of standard kinematics, operating within a physical environment. They can make non-deterministic decisions regarding acceleration and follow strategies to avoid collisions. We instantiate our model according to the Responsibility-Sensitive Safety (RSS) setting. By defining agent properties such as extensions, cycle times, and acceleration limits, we concentrate on the single-lane model specified in the case study requirements document. We also consider a polychronous setting, i.e. we demonstrate that the safety invariants still hold if agents have mutually independent and unknown clocks. This enhances the model's realism and makes it well-suited for refinement into implementations using synchronous languages.
Keywords:
Process-Algebra
Semantics
Concurrency
Computational Models
Theorem Proving
Isabelle/HOL
Journal
R
IF:
0
Papers:
23
Citations:
0