AA228V/CS238V
Validation of Safety-Critical Systems

Lecture 04: Property Specification
Sydney Katz (smkatz@stanford.edu)

Property specification allows us to formally specify what a system should do.

Properties of Systems

System Behavior

Real Number

Metrics

Boolean Value

Specifications

Properties of Systems

Sometimes we derive specifications from metrics.

Properties of Systems

Sometimes we derive specifications from metrics.

Properties of Systems

Sometimes we derive specifications from metrics.

Sometimes we derive metrics from specifications.

Properties of Systems

single trajectory

multiple trajectories

Plan for Today

1

Properties of Systems

2

Metrics

3

Specifications

4

Reachability

distribution over trajectories: $p(\tau )$

distribution over trajectories: $p(\tau )$

distribution over miss distances

expected miss
distance

Note: more on this in chapter 7!

Expected value often is not enough to summarize a distribution.

expected miss
distance

expected miss
distance

expected miss
distance

These distributions have the same expected value but differ in their variance.

In safety-critical settings, we often want more conservative metrics that focus on worst-case outcomes.

In safety-critical settings, we often want more conservative metrics that focus on worst-case outcomes.

Risk metric: metric in which higher values indicate worse outcomes.

In safety-critical settings, we often want more conservative metrics that focus on worst-case outcomes.

Risk metric: metric in which higher values indicate worse outcomes.

e.g. loss of separation: $f(\tau )=2000\text{ meters }-\text{ miss distance}(\tau )$

In safety-critical settings, we often want more conservative metrics that focus on worst-case outcomes.

Risk metric: metric in which higher values indicate worse outcomes.

e.g. loss of separation: $f(\tau )=2000\text{ meters }-\text{ miss distance}(\tau )$

most risky

least risky

The value at risk (VaR) is the highest value that the risk is guaranteed not to exceed with probability $\alpha$.

i.e. the $\alpha$-quantile of the distribution over the risk metric

In safety-critical settings, we often want more conservative metrics that focus on worst-case outcomes.

Risk metric: metric in which higher values indicate worse outcomes.

e.g. loss of separation: $f(\tau )=2000\text{ meters }-\text{ miss distance}(\tau )$

most risky

least risky

Some intuition for VaR and CVaR

“What is the value that the risk is guaranteed
not to exceed with probability 0.7?”

The higher this value is, the worse the situation.

“I don’t just want the expected value - I want the
expected value of the worst-case outcomes.”

The higher this value is, the worse the situation.

Some intuition for VaR and CVaR

↺ Reset

Metrics are often at odds with one another.

A system design is Pareto optimal if we cannot improve one metric without worsening another.

Pareto optimal?

Metrics are often at odds with one another.

A system design is Pareto optimal if we cannot improve one metric without worsening another.

Pareto optimal?

Metrics are often at odds with one another.

A system design is Pareto optimal if we cannot improve one metric without worsening another.

The Pareto frontier is the subset of all designs that are Pareto optimal.

Metrics are often at odds with one another.

Composite metrics allow us to create a single metric to select a point on the Pareto frontier.

A system design is Pareto optimal if we cannot improve one metric without worsening another.

The Pareto frontier is the subset of all designs that are Pareto optimal.

Metrics are often at odds with one another.

Composite metrics allow us to create a single metric to select a point on the Pareto frontier.

Metrics are often at odds with one another.

Composite metrics allow us to create a single metric to select a point on the Pareto frontier.

Weighted Sum Method:

Metrics are often at odds with one another.

Composite metrics allow us to create a single metric to select a point on the Pareto frontier.

Weighted Sum Method:

Metrics are often at odds with one another.

Composite metrics allow us to create a single metric to select a point on the Pareto frontier.

Goal Distance Metric:

Metrics are often at odds with one another.

Composite metrics allow us to create a single metric to select a point on the Pareto frontier.

Goal Distance Metric:

Why not combine the two?

Weighted Exponential Sum Metric:

How do we pick the weights?

How do we pick the weights?

One option is preference elicitation.

