Task and Motion Planning of Dynamic Systems using Hyperproperties for Signal Temporal Logics
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918134846324736 |
|---|---|
| author | Zhao, Jianing Ye, Bowen Yu, Xinyi Majumdar, Rupak Yin, Xiang |
| author_facet | Zhao, Jianing Ye, Bowen Yu, Xinyi Majumdar, Rupak Yin, Xiang |
| contents | We investigate the task and motion planning problem for dynamical systems under signal temporal logic (STL) specifications. Existing works on STL control synthesis mainly focus on generating plans that satisfy properties over a single executed trajectory. In this work, we consider the planning problem for hyperproperties evaluated over a set of possible trajectories, which naturally arise in information-flow control problems. Specifically, we study discrete-time dynamical systems and employ the recently developed temporal logic HyperSTL as the new objective for planning. To solve this problem, we propose a novel recursive counterexample-guided synthesis approach capable of effectively handling HyperSTL specifications with multiple alternating quantifiers. The proposed method is not only applicable to planning but also extends to HyperSTL model checking for discrete-time dynamical systems. Finally, we present case studies on security-preserving planning and ambiguity-free planning to demonstrate the effectiveness of the proposed HyperSTL planning framework. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_02184 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Task and Motion Planning of Dynamic Systems using Hyperproperties for Signal Temporal Logics Zhao, Jianing Ye, Bowen Yu, Xinyi Majumdar, Rupak Yin, Xiang Systems and Control We investigate the task and motion planning problem for dynamical systems under signal temporal logic (STL) specifications. Existing works on STL control synthesis mainly focus on generating plans that satisfy properties over a single executed trajectory. In this work, we consider the planning problem for hyperproperties evaluated over a set of possible trajectories, which naturally arise in information-flow control problems. Specifically, we study discrete-time dynamical systems and employ the recently developed temporal logic HyperSTL as the new objective for planning. To solve this problem, we propose a novel recursive counterexample-guided synthesis approach capable of effectively handling HyperSTL specifications with multiple alternating quantifiers. The proposed method is not only applicable to planning but also extends to HyperSTL model checking for discrete-time dynamical systems. Finally, we present case studies on security-preserving planning and ambiguity-free planning to demonstrate the effectiveness of the proposed HyperSTL planning framework. |
| title | Task and Motion Planning of Dynamic Systems using Hyperproperties for Signal Temporal Logics |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2509.02184 |