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.

AbstractLift

A composable, optional generalization applied to a base AbstractSymbolicModel: it adds one factor (an extra axis) to the abstraction. Concrete lifts:

• ClockLift — adds a monotone time axis t;
• a mode lift (planned) — adds the hybrid mode axis k.

The four abstractions x, (x,t), (x,k), (x,k,t) are obtained by applying zero, one, or both lifts to a base model. Each lift implements lift(l, model) (and, in a later phase, lift(l, spec) so specifications extend the same way).

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. HybridSymbolicModel) subtype this root directly.

ClockAbstraction{N, T}

Symbolic abstraction of a 1-D monotone clock (the time axis of one mode of a timed hybrid system, or a standalone clock lifted onto a continuous model).

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

ClockAbstraction(domain, tstep::Float64)

Build an active ClockAbstraction directly from a 1-D time domain (a box interval) discretized with step tstep. Used to lift a continuous model with a clock (no time subsystem required).

ClockAbstraction(sys::ConstrainedLinearContinuousSystem, tstep)

Build a ClockAbstraction 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).

ClockLift{C} <: AbstractLift

The time lift: augments a base abstraction with a monotone clock ClockAbstraction, turning a model of x into a model of (x, t). The same lift applies to a plain continuous model or (per mode) to a hybrid mode, so it is the single reusable mechanism for time-dependent abstractions.

ClockLiftedSymbolicModel{B, C, A} <: AbstractSymbolicModel

Result of lift(::ClockLift, base): the synchronized product of a base model with a clock. Abstract states are the flattened (base_state_id, time_id) pairs; the concrete coordinate is the augmented vector [x; t] (time is the trailing dimension). For an active clock a base transition q → q′ is replicated as (q, p) → (q′, p+1) across time steps; a frozen clock keeps p fixed.

Inputs pass through to base unchanged (the clock adds no inputs).

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.

FlatIndex{K}

Bijection between composite keys of type K (e.g. an augmented-state tuple) and a dense integer range 1:n. Backs the flattened integer numbering used by product/lifted symbolic models.

Both directions are O(1): id_to_key is a plain vector (id → key), key_to_id a hash map (key → id). Absence is encoded by the id 0, so callers can branch on flat_id(...) > 0 without a second lookup.

FlatIndex(keys::AbstractVector{K}) -> FlatIndex{K}

Build a FlatIndex from a vector of unique keys, numbering them 1:length(keys) in order.

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_models, hs::HybridSystem)

Build the GlobalInputMap for a hybrid system from its per-mode symbolic models: 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

HybridSymbolicModel{Mods, A, G} <: AbstractSymbolicModel

Symbolic abstraction of a hybrid system, composed from one AbstractSymbolicModel per mode via a ModeLift. Each mode model is either a plain spatial abstraction (x) or a ClockLiftedSymbolicModel ((x, t)); the (local_state_id, mode_id) pairs are flattened to a single integer numbering and wired into one automaton, with inputs unified through a GlobalInputMap.

Fields

• mode_models: per-mode symbolic models.
• flat: FlatIndex bijection between the integer numbering and the (local_state_id, mode_id) pairs.
• automaton: the flattened transition automaton.
• input_mapping: the global input map.

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.

ModeLift{H, G} <: AbstractLift

The mode lift: composes one AbstractSymbolicModel per mode into a single HybridSymbolicModel, wiring the guarded, reset-coupled switches of the hybrid automaton hs and unifying inputs through input_mapping.

Unlike ClockLift — which lifts a single base model — ModeLift consumes a vector of per-mode base models (each plain or clock-lifted), so it is applied via lift(l, mode_models).

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.

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.

abstract_switch_target(mode_model, reset_coord) -> Int

Local abstract state of a guarded-switch target in mode_model, from the concrete coordinate produced by the reset map (0 if out of range). For a clock-lifted mode the coordinate is [x; t] and the time is rounded up (the smallest clock step ≥ t); for a time-free mode it is just x.

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

Embed each mode model's own transitions into the global list, relabelling inputs.

base_state_and_time(m::ClockLiftedSymbolicModel, id) -> (x, t)

Decompose a flattened id into the base concrete state x (unaugmented, keeping the base's coordinate type) and the clock value t. Used by the mode composition to build a hybrid coordinate without re-splitting the [x; t] vector.

build_all_transitions(hs, mode_models, input_mapping) -> Vector{HybridTransition}

Assemble every hybrid transition: intra-mode (each mode model's own transitions, which already encode any time advance) followed by inter-mode (guarded switches between modes).

build_symbolic_automaton(transition_list, mode_models, input_mapping) -> (flat, automaton)

Flatten the hybrid transitions into an IndexedAutomatonList, returning (flat, automaton) where flat is the FlatIndex between the integer numbering and the (local_id, mode_id) pairs.

ceil_time2int(tm::ClockAbstraction, 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.

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.

Flattened id of key, or 0 if the key is absent.

Key associated with flattened id id (bounds-checked by the caller).

floor_time2int(tm::ClockAbstraction, 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).

Abstract an augmented coordinate [x; t] to its flattened id (0 if absent).

get_abstract_state(model::HybridSymbolicModel, augmented_state) -> Int

Abstract a concrete augmented state ((x, t, mode) or (x, mode)) to its flattened index, or 0 if it is out of the abstraction's domain (unknown mode, or a spatial/time coordinate outside the grid). Callers that require a valid state (e.g. an initial state) should check for 0.

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

Concretize a flattened id to the augmented coordinate [x; t].

get_concrete_state(model::HybridSymbolicModel, state_index) -> (x[, t], mode_id)

Concretize a flattened state index to the augmented concrete state: (x, t, mode) for a clock-lifted mode, (x, mode) for a time-free mode.

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) hybrid states.

get_states_from_set(m::ClockLiftedSymbolicModel, set, incl_mode)

Flattened states whose spatial part lies in the projection of set onto the base coordinates and whose time index lies in the projection onto the trailing (time) dimension. set is a box over [x; t].

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

int2time(tm::ClockAbstraction, 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.

lift(l::AbstractLift, base::AbstractSymbolicModel) -> AbstractSymbolicModel

Apply the lift l to base, returning a symbolic model with one additional factor.

lift(l::ModeLift, mode_models) -> HybridSymbolicModel

Compose the per-mode mode_models (each plain or clock-lifted) into a hybrid symbolic model, assembling the intra-mode and guarded inter-mode transitions.

lift_per_slice(bases, clock) -> ClockLiftedSymbolicModel

Clock lift with per-time-slice dynamics: bases[p] is the spatial abstraction valid at clock step p — for time-varying dynamics f(x, u, t), the abstraction of f(·, ·, t_p). The transitions out of slice p come from bases[p], advancing the clock to p+1. All bases must share the same state/input grid (only their transitions differ), so any of them concretizes a (q, p) state.

For time-invariant dynamics, lift(ClockLift(clock), base) is the cheaper equivalent (one base replicated across every slice).

Number of flattened ids.

Clock-lifted model + base spec: matching base states at every time index.

Clock-lifted model + timed spec: matching base states within the time window.

Hybrid model + mode spec: per-mode local states mapped to global ids.

Abstract states of a base model satisfying a base state spec.