CDC submission

Introduction: This is the code for case studies in year 2025 CDC submission: 'Unraveling tensor structures in correct-by-design controller synthesis'.

Reference paper: https://arxiv.org/pdf/2503.24085
Branch: main_ruohan

i.

To reproduce time(s) and memory usage (MB) in TABLE.I of paper:

1. Run ToycaseTensor\Exact\RA_Exact_2D.m for line 1 in TABLE.I: Exact value iteration applied on specification ψ := (¬p2 ∧ ¬p3)U p1 on a 2D system.

2. Run ToycaseTensor\FullRankTree\RA_FullTree_2D.m for line 2 in TABLE.I: Full rank tree value iteration applied on specification ψ := (¬p2 ∧ ¬p3)U p1 on a 2D system.

3. Run ToycaseTensor\Rank1Tree\RA_Rank1_2D.m for line 3: Rank-1 tree value iteration applied on specification ψ := (¬p2 ∧ ¬p3)U p1 on a 2D system.

4. Run ToycaseTensor\Rank1Tree\RA_Rank1_4D.m for line 4,5,6,7 in TABLE.I and Fig.6 and Fig.7: Rank-1 tree value iteration applied on specification ψ := (¬p2 ∧ ¬p3)U p1 on a 4D system with varying grid counts (line 53).

ii.

To reproduce time(s) and memory usage (MB) for Sec V.C Scalability benchmark:

1. Run ToycaseTensor\Rank1Tree\RA_Rank1_sca.m for specification ψ1 (reach-avoid specification) with varying number of agents.

2. Run ToycaseTensor\Rank1Tree\Safe_Rank1_sca.m for specification ψ2 (safety specification) with varying number of agents.

3. Run ToycaseTensor\Rank1Tree\figure_scalability_analysis.m for Fig.8 of paper.