Properties

Abstract supertype of properties that can be checked.

Every concrete subtype should provide the following functions:

• dim(𝑃::Property)::Int
• check(𝑃::Property, X::LazySet; witness::Bool=false)

Conjunction <: Property

Type that represents a conjunction of properties.

Fields

• conjuncts – vector of properties

Notes

The following formula characterizes whether a set $X$ satisfies a disjunction $𝑃 = 𝑃_1 ∧ 𝑃_2 ∧ … ∧ 𝑃_m$:

dim(𝑃::Conjunction)::Int

Return the dimension of a conjunction of properties.

Input

• 𝑃 – conjunction of properties

Output

The dimension of the conjunction of properties.

check(𝑃::Conjunction, X::LazySet{N}; witness::Bool=false) where {N<:Real}

Check whether a convex set satisfies a conjunction of properties.

Input

• 𝑃 – conjunction of properties
• X – convex set
• witness – (optional, default: false) flag for returning a counterexample if the property is violated

Output

• If witness option is deactivated: true iff X satisfies the property 𝑃
• If witness option is activated:
  • (true, []) iff X satisfies the property 𝑃
  • (false, v) iff X does not satisfy the property 𝑃 with witness v

Notes

By convention, the empty conjunction is equivalent to true and hence is satisfied by any set.

Disjunction <: Property

Type that represents a disjunction of properties.

Fields

• disjuncts – vector of properties (elements are reordered by this type)
• reorder – flag to indicate whether shuffling is allowed

Notes

The following formula characterizes whether a set $X$ satisfies a disjunction $𝑃 = 𝑃_1 ∨ 𝑃_2 ∨ … ∨ 𝑃_m$:

If the reorder flag is set, the disjuncts may be reordered after each call to check as a heuristics to make subsequent checks faster.

dim(𝑃::Disjunction)::Int

Return the dimension of a disjunction of properties.

Input

• 𝑃 – disjunction of properties

Output

The dimension of the disjunction of properties.

check(𝑃::Disjunction, X::LazySet{N}; witness::Bool=false) where {N<:Real}

Check whether a convex set satisfies a disjunction of properties.

Input

• 𝑃 – disjunction of properties
• X – convex set
• witness – (optional, default: false) flag for returning a counterexample if the property is violated

Output

• If witness option is deactivated: true iff X satisfies the property 𝑃
• If witness option is activated:
  • (true, []) iff X satisfies the property 𝑃
  • (false, v) iff X does not satisfy the property 𝑃 with witness v; note that v == N[] if 𝑃 is the empty disjunction

Notes

By convention, the empty disjunction is equivalent to false and hence is satisfied by no set.

If the 𝑃.reorder flag is set, the disjuncts may be reordered as a heuristics to make subsequent checks faster. Since we check satisfaction from left to right, we move the disjunct for which satisfaction was established to the front.

To be consistent with other propertes, the witness option only returns one counterexample, namely for the left-most disjunct in the disjuncts vector. We deactivate witness production for checking the remaining disjuncts.

SafeStatesProperty{N<:Real} <: Property

Type that represents a safety property characterized by a set of safe states. The property is satisfied by a given set of states $X$ if $X$ is fully contained in the set of safe states.

Fields

• safe – convex set representing the safe states
• witness – witness point (empty vector if not set)

Notes

The following formula characterizes whether a set $X$ satisfies a safety property characterized by a set of safe states 𝑃:

dim(𝑃::SafeStatesProperty)::Int

Return the dimension of a property with safe states.

Input

• 𝑃 – safety property with safe states

Output

The dimension of the safe states.

check(𝑃::SafeStatesProperty, X::LazySet; witness::Bool=false)

Checks whether a convex set is contained in the set of safe states.

Input

• 𝑃 – safety property with safe states
• X – convex set
• witness – (optional, default: false) flag for returning a counterexample if the property is violated

Output

Let $Y$ be the safe states represented by 𝑃.

• If witness option is deactivated: true iff $X ⊆ Y$
• If witness option is activated:
  • (true, []) iff $X ⊆ Y$
  • (false, v) iff $X ⊈ Y$ and $v ∈ X \setminus Y$

BadStatesProperty{N<:Real} <: Property

Type that represents a safety property characterized by a set of bad states. The property is satisfied by a given set of states if the intersection with the set of bad states is empty.

Fields

• bad – convex set representing the bad states
• witness – witness point (empty vector if not set)

Notes

The following formula characterizes whether a set $X$ satisfies a safety property characterized by a set of bad states 𝑃:

dim(𝑃::BadStatesProperty)::Int

Return the dimension of a property with bad states.

Input

• 𝑃 – safety property with bad states

Output

The dimension of the bad states.

check(𝑃::BadStatesProperty, X::LazySet; witness::Bool=false)

Checks whether a convex set is disjoint from the set of bad states.

Input

• 𝑃 – safety property with bad states
• X – convex set
• witness – (optional, default: false) flag for returning a counterexample if the property is violated

Output

Let $Y$ be the bad states represented by 𝑃.

• If witness option is deactivated: true iff $X ∩ Y = ∅$
• If witness option is activated:
  • (true, []) iff $X ∩ Y = ∅$
  • (false, v) iff $X ∩ Y ≠ ∅$ and $v ∈ X ∩ Y$