Candy Example

We want to learn a weight vector over the following three candies:

1.  M&Ms $(w_1)$
2.  Sour Patch Kids $(w_2)$
3.  Skittles $(w_3)$

We will do so using pairwise queries.

Candy Example

Candy Example

Candy Example

Candy Example

In this case, we preselected the queries. We would probably do better if we selected the queries as we went to maximize the amount of information they provide! (lots of research on preference-based learning, beyond the scope of this class)

We also assumed that the expert was perfectly rational. It is common to relax this assumption and instead compute a distribution over the weights. (beyond the scope of this class)

Plan for Today

1

Properties of Systems

2

Metrics

3

Specifications

4

Reachability

A logical specification formally defines an operating requirement for a system using a logical formula.

A logical specification formally defines an operating requirement for a system using a logical formula.

A logical formula is a precise expression that evaluates to either true or false.

Propositional Logic

Propositional Logic

A proposition is a statement that evaluates to either true or false.

An atomic proposition is a proposition that cannot be broken down further.

Propositional Logic

A proposition is a statement that evaluates to either true or false.

An atomic proposition is a proposition that cannot be broken down further.

Propositional Logic

A proposition is a statement that evaluates to either true or false.

An atomic proposition is a proposition that cannot be broken down further.

“A and B and not C”

Propositional Logic

Propositional Logic

Example

Express the following statement using propositional logic:

“If the agent is in a safe state, then the agent is not in a collision state”

Atomic propositions:

$S$: the agent is in a safe state

$C$: the agent is in a collision state

Propositional Logic

Propositional Logic

First-Order Logic

First-Order Logic

First-order logic adds variables, predicates, and quantifiers to propositional logic.

First-Order Logic

First-order logic adds variables, predicates, and quantifiers to propositional logic.

First-Order Logic

First-order logic adds variables, predicates, and quantifiers to propositional logic.

First-Order Logic

First-order logic adds variables, predicates, and quantifiers to propositional logic.

quantifiers allow us to evaluate propositions over a collection of variables

Universal Quantifier $\forall$ (“for all”): all variables must satisfy the proposition.

Existential Quantifier $\exists$ (“there exists”): at least one variable in the domain satisfies the proposition.

First-Order Logic

Example

“for all states in the trajectory, the
agent does not hit an obstacle”

$O(x)$: $x$ is an obstacle state

First-Order Logic

Example

“the agent must reach a goal state and
avoid the obstacle state.”

$O(x)$: $x$ is an obstacle state

$G(x)$: $x$ is a goal state

Propositional Logic

First-Order Logic

Propositional Logic

First-Order Logic

Temporal Logic

Temporal Logic

Temporal logic extends first-order logic to specify properties over time.

Linear

Temporal Logic

Properties over linear sequences of states:

“always $P$”

“$P$ is true at all time
steps in the future”

“eventually $P$”

“$P$ is true at some time
step in the future”

“$P$ until $Q$”

“$Q$ is true at some time step in
the future and $P$ is true at least
until $Q$ becomes true.”

Linear

Temporal Logic

Example

“eventually reach the goal after
passing through the checkpoint and
always avoid the obstacle”

$F(s_t):$ the state $s$ at time $t$ contains an obstacle

$G(s_t):$ the state $s$ at time $t$ is the goal

$C(s_t):$ the state $s$ at time $t$ is the checkpoint

$\psi =$ $◊G$ $\wedge$ $\neg G\mathcal{U}C$ $\wedge$ $\square \neg F$

Linear

Temporal Logic

Example

“eventually reach the goal after
passing through the checkpoint and
always avoid the obstacle”

$F(s_t):$ the state $s$ at time $t$ contains an obstacle

$G(s_t):$ the state $s$ at time $t$ is the goal

$C(s_t):$ the state $s$ at time $t$ is the checkpoint

$\psi =$ $◊G$ $\wedge$ $\neg G\mathcal{U}C$ $\wedge$ $\square \neg F$

Linear

Temporal Logic

Example

