Symbolic

AbstractAutomatonList <: HybridSystems.AbstractAutomaton

Interface for the finite automaton backing a symbolic model: a set of transitions over integer states and input symbols. Transitions are stored and enumerated as (target, source, symbol) tuples (see TransitionKey).

Extending

Implement get_n_state, get_n_input, enum_transitions, add_transition!, pre, post and Base.empty!. Concrete implementations trade memory for pre/post speed: SortedAutomatonList (compact, sorted-set backed), IndexedAutomatonList (dict indices) and FastIndexedAutomatonList (dense vector indices).

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.

AbstractSymbolicModel

Root of the symbolic-model hierarchy: anything that owns a finite automaton (get_automaton). Models with a single concrete state/input space of fixed dimension subtype SymbolicModel{N, M}; models whose spaces vary per mode (e.g. TimedHybridSymbolicModel) subtype this root directly.

FastIndexedAutomatonList <: AbstractAutomatonList

Automaton with dense vector indices: postmap is keyed by the flattened (state, symbol) pair and premap by target state, so post/pre are direct array lookups. Fastest to query and densest in memory; best for large fixed automata. Call finalize! after bulk insertion to deduplicate.

GlobalInputMap

Bijection between per-mode local input ids and a single global input alphabet for a timed hybrid system. Continuous inputs (one block per mode) occupy continuous_range; switching inputs (one per hybrid-automaton transition) occupy switching_range.

Fields

• total_inputs, continuous_inputs, switching_inputs: counts.
• continuous_to_global / global_to_continuous: (mode_id, local_input_id) ↔ global_id.
• switching_to_global / global_to_switching: transition_id ↔ global_id.
• continuous_range, switching_range: the id ranges of each block.
• switch_labels: human-readable "SWITCH src -> tgt" label per switching input.

GlobalInputMap(mode_abstractions, hs::HybridSystem)

Build the GlobalInputMap for a hybrid system from its per-mode (symbolic_dynamics, symbolic_time) abstractions: continuous inputs are laid out mode by mode, then one switching input per hybrid-automaton transition.

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
• state set (Xset): states enumerated as sources
• retained set (Rset): states allowed as targets

IndexedAutomatonList <: AbstractAutomatonList

Automaton that maintains dictionary indices (postmap, premap) alongside the transition list, giving O(1) post(q, u) and pre(q′) at the cost of extra memory. Suited to repeated fixed-point queries on a fixed automaton.

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

Distributed execution over Julia worker processes. Each worker receives its share of the work in a single remotecall carrying the symbolic model and the approximation explicitly — there is no per-worker global state to install or clear, and workers JIT-compile in parallel inside their call.

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.

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.

SequentialBackend()

Sequential execution (no parallelism).

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

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

SortedAutomatonList <: AbstractAutomatonList

Automaton backed by a sorted tuple set of (target, source, symbol) transitions. Compact and cheap to build; pre/post are answered by range queries on the sorted set. Good default when memory matters.

Abstract Type: SymbolicModel{N, M}

Defines a generic symbolic model interface, where:

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

SymbolicModelList:

• X: source states bundled with the state mapping (MP.MappedStateSet)
• R: allowed target states, same state mapping ("relation universe allowance")
• U: inputs considered, bundled with the input mapping

ThreadedBackend(progress_dt=0.2)

Multithreaded execution using all available Julia threads.

TimeSymbolicModel{N, T}

Symbolic abstraction of the time axis for one mode of a timed hybrid system.

tsteps are the discretized time values; time_domain is the concrete time domain X; is_time_active distinguishes an evolving clock (ẋ = 1, matrix A = I) from a frozen one (A = 0).

TimeSymbolicModel(sys::ConstrainedLinearContinuousSystem, tstep)

Build a TimeSymbolicModel from a linear time subsystem. The dynamics matrix A must be the identity (time evolves, discretized with step tstep over the box time domain) or zero (time frozen, a single step at 0.0).

