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, U, OS} <: 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.

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