Symbolic

Abstract Type: SymbolicModel{N, M}

Defines a generic symbolic model interface, where:

• N is the state space dimension.
• M is the input space dimension.

GridBasedSymbolicModel{N,M} <: SymbolicModel{N,M}

Intermediate abstract type for symbolic models that rely on a grid-based or mapping-based discretization.

Semantics:

• state mapping: global abstract-state numbering / coordinate map
• input mapping: global abstract-input numbering / coordinate map
• source domain (Xset): states enumerated as sources
• retained domain (Rset): states allowed as targets

SymbolicModelList:

• XMapping / UMapping define universes and conversions
• Xset: states we build from (sources)
• Rset: allowed states as targets (superset; "relation universe allowance")
• Uset: inputs considered

LocalGridBasedSymbolicModel

Wrapper around a global symbolic model that overrides only the source domain. The state mapping, input mapping, retained domain and input domain remain global.

determinize_symbolic_model(sym; AutomatonConstructor, convert_U_to_list)

Return a deterministic symbolic model by refining the input alphabet: each original input u is replaced by a pair (u_coord, target_state).

This is useful to turn nondeterministic transitions into deterministic ones by making the target part of the symbol.

AbstractExecutionBackend

Abstract type for execution backends used to compute the transition relation in grid-based symbolic abstraction.

An execution backend defines how the abstraction computation is executed:

• sequentially,
• multithreaded,
• distributed across Julia workers,
• or via SLURM array jobs.

SequentialBackend()

Sequential execution (no parallelism).

ThreadedBackend(progress_dt=0.2)

Multithreaded execution using all available Julia threads.

Parameters

• progress_dt: minimum time (in seconds) between progress updates.

JuliaDistributedBackend(
    procs=nothing,
    nparts=nothing,
    partition_strategy=:roundrobin,
    threaded_per_worker=false,
    warmup_workers=true,
)

Distributed execution over Julia worker processes.

Parameters

• procs: worker IDs (defaults to Distributed.workers()).
• nparts: number of partitions (defaults to number of workers).
• partition_strategy: how to split states (:roundrobin or :contiguous).
• threaded_per_worker: enable threading inside each worker.
• warmup_workers: run a small warm-up to reduce compilation overhead.

SlurmArrayBackend(
    nchunks,
    chunk_id=nothing,
    outdir,
    partition_strategy=:contiguous,
    write_only=true,
)

Execution using SLURM array jobs (file-based parallelism).

Parameters

• nchunks: total number of chunks (slurm array size).
• chunk_id: current chunk (defaults to SLURM_ARRAY_TASK_ID).
• outdir: directory where results are written.
• partition_strategy: how to split states (:contiguous or :roundrobin).
• write_only: if true, only writes transitions to disk (recommended for SLURM).