TimedHybridSymbolicModel{S1, A, T, G} <: AbstractSymbolicModel

Symbolic abstraction of a timed hybrid system. Each mode contributes a spatial dynamics abstraction and a TimeSymbolicModel; the augmented states (state_id, time_id, mode_id) are flattened to a single integer numbering and wired into one automaton, with inputs unified through a GlobalInputMap.

Fields

• mode_abstractions: per-mode spatial dynamics symbolic models.
• time_abstractions: per-mode time symbolic models.
• state_index_to_augmented / augmented_to_state_index: integer ↔ augmented state.
• symbolic_automaton: the flattened transition automaton.
• input_mapping: the global input map.

TransitionKey = NTuple{3, Int}

A transition, stored and enumerated as (target, source, symbol). Note the ordering flip vs. add_transition!(autom, source, target, symbol), whose arguments put the source first. Prefer the transition_target/transition_source/transition_symbol accessors over raw positional indexing at call sites.

Add the guarded mode-switch transitions using each transition's guard and reset map.

Add the within-mode transitions (spatial dynamics advanced across each time step).

build_all_transitions(hs, mode_abstractions, input_mapping) -> Vector{TransitionTuple}

Assemble every augmented transition of the timed hybrid system: intra-mode (dynamics × time steps within each mode) followed by inter-mode (guarded switches between modes).

build_symbolic_automaton(transition_list, mode_abstractions, input_mapping)

Flatten the augmented transitions into an IndexedAutomatonList, returning (state_index_to_augmented, augmented_to_state_index, automaton).

ceil_time2int(tm::TimeSymbolicModel, t) -> Int

Index of the smallest time step ≥ t (always 1 when time is frozen).

Append the successors of (source, symbol) to targetlist in place.

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.

Enumerate the local input ids of mode_id.

Spatial part (all but the last dimension) of a box guard.

Temporal part [t_min, t_max] (last dimension) of a box guard.

finalize!(autom::AbstractAutomatonList)

Compact the automaton after bulk transition insertion (e.g. deduplicate index entries). The generic fallback is a no-op; implementations that accumulate duplicates override it. Returns the automaton.

find_symbolic_state(symmodel, continuous_state) -> Int

Abstract-state index of continuous_state in a per-mode dynamics model, or 0 if the state is empty/nothing or has no valid abstraction.

floor_time2int(tm::TimeSymbolicModel, t) -> Int

Index of the largest time step ≤ t (always 1 when time is frozen).

Abstract a concrete input in mode_id to its global input id (0 if not found).

get_abstract_state(model::TimedHybridSymbolicModel, (x, t, mode_id)) -> Int

Abstract a concrete augmented state to its flattened index (0 if the augmented key is not present in the model).

Concretize global input input_id in mode_id (nothing for switching inputs).

get_concrete_state(model::TimedHybridSymbolicModel, state_index) -> (x, t, mode_id)

Concretize a flattened state index to (continuous_state, time_value, mode_id).

Global input id of a local continuous input (mode_id, local_input_id) (0 if absent).

get_local_input_info(gim::GlobalInputMap, global_id) -> (kind, info)

Classify a global input id: returns (:continuous, (mode_id, local_input_id)), (:switching, transition_id), or (:invalid, nothing).

Total number of global inputs (continuous + switching).

Number of (flattened) augmented states.

get_states_from_set(model, state_sets, time_sets, mode_indices; domain=MP.INNER)

For each mode in mode_indices, collect the flattened state indices whose spatial part lies in state_sets[idx] and whose time index lies in time_sets[idx].

Global input id of the switching input for transition_id (0 if absent).

Time indices of time_model falling within the [t_min, t_max] interval.

int2time(tm::TimeSymbolicModel, idx) -> Float64

Time value at index idx (always 0.0 when time is frozen).

Whether global_id is a continuous input.

Whether global_id is a switching input.