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}

An intermediate abstract type for symbolic models that rely on a grid-based discretization.

• N: Dimension of the state space.
• M: Dimension of the input space.

SymbolicModelList{N, M, S1, S2, A} <: GridBasedSymbolicModel{N, M}

A classical symbolic model where the entire domain is partitioned into grid cells.

LazySymbolicModel{N, M, S1, S2, A} <: GridBasedSymbolicModel{N, M}

A symbolic model using lazy abstraction where the automaton is computed only for a subset of the state space.

compute_symmodel_from_hybridcontrolsystem!(symmodel::SymbolicModel{N}, transitionCost::AbstractDict, transitionCont::AbstractDict,
hybridsys::AbstractHybridSystem, W, L, U, opt_sdp, opt_qp)

Builds an abstraction symmodel where the transitions have costs given in transitionCost and are parameterized by affine-feedback controllers in transitionCont. The concrete system is hybridsys and W, L and U are defined as in _has_transition. An SDP optimizer opt_sdp and a QP optimizer opt_qp must be provided as JuMP optimizers.

is_deterministic(symmodel::SymbolicModelList) -> Bool

Returns true if the symbolic model is deterministic.

A symbolic model is deterministic if, for every (state, input) pair, there is at most one successor.

determinize_symbolic_model(symmodel::SymbolicModelList) -> SymbolicModelList

Returns a determinized version of the given symbolic model by encoding each transition input as a pair (input_symbol, target_state).

This transformation removes nondeterminism by lifting the input space: each original input is paired with its intended target, making transitions unique.

Arguments

• symmodel: A SymbolicModelList that may contain nondeterministic transitions.

Returns

• A new SymbolicModelList that is deterministic, with:
  • New unique inputs: (symbol, target) pairs.
  • Transitions remapped to be deterministic.
  • metadata[:original_symmodel] containing a reference to the original model.

Notes

• The determinized model will have more inputs than the original.

Example

det_symmodel = determinize_symbolic_model(symmodel)
is_deterministic(det_symmodel) == true