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.

SIAM paper - multimethod

v0.3

update simulation_time.m

SIAM paper - multi layered

v0.3ML

Compare to single layered approach

Multi-method for thesis

Multi-method approach used in Birgits thesis.

CDC code

This version of Main was used for the initial submission to CDC 2022.

Linear 2D

Version of the Matlab tool that is able to handle two-dimensional case studies that are linear. Tutorials include CarPark2D(_optimized) and a Scalability_Model. This version is also used to simulate the building automation (BAS) case study including Model Order Reduction.