“eventually reach the goal after
passing through the checkpoint and
always avoid the obstacle”

$F(s_t):$ the state $s$ at time $t$ contains an obstacle

$G(s_t):$ the state $s$ at time $t$ is the goal

$C(s_t):$ the state $s$ at time $t$ is the checkpoint

$\psi =$ $◊G$ $\wedge$ $\neg G\mathcal{U}C$ $\wedge$ $\square \neg F$

Linear

Temporal Logic

Example

“eventually reach the goal after
passing through the checkpoint and
always avoid the obstacle”

$F(s_t):$ the state $s$ at time $t$ contains an obstacle

$G(s_t):$ the state $s$ at time $t$ is the goal

$C(s_t):$ the state $s$ at time $t$ is the checkpoint

$\psi =$ $◊G$ $\wedge$ $\neg G\mathcal{U}C$ $\wedge$ $\square \neg F$

Signal

Linear

Temporal Logic

Signal

Linear

Temporal Logic

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

1

2

allows us to specify properties over a time interval $[a,b]$

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

1

2

allows us to specify properties over a time interval $[a,b]$

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

1

2

allows us to specify properties over a time interval $[a,b]$

allows us to map real-valued signals to truth values: ${\mu }_c(s_t)$ is true if $\mu (s_t)>c$

Signal

Temporal Logic

extends linear temporal logic to real-valued signals

Time

Value

1

2

allows us to specify properties over a time interval $[a,b]$

allows us to map real-valued signals to truth values: ${\mu }_c(s_t)$ is true if $\mu (s_t)>c$

Important stuff we will use for the rest of the course about to happen!

i.e. $P$ is true if $s_t>c$

i.e. $P$ is true if $s_t>c$

i.e. $P$ is true if $s_t>c$

This:

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness $\rho$

i.e. $P$ is true if $s_t>c$

Robustness of propositional
logic operators:

i.e. $P$ is true if $s_t>c$

Robustness of propositional
logic operators:

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Robustness of propositional
logic operators:

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Robustness of propositional
logic operators:

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Robustness of propositional
logic operators:

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Robustness of propositional
logic operators:

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Robustness of propositional
logic operators:

Robustness of Temporal Operators

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Robustness of Temporal Operators

i.e. $P$ is true if $s_t>c$

i.e. $Q$ is true if $s_t>d$

Yay! But there is still one problem we need to solve:

Yay! But there is still one problem we need to solve:

Later in this course, we will want to take the gradient of the robustness with respect to the trajectory inputs.

Yay! But there is still one problem we need to solve:

Later in this course, we will want to take the gradient of the robustness with respect to the trajectory inputs.

But all those maxes and mins in the robustness formulas result in not-so-nice gradients.

Propositional Operators

Temporal Operators

i.e. $P$ is true if $s_t>c$

i.e. $P$ is true if $s_t>c$

This is not a very interesting or useful gradient.

The fix: smooth robustness

The fix: smooth robustness

smooth robustness replaces the min and max operators in softmin and softmax

↺ Reset

Plan for Today

1

Properties of Systems

2

Metrics

3

Specifications

4

Reachability

Reachability

Target Set ${\mathcal{S}}_T$

Reachability

$R(s_t):$ true if $s_t\in {\mathcal{S}}_T$ and false otherwise

Target Set ${\mathcal{S}}_T$

Reachability

$R(s_t):$ true if $s_t\in {\mathcal{S}}_T$ and false otherwise

Reachability

$R(s_t):$ true if $s_t\in {\mathcal{S}}_T$ and false otherwise

Reachability

$R(s_t):$ true if $s_t\in {\mathcal{S}}_T$ and false otherwise

$G:$ the robot reaches the goal

$C:$ the robot reaches the checkpoint

This formulation fails to take into account that both the checkpoint and goal must be reached and that they must be reached in a particular order.

Reachability

$R(s_t):$ true if $s_t\in {\mathcal{S}}_T$ and false otherwise

$G:$ the robot reaches the goal

$C:$ the robot reaches the checkpoint