subsecref subsecname = thmref thmname = theorem lemref lemname = lemma

# Uncertainty in Monotone Co-Design Problems

Andrea Censi This paper was recommended for publication by Editor Kevin Lynch
upon evaluation of the Associate Editor and Reviewers’ comments.This work was
supported by the National Science Foundation, National Robotics Initiative,
award 1405259.Andrea Censi<EMAIL_ADDRESS>is with the Institute for Dynamic
Systems and Control at ETH Zürich. This work was performed while the author
was with the Laboratory for Information and Decision Systems (LIDS) at the
Massachusetts Institute of Technology. Digital Object Identifier (DOI): see
top of this page.

###### Abstract

This work contributes to a compositional theory of “co-design” that allows to
optimally design a robotic platform. In this framework, the user describes
each subsystem as a monotone relation between “functionality” provided and
“resources” required. These models can be easily composed to express the co-
design constraints among different subsystems. The user then queries the
model, to obtain the design with minimal resources usage, subject to a lower
bound on the provided functionality. This paper concerns the introduction of
uncertainty in the framework. Uncertainty has two roles: first, it allows to
deal with limited knowledge of the models; second, it also can be used to
generate consistent relaxations of a problem, as the computation requirements
can be lowered, should the user accept some uncertainty in the answer.

###### Index Terms:

Co-Design; Optimization and Optimal Control; Formal Methods for Robotics

##  I Introduction

(a) Part of a co-design diagram for a UAV. (b) Uncertain design problems

Figure 1: _Panel_ _a_ : Monotone Co-Design Problems capture the co-design
constraints among the components of a complex design, by describing _design
problems_ for each component in isolation and _co-design constraints_ among
different components. The co-design diagram in the figure describes part of
the design problem for a UAV, and in particular how the _resources_ (total
mass and cost) are related to the _functionality_ (distance, payload, number
of missions). Functionality edges are green and solid; resources are red and
dotted. _Panel_ _b_ : This paper describes how to introduce uncertainty in
this framework, which allows, for example, to introduce parametric uncertainty
in the definition of components properties (e.g. specific cost of batteries).
An Uncertain Design Problem (UDP) is described by a pair of functions from
functionality to subset of resources that give an upper and lower bound on the
resource consumption.

The design of a robotic platform involves the choice and configuration of many
hardware and software subsystems (actuation, energetics, perception, control,
…) in an harmonious entity. Because robotics is a young discipline, there is
still little work towards obtaining systematic procedures to derive optimal
designs. Therefore, robot design is a lengthly process based on empirical
evaluation and trial and error.

The work presented here contributes to a theory of co-design [1, 2] that
allows to optimally design a robotic platform based on formal models of its
subsystems. The goal is to allow a designer to create better designs, faster.
This work on “co-design” is related to and complementary to works that deal
with “co-generation” (the ability of synthesizing hardware and software
blueprints for entire robot platforms) [3, 4].

This paper describes the introduction of uncertainty in the theory developed
so far. In this framework, the user defines “design problems” for each
physical or logical subsystem. Each design problem (DP) is a relation between
“functionality” provided and “resources” required by the component. The DPs
can then composed in a graph, where each edge represents a “co-design
constraint” between two DPs _._ The resulting class of problems is called
Monotone Co-Design Problems (MCDPs).

An example of MCDP is sketched in Fig. 1a. The design problem consists in
finding an optimal configuration of a UAV, optimizing over actuators, sensors,
processors, and batteries. In this simplified example, the functionality of
the UAV is parameterized by three numbers: the distance to travel for each
mission; the payload to transport; the number of missions to fly. The optimal
design is defined as the one that satisfies the functionality constraints
while using the minimal amount of resources (cost and mass). In the figure,
the model is exploded to show how actuation and energetics are modeled.
Perception is modeled as a relation between the velocity of the platform and
the power required (the faster the platform, the more data needs to be
processed). Actuation is modeled as a relation between lift and power/cost.
Batteries are described by a relation between capacity and mass/cost. In this
example, there are different battery technologies (LiPo, etc.), each specified
by specific energy, specific cost, and lifetime, thus characterized by a
different relation between capacity, number of missions and mass and cost. The
interconnection between design problems describe the “co-design constraints”,
which could be recursive: e.g., actuators must lift the batteries, the
batteries must power the actuators. Cycles represent design problems that are
coupled.

Once the model is defined, it can be queried to obtain the _minimal_ solution
in terms of resources — here, total cost and total mass. The output to the
user is the Pareto front containing all non-dominated solutions. The
corresponding optimization problem is, in general, nonconvex. Yet, with few
assumptions, it is possible to obtain a systematic solution procedure, and
show that there exists a dynamical system whose fixed point corresponds to the
set of minimal solutions.

This paper describes how to add a notion of _uncertainty_ in the MCDP
framework. The model of uncertainty considered is interval uncertainty on
arbitrary partial orders. For a partially ordered set (poset)
$\left\langle\mathcal{P},\preceq\right\rangle$, these are sets of the type
$\\{x\in\mathcal{P}\colon a\preceq x\preceq b\\}$. I will show how one can
introduce this type of uncertainty in the MCDP framework by considering
ordered pairs of design problems. Each pair describes lower and upper bounds
for resources usage. These _uncertain design problems_ (UDPs) can be composed
using series, parallel, and feedback interconnection, just like their non-
uncertain counterparts.

The output to the user is _two_ Pareto fronts, describing the minimal resource
consumptions in the best case and in the worst case according to the models
specified. One or both the Pareto fronts can be empty, meaning that the
problem does not have a feasible solution.

This is different from the usual formalization of “robust optimization” [5,
6], usually formulated as a “worst case” analysis, in which the uncertainty in
the problem is described by a set of possible parameters, and the optimization
problem is posed as finding the one design that is valid for all cases.

Uncertainty plays two roles: it can be used as a _modeling_ _tool_ , where the
relations are uncertain because of our limited knowledge, and it can be used
as a _computational_ _tool_ , in which we deliberately choose to consider
uncertain relations as a relaxation of the problem, to reduce the
computational load, while maintaining precise consistency guarantees. With
these additions, the MCDP framework can describe even richer design problems
and to efficiently solve them.

#### Paper organization

Section II and III summarize previous work. They give a formal definition of
design problems (DPs) and their composition, called Monotone Co-Design
Problems (MCDPs). Section IV through VI describe the notion of Uncertain
Design Problem (UDP), the semantics of their interconnection, and the general
theoretical results. Section VII describes three specific applications of the
theory with numerical results. The supplementary materials (also available as
[7]) include detailed models written in MCDPL and pointers to obtain the
source code and a virtual machine for reproducing the experiments.

##  II Design Problems

_A design problem_ (DP) is a monotone relation between _provided
functionality_ and _required resources_. Functionality and resources are
complete partial orders (CPO) [8], denoted
$\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}},\preceq_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}}\rangle$
and
$\langle{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}},\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}\rangle$.
The graphical representations uses nodes for DPs and green and red edges for
functionality and resources.

Figure 2: Modeling a battery as a _design problem._

######  Example 1.

The first-order characterization of a battery is as a store of energy, in
which the capacity [kWh] is the functionality (what the battery provides) and
mass [kg] and cost [$] are resources (what the battery requires) (Fig. 2).

For a fixed functionality
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}\in{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}$,
the set of minimal resources in
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}$
sufficient to perform the functionality might contain two or more elements
that are incomparable with respect to
$\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$.
For example, in the case of a battery, one might consider different battery
technologies that are incomparable in the mass/cost resource space.

A subset with “minimal”, “incomparable” elements is called “antichain”. This
is the mathematical formalization of what is informally called a “Pareto
front”.

######  Definition 2.

An _antichain_ $S$ in a poset $\left\langle\mathcal{P},\preceq\right\rangle$
is a subset of $\mathcal{P}$ such that no element of $S$ dominates another
element: for all $x,y\in S$ and $x\preceq y$, then $x=y$.

######  Lemma 3.

Let $\mathsf{A}\mathcal{P}$ be the set of antichains of $\mathcal{P}$.
$\mathsf{A}\mathcal{P}$ is a poset itself, with the partial order
$\preceq_{\mathsf{A}\mathcal{P}}$ defined as

$S_{1}\preceq_{\mathsf{A}\mathcal{P}}S_{2}\ \equiv\ \uparrow
S_{1}\supseteq\,\uparrow S_{2},$ (1)

where “$\uparrow$” denotes the upper closure of a set.

######  Definition 4.

A _design problem_(DP) is a tuple
$\left\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}\right\rangle$
such that
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}$
and
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}$
are CPOs, and
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$
is a monotone and Scott-continuous function ([9] or [2, Definition 11]). Each
functionality
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}$
(or vector of functionalities, if
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}$
is a product of posets) corresponds to an antichain of resources
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})\in{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$
(Fig. 3).

Figure 3: A DP is a represented by a map
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$
from functionality to antichains of resources.

Monotonicity implies that, if the functionality is increased, then the
required resources increase as well.

##  III Monotone Co-Design Problems

A Monotone Co-Design Problem (MCDP) is a multigraph of DPs. An edge between a
resource
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}$
of a DP and a functionality
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}$
of another denotes the partial order inequality constraint
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}\preceq{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}$.
Cycles and self-loops are allowed.

######  Example 5.

The MCDP in Fig. 4a is the interconnection of 3 DPs
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{c}.$
The semantics as an optimization problem is shown in Fig. 4b. We will also use
an “algebraic” representation, shown in Fig. 4c, and defined in Def. 6.

(a) Graphical representation

(b) Semantics as an optimization problem

(c) Algebraic representation

Figure 4: Three equivalent representations of an MCDP.

The functionality/resources parametrization is quite natural for many design
engineering domains. Moreover, it allows for quantitative optimization, in
contrast to qualitative modeling tools such as _function structure_ diagrams
[10]. All models considered may be nonlinear, in contrast to work such as
Suh’s theory of _axiomatic design_[11].

###  III-A Algebraic definition

Some of the proofs rely on an algebraic representation of the graph. Series-
parallel graphs (see, e.g., [12]) have widespread use in computer science.
Here, we add a third operator to be able to represent loops. In the algebraic
definition, the graph is a represented by a tree, where the leaves are the
nodes, and the junctions are one of three operators
($\mathsf{series},\mathsf{par},\mathsf{loop}$), as in Fig. 5. An equivalent
construction for network processes is given in Stefanescu [13]. Equivalently,
we are defining a symmetric traced monoidal category (see, e.g., [14] or [15]
for an introduction); note that the $\mathsf{loop}$ operator is related to the
“trace” operator, but not exactly equivalent, though they can be defined in
terms of each other.

(a) $\mathsf{series}(a,b)$ (b) $\mathsf{par}(a,b)$

(c) $\mathsf{loop}(a)$

Figure 5: The three operators used in the inductive definition of MCDPs.

Let us use a standard definition of “operators”, “terms”, and “atoms” (see,
e.g., [16, p.41]). Given a set of operators $\mathsf{ops}$ and a set of atoms
$\mathcal{A}$, let $\mathsf{Terms}(\mathsf{ops},\mathcal{A})$ be the set of
all inductively defined expressions. For example, if the operator set contains
only one operator $f$ with one argument, and there is only one atom $a$, then
the terms are $\mathsf{Terms}(\\{f\\},\\{a\\})=\\{a,f(a),f(f(a)),\dots\\}.$

######  Definition 6 (Algebraic definition of Monotone Co-Design Problems).

An MCDP is a tuple
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle$,
where:

  1. 1.

$\mathcal{A}$ is any set of atoms, to be used as labels.

  2. 2.

The term $\boldsymbol{\mathsf{T}}$ in the
$\\{\mathsf{series},\mathsf{par},\mathsf{loop}\\}$ algebra describes the
structure of the graph:

$\boldsymbol{\mathsf{T}}\in\mathsf{Terms}(\\{\mathsf{series},\mathsf{par},\mathsf{loop}\\},\mathcal{A}).$

  3. 3.

The _valuation_ $\boldsymbol{v}:\mathcal{A}\rightarrow\mathsf{DP}$ assigns a
DP to each atom.

######  Example 7.

The MCDP in Fig. 4a can be described by the atoms $\mathcal{A}=\\{a,b,c\\}$,
the term
$\boldsymbol{\mathsf{T}}=\mathsf{loop}(\mathsf{series}(a,\mathsf{par}(b,c)),$
plus the valuation
$\boldsymbol{v}:\\{a\mapsto{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a},b\mapsto{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b},c\mapsto{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{c}\\}.$
The tuple
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle$
for this example is shown in Fig. 4c.

###  III-B Semantics of MCDPs

We can now define the _semantics_ of an MCDP. The _semantics_ is a function
$\varphi$ that, given an algebraic definition of an MCDP, returns a
$\mathsf{DP}$. Thanks to the algebraic definition, to define $\varphi$, we
need to only define what happens in the base case (equation 2), and what
happens for each operator $\mathsf{series},\mathsf{par},\mathsf{loop}$
(equations 3–5).

######  Definition 8 (Semantics of MCDP).

Given an MCDP in algebraic form
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle$,
the semantics

$\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle\rrbracket\in\mathsf{DP}$

is defined as follows:
$\displaystyle\varphi\llbracket\left\langle\mathcal{A},a,\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle\doteq\boldsymbol{v}(a),\qquad\text{for all}\ a\in\mathcal{A},$
(2)
$\displaystyle\varphi\llbracket\left\langle\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle\doteq\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{1},\boldsymbol{v}\right\rangle\rrbracket\,\mathbin{\varocircle}\,\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{2},\boldsymbol{v}\right\rangle\rrbracket,$
(3)
$\displaystyle\varphi\llbracket\left\langle\mathcal{A},\mathsf{par}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle\doteq\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{1},\boldsymbol{v}\right\rangle\rrbracket\,\mathbin{\varotimes}\,\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{2},\boldsymbol{v}\right\rangle\rrbracket,$
(4)
$\displaystyle\varphi\llbracket\left\langle\mathcal{A},\mathsf{loop}(\boldsymbol{\mathsf{T}}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle\doteq\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle\rrbracket^{\dagger}.$
(5)

The operators $\mathbin{\varocircle},\mathbin{\varotimes},\dagger$ are defined
in Def. 9–Def. 11. Please see [2, Section VI] for details about the
interpretation of these operators and how they are derived.

The $\mathbin{\varotimes}$ operator is a regular product in category theory:
we are considering all possible combinations of resources required by
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}$
and
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}$.

######  Definition 9 (Product operator $\mathbin{\varotimes}$).

For two maps
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{1}$
and
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{2}$,
define

$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\mathbin{\varotimes}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}:({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}\times{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2})$
$\displaystyle\rightarrow\mathsf{A}({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}),$
$\displaystyle\left\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}\right\rangle$
$\displaystyle\mapsto{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})\mathbin{\boldsymbol{\times}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}),$

where $\mathbin{\boldsymbol{\times}}$ is the product of two antichains.

The $\mathbin{\varocircle}$ operator is similar to a convolution: fixed
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}$,
one evaluates the resources
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}\in{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})$,
and for each
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}$,
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1})$
is evaluated. Then the minimal elements are selected.

######  Definition 10 (Series operator $\mathbin{\varocircle}$).

For two maps
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{1}$
and
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{2}$,
if
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}={\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2}$
, define

$\displaystyle{\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\mathbin{\varocircle}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{2},$
$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}$
$\displaystyle\mapsto\operatorname*{Min}_{\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}}}\bigcup_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}\in{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}).$

The dagger operator $\dagger$ is actually a standard operator used in domain
theory (see, e.g., [9, II-2.29]).

######  Definition 11 (Loop operator $\dagger$).

For a map
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}\times{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$,
define

$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}^{\dagger}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}},$
$\displaystyle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}$
$\displaystyle\mapsto\mathsf{lfp}\left(\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}\right),$
(6)

where $\mathsf{lfp}$ is the least-fixed point operator, and
$\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}$
is

$\displaystyle\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}:{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}},$
$\displaystyle{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}$
$\displaystyle\mapsto\operatorname*{Min}_{\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}}\bigcup_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\in{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}})\
\cap\uparrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}.$

###  III-C Solution of MCDPs

Def. 8 gives a way to evaluate the map
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}$
for the graph, given the maps
$\\{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}{}_{a}\mid
a\in\mathcal{A}\\}$ for the leaves. Following those instructions, we can
compute
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})$,
and thus find the minimal resources needed for the entire MCDP.

######  Example 12.

The MCDP in Fig. 4a is so small that we can do this explicitly. From Def. 8,
we can compute the semantics as follows:

$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}$
$\displaystyle=\varphi\left\llbracket\langle\mathcal{A},\mathsf{loop}(\mathsf{series}(a,\mathsf{par}(b,c)),\boldsymbol{v}\rangle\right\rrbracket$
$\displaystyle=\left({\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}\,\mathbin{\varocircle}\,\left({\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}\,\mathbin{\varotimes}\,{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{c}\right)\right)^{\dagger}.$

Substituting the definitions 9–11 above, one finds that
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})=\mathsf{lfp}\left(\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}}\right),$
with

$\displaystyle\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}}:{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}},$
$\displaystyle{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}$
$\displaystyle\mapsto\bigcup_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\in{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}}\Big{[}\operatorname*{Min}_{\preceq}\uparrow\bigcup_{s\in{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}})}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}(s)\mathbin{\boldsymbol{\times}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{c}(s)\Big{]}\
\cap\uparrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}.$

The least fixed point equation can be solved using Kleene’s algorithm [8, CPO
Fixpoint theorem I, 8.15]. A dynamical system that computes the set of
solutions is given by

$\begin{cases}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}_{0}&\leftarrow\\{\bot_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}\\},\\\
{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}_{k+1}&\leftarrow\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}}({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}_{k}).\end{cases}$

The limit
$\sup{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}_{k}$
is the set of minimal solutions, which might be an empty set if the problem is
unfeasible for a particular value
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}$.

This dynamical system is a proper algorithm only if each step can be performed
with bounded computation. An example in which this is not the case are
relations that give an infinite number of solutions for each functionality.
For example, the very first DP appearing in Fig. 1a corresponds to the
relation
_${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\text{travel
distance}}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{velocity}}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{endurance}},$_
for which there are infinite numbers of pairs
$\langle{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{velocity}},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{endurance}}\rangle$
for each value of travel distance. The machinery developed in this paper will
make it possible to deal with these infinite-cardinality relations by
relaxation.

##  IV Uncertain Design Problems

This section describes the notion of Uncertain DPs (UDPs). UDPs are an ordered
pair of DPs that can be interpreted as upper and lower bounds for resource
consumptions (Fig. 1b). We will be able to propagate this interval uncertainty
through an arbitrary interconnection of DPs. The result presented to the user
will be a _pair_ of antichains — a lower and an upper bound for the resource
consumption.

###  IV-A Partial order $\preceq_{\mathsf{DP}}$

Being able to provide both upper and lower bounds comes from the fact that in
this framework everything is ordered – there is a poset of resources, lifted
to posets of antichains, which is lifted to posets of DPs, and finally, to the
poset of uncertain DPs.

The first step is defining a partial order $\preceq_{\mathsf{DP}}$ on
$\mathsf{DP}$.

######  Definition 13 (Partial order $\preceq_{\mathsf{DP}}$).

Consider two DPs
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$.
The DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}$
precedes
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}$
if it requires fewer resources for all functionality
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}$:

${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}\quad\equiv\quad{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}),\
\text{for all
}{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}\in{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}.$

Figure 6: The partial order $\preceq_{\mathsf{DP}}$ in the space of design
problems.

In this partial order, there is both a top $\top_{\mathsf{DP}}$ and a bottom
$\bot_{\mathsf{DP}}$, defined as follows:

$\displaystyle\bot_{\mathsf{DP}}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}},$
$\displaystyle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}$
$\displaystyle\mapsto\\{\bot_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}\\}.$

$\displaystyle\top_{\mathsf{DP}}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}},$
$\displaystyle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}$
$\displaystyle\mapsto\emptyset.$ (7)

$\bot_{\mathsf{DP}}$ means that any functionality can be done with zero
resources, and $\top_{\mathsf{DP}}$ means that the problem is always
infeasible (“the set of feasible resources is empty”).

###  IV-B Uncertain DPs (UDPs)

######  Definition 14 (Uncertain DPs).

An Uncertain DP (UDP) $\boldsymbol{u}$ is a pair of DPs
$\langle{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}\rangle$
such that
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u}\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}$
.

######  Definition 15 (Partial order $\preceq_{\mathsf{UDP}}$).

A UDP $\boldsymbol{u}_{a}$ precedes another UDP $\boldsymbol{u}_{b}$ if the
interval
$[{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u}_{a},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}_{a}]$
is contained in the interval
$[{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u}_{b},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}_{b}]$
(Fig. 7):

$\boldsymbol{u}_{a}\preceq_{\mathsf{UDP}}\boldsymbol{u}_{b}\quad\equiv\quad{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u}_{b}\preceq_{\mathsf{DP}}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u}_{a}\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}_{a}\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}_{b}.$

Figure 7: The partial order $\preceq_{\mathsf{UDP}}$ has a top
$\top_{\mathsf{UDP}}=\left\langle\bot_{\mathsf{DP}},\top_{\mathsf{DP}}\right\rangle.$
This pair describes the state of maximum uncertainty about the DP: we do not
know if the DP is feasible with 0 resources ($\bot_{\mathsf{DP}}$), or if it
is completely infeasible ($\top_{\mathsf{DP}}$).

A DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}$
is equivalent to a degenerate UDP
$\langle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}\rangle$.

A UDP $\boldsymbol{u}$ is a bound for a DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}$
if
$\boldsymbol{u}\preceq_{\mathsf{UDP}}\langle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}\rangle$,
or, equivalently, if
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\boldsymbol{u}\preceq_{\mathsf{UDP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}\preceq_{\mathsf{UDP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\boldsymbol{u}$.

##  V Interconnection of Uncertain Design Problems

We now define the interconnection of UDPs, in an equivalent way to the
definition of MCDPs. The only difference between Def. 6 and Def. 16 below is
that the valuation assigns to each atom an UDP, rather than a DP.

######  Definition 16 (Algebraic definition of UMCDPs).

An Uncertain MCDP (UMCDP) is a tuple
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle$,
where $\mathcal{A}$ is a set of atoms,
$\boldsymbol{\mathsf{T}}\in\mathsf{Terms}(\\{\mathsf{series},\mathsf{par},\mathsf{loop}\\},\mathcal{A})$
is the algebraic representation of the graph, and
$\boldsymbol{v}:\mathcal{A}\rightarrow\mathsf{UDP}$ is a valuation that
assigns to each atom a UDP.

Next, the semantics of a UMCDP is defined as a map $\Phi$ that computes the
UDP. Def. 17 below is analogous to Def. 8.

######  Definition 17 (Semantics of UMCDPs).

Given an UMCDP
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle$,
the semantics function $\Phi$ computes a UDP

$\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle\rrbracket\in\mathsf{UDP},$

and it is recursively defined as follows:

$\Phi\llbracket\left\langle\mathcal{A},a,\boldsymbol{v}\right\rangle\rrbracket=\boldsymbol{v}(a),\qquad\text{for
all}\ a\in\mathcal{A}.$
$\displaystyle{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle=({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{1},\boldsymbol{v}\right\rangle\rrbracket)\,\mathbin{\varocircle}\,({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{2},\boldsymbol{v}\right\rangle\rrbracket),$
$\displaystyle{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle=({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{1},\boldsymbol{v}\right\rangle\rrbracket)\,\mathbin{\varocircle}\,({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{2},\boldsymbol{v}\right\rangle\rrbracket),$
$\displaystyle{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{par}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle]$
$\displaystyle=({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{1},\boldsymbol{v}\right\rangle\rrbracket)\
\mathbin{\varotimes}\
({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{2},\boldsymbol{v}\right\rangle\rrbracket),$
$\displaystyle{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{par}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle]$
$\displaystyle=({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{1},\boldsymbol{v}\right\rangle\rrbracket)\
\mathbin{\varotimes}\
({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}}_{2},\boldsymbol{v}\right\rangle\rrbracket),$
$\displaystyle{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{loop}(\boldsymbol{\mathsf{T}}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle=({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle\rrbracket)^{\dagger},$
$\displaystyle{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{loop}(\boldsymbol{\mathsf{T}}),\boldsymbol{v}\right\rangle\rrbracket$
$\displaystyle=({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle\rrbracket)^{\dagger}.$

The operators $\dagger,\mathbin{\varocircle},\mathbin{\varotimes}$ are defined
in Def. 10–Def. 11.

##  VI Approximation results

The main result of this section is a relaxation result stated as Theorem 19
below. The following is an informal statement.

(a) Consider an MCDP containing the DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$.

(b) Suppose that a bound
$\left\langle\boldsymbol{\mathsf{L}},\boldsymbol{\mathsf{U}}\right\rangle$ is
known.

(c) Replace the DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$
by the uncertain bounds.

(d) Create a pair of MCDPs by choosing either lower or upper bound.

(e) The resulting MCDPs are bounds for the original MCDP.

Figure 8: Illustrations for the informal statement of the main result.

#### Informal statement

Consider an MCDP composed of many DPs, and call one
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$
(Fig. 8a). Suppose there exist two DPs $\boldsymbol{\mathsf{L}}$,
$\boldsymbol{\mathsf{U}}$ that bound the DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$
in the sense that
$\boldsymbol{\mathsf{L}}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}\preceq_{\mathsf{DP}}\boldsymbol{\mathsf{U}}$
(Fig. 8b). This can model either uncertainty in our knowledge of
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$,
or it can be a relaxation that we willingly introduce. The pair
$\left\langle\boldsymbol{\mathsf{L}},\boldsymbol{\mathsf{U}}\right\rangle$
forms a UDP that can be plugged in the MCDP in place of
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$
(Fig. 8c). We will see that if we plug in only $\boldsymbol{\mathsf{L}}$ or
$\boldsymbol{\mathsf{U}}$ separately in place of the original DP
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}$
(Fig. 8d), we obtain a pair of MCDPs that form a UDP. Moreover, the solution
of these two MCDPs are upper and lower bounds for the solution of the original
MCDP (Fig. 8e). Therefore, we can propagate the uncertainty in the model to
the uncertain in the solution. This result generalizes for any number of
substitutions.

#### Formal statement

First, we define a partial order on the valuations. A valuation precedes
another if it gives more information on each DP.

######  Definition 18 (Partial order $\preceq_{V}$ on valuations).

For two valuations
$\boldsymbol{v}_{1},\boldsymbol{v}_{2}:\mathcal{A}\rightarrow\mathsf{UDP}$,
say that $\boldsymbol{v}_{1}\preceq_{V}\boldsymbol{v}_{2}$ if
$\boldsymbol{v}_{1}(a)\preceq_{\mathsf{UDP}}\boldsymbol{v}_{2}(a)$ for all
$a\in\mathcal{A}$.

At this point, we have enough machinery in place that we can simply state the
result as “the semantics is monotone in the valuation”.

######  Theorem 19 ($\Phi$ is monotone in the valuation).

If $\boldsymbol{v}_{1}\preceq_{V}\boldsymbol{v}_{2}$, then

$\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\right\rangle\rrbracket\preceq_{\mathsf{UDP}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\right\rangle\rrbracket.$

###### Proof:

This follows easily from the definitions in Def. 18. As intermediate results,
first prove that the lower bound
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi$
is monotone in the valuation with respect to the order
$\preceq_{\mathsf{DP}}$:

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket.$

Then repeat the same reasoning for
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}$,
to obtain:

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket.$

These two together allow to conclude that $\Phi$ is monotone with respect to
the valuation with respect to the order $\preceq_{\mathsf{UDP}}$:

$\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket\preceq_{\mathsf{UDP}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket.$

∎

This result says that we can swap any DP in a MCDP with a UDP relaxation to
obtain a UMCDP, which then we can solve to obtain inner and outer
approximations to the solution of the original MCDP. This shows that
considering interval uncertainty in the MCDP framework is easy because it
reduces to solving a pair of problems instead of one. The rest of the paper
consists of applications of this result.

##  VII Applications

This section shows three example applications of the theory:

  1. 1.

The first example deals with _parametric uncertainty_.

  2. 2.

The second example deals with the idea of relaxation of a scalar relation.
This is equivalent to accepting a _tolerance_ for a given variable, in
exchange for reduced computation.

  3. 3.

The third example deals with the _relaxation of relations with infinite
cardinality_. In particular it shows how one can obtain consistent estimates
with a finite and prescribed amount of computation.

###  VII-A Parametric Uncertainty

To instantiate the model in Fig. 1a, we need to obtain numbers for energy
density, specific cost, and operating life for all batteries technologies we
want to examine. By browsing Wikipedia, one can find the figures in Table I.

Table I: Specifications of common batteries technologies _technology_ | _energy density_ | _specific cost_ | _operating life_
---|---|---|---
[Wh/kg] | [Wh/$] | # cycles
NiMH | 100 |  3. | 41 | 500
NiH2 | 45 |  10. | 50 | 20000
LCO | 195 |  2. | 84 | 750
LMO | 150 |  2. | 84 | 500
NiCad | 30 |  7. | 50 | 500
SLA | 30 |  7. | 00 | 500
LiPo | 150 |  2. | 50 | 600
LFP | 90 |  1. | 50 | 1500

Should we trust those figures? Fortunately, we can easily deal with possible
mistrust by introducing uncertain DPs. Formally, we replace the DPs for
_energy density_ , _specific cost_ , _operating life_ in Fig. 1a with the
corresponding Uncertain DPs with a configurable uncertainty. We can then solve
the UDPs to obtain a lower bound and an upper bound to the solutions that can
be presented to the user.

Fig. 9 shows the relation between the provided endurance and the minimal total
mass required, when using uncertainty of $5\%$, $10\%$, $25\%$ on the numbers
above. Each panel shows two curves: the lower bound (best case analysis) and
the upper bound (worst case analysis). In some cases, the lower bound is
feasible, but the upper bound is not. For example, in panel  _b_ , for 10%
uncertainty, we can conclude that, notwithstanding the uncertainty, there
exists a solution for endurance $\leq 1.35\,\text{hours}$, while for values in
$[1.35,1.5]$, represented by the shaded area, we cannot conclude either the
existence or nonexistence of a solution, because the lower bound is feasible,
but the upper bound is not. This area of uncertainty depends on the parameter
uncertainty injected (smaller for 5%, and larger for 25%).

Figure 9: Uncertain relation between endurance and the minimal total mass
required, obtained by solving the example in Fig. 1a for different values of
the uncertainty on the characteristics of the batteries (5%, 10%, 25%). The
shaded area represents the subset of the functionality space for which we
cannot conclude that a solution exists, because the upper bound DP is not
feasible, while the lower bound DP is feasible.

###  VII-B Introducing Tolerances

Another application of the theory is the introduction of tolerances for any
variable in the optimization problem. For example, one might not care about
the variations of the battery mass below, say, $1\,\text{g}$. One can then
introduce a $\pm 1\,\text{$\text{g}$ }$ uncertainty in the definition of the
problem by adding a UDP hereby called “uncertain identity”.

####  VII-B1 The uncertain identity

Let $\alpha>0$ be a step size. Define
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathsf{floor}}_{\alpha}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{ceil}}_{\alpha}$
to be the floor and ceil with step size $\alpha$ (Fig. 10). By construction,
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathsf{floor}}_{\alpha}\preceq_{\mathsf{DP}}\mathsf{Id}\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{ceil}}_{\alpha}.$

(a)  (b)  (c)

Figure 10: The identity and its two relaxations
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathsf{floor}}_{\alpha}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{ceil}}_{\alpha}$.

Let
$\mathsf{UId}_{\alpha}\doteq\left\langle{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\mathsf{floor}}_{\alpha},{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\mathsf{ceil}}_{\alpha}\right\rangle$
be the “uncertain identity”. For $0<\alpha<\beta$, it holds that

$\mathsf{Id}\prec_{\mathsf{UDP}}\mathsf{UId}_{\alpha}\prec_{\mathsf{UDP}}\mathsf{UId}_{\beta}.$

Therefore, the sequence $\mathsf{UId}_{\alpha}$ is a descending chain that
converges to $\mathsf{Id}$ as $\alpha\rightarrow 0$ (Fig. 11).

Figure 11: Convergence of $\mathsf{UId}_{\alpha}$ to the identity
$\mathsf{Id}$.

####  VII-B2 Approximations in MCDP

We can take any edge in an MCDP and apply this relaxation. Formally, we first
introduce an identity $\mathsf{Id}$ and then relax it using
$\mathsf{UId}_{\alpha}$ (Fig. 12).

Figure 12: Introduction of tolerances by using the “uncertain identity”
$\text{UId}_{\alpha}$.

Mathematically, given an MCDP
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle$,
we generate a UMCDP
$\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{\alpha}\right\rangle$,
where the new valuation $\boldsymbol{v}_{\alpha}$ agrees with $\boldsymbol{v}$
except on a particular atom $a\in\mathcal{A}$, which is replaced by the series
of the original $\boldsymbol{v}(a)$ and the approximation
$\text{UId}_{\alpha}$:

$\displaystyle\boldsymbol{v}_{\alpha}(a)$
$\displaystyle\doteq\mathsf{series}(\mathsf{UId}_{\alpha},\boldsymbol{v}(a))$

Call the original and approximated DPs $\mathsf{dp}$ and
$\mathsf{dp}_{\alpha}$:

$\begin{array}[]{ccc}\mathsf{dp}\doteq\Phi\left\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\right\rangle\right\rrbracket,&&\mathsf{dp}{}_{\alpha}\doteq\Phi\left\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{\alpha}\right\rangle\right\rrbracket.\end{array}$

Because $\boldsymbol{v}\preceq_{V}\boldsymbol{v}_{\alpha}$ (in the sense of
Def. 18), Theorem 19 implies that

$\mathsf{dp}\preceq_{\mathsf{UDP}}\mathsf{dp}_{\alpha}.$

This means that we can solve
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\mathsf{dp}_{\alpha}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\mathsf{dp}_{\alpha}$
and obtain upper and lower bounds for $\mathsf{dp}$. Furthermore, by varying
$\alpha$, we can construct an approximating sequence of DPs whose solution
will converge to the solution of the original MCDP.

##### Numerical results

This procedure was applied to the example model in Fig. 1a by introducing a
tolerance to the “power” variable for the actuation. The tolerance $\alpha$ is
chosen at logarithmic intervals between $0.01\,\text{mW}$ and $1\,\text{W}$.
Fig. 13a shows the solutions of the minimal mass required for
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\mathsf{dp}_{\alpha}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\mathsf{dp}_{\alpha}$,
as a function of $\alpha$. Fig. 13a confirms the consistency results predicted
by the theory. First, if the solutions for both
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\mathsf{dp}_{\alpha}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\mathsf{dp}_{\alpha}$
exist, then they are ordered
(${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\mathsf{dp}_{\alpha}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})\preceq{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\mathsf{dp}_{\alpha}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})$).
Second, as $\alpha$ decreases, the interval shrinks. Third, the bounds are
consistent, in the sense that the solution for the original DP is always
contained in the bounds.

(a)  (b)

Figure 13: Results of model in Fig. 1a when tolerance is applied to the
actuation power resource. Panel  _a_ shows the uncertainty in the solution as
a function of tolerance. Panel  _b_ shows the iterations needed.

Next, it is interesting to consider the computational complexity. Fig. 13b
shows the number of iterations as a function of the resolution $\alpha$, and
the trade-off of the uncertainty of the solution and the computational
resources spent. This shows that this approximation scheme is an effective way
to reduce the computation load while maintaining a consistent estimate.

###  VII-C Relaxation for relations with antichains of infinite cardinality

Another way in which uncertain DPs can be used is to construct approximations
of DPs that would be too expensive to solve exactly. For example, consider a
relation like

${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\text{travel\\_distance}}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{velocity}}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{endurance}},$
(8)

which appears in the model in Fig. 1a. If we take these three quantities in
(8) as belonging to $\mathbb{R}$, then, for each value of the travel distance,
there are infinite pairs of
$\left\langle{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{velocity}},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{endurance}}\right\rangle$
that are feasible. On a computer, if the quantities are represented as
floating point numbers, the combinations are properly not “infinite”, but,
still, extremely large. We can avoid considering all combinations by creating
a sequence of uncertain DPs that use finite and prescribed computation.

####  VII-C1 Relaxations for addition

Consider a monotone relation between some functionality
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\in\mathbb{R}_{+}$
and resources
${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}\in\mathbb{R}_{+}$
described by the constraint that
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}+{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}$
(Fig. 14). For example, this could represent the case where there are two
batteries providing the power
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}$,
and we need to decide how much to allocate to the first
(${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}$)
or the second
(${\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}$).

Figure 14: Graphical relation of the DP for the relation
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}+{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}$.
The overline in “$\overline{+}$” represents the fact that this is the “dual”
of the relation
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}+{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}$,
for which we used the name “$+$”.

The formal definition of this constraint as an DP is

$\displaystyle\overline{+}:{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathbb{R}_{+}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}(\mathbb{R}_{+}\times\mathbb{R}_{+})},$
$\displaystyle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}$
$\displaystyle\mapsto\\{\left\langle
x,{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}-x\right\rangle\mid
x\in\mathbb{R}_{+}\\}.$

Note that, for each value
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}$,
$\overline{+}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})$
is a set of infinite cardinality. We will now define two sequences of
relaxations for $\overline{+}$ with a fixed number of solutions $n\geq 1$.

#### Using uniform sampling

We will first define a sequence of UDPs $S_{n}$ based on uniform sampling. Let
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}S_{n}$
consist of $n$ points sampled on the segment with extrema $\left\langle
0,{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\right\rangle$
and
$\left\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},0\right\rangle$.
For
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}S_{n}$,
sample $n+1$ points on the segment and take the _meet_ of successive points
(Fig. 15).

Figure 15: Construction of approximating antichains.

The first elements of the sequences are shown in Fig. 16. One can easily prove
that
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}S_{n}\preceq_{\mathsf{DP}}\overline{+}\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}S_{n}$,
and thus $S_{n}$ is a relaxation of $\overline{+}$, in the sense that
$\overline{+}\preceq_{\mathsf{UDP}}S_{n}$. Moreover, $S_{n}$ converges to
$\overline{+}$ as $n\rightarrow\infty$.

Figure 16: Approximations to $\overline{+}$ using the uniform sampling
sequence $S_{n}$.

However, the convergence is not monotonic, in the sense that
$S_{n+1}{\not\preceq}_{\mathsf{UDP}}S_{n}.$ The situation can be represented
graphically as in Fig. 19a. The sequence $S_{n}$ eventually converges to
$\overline{+}$, but it is not a descending chain. This means that it is not
true, in general, that the solution to the MCDP obtained by plugging in
$S_{n+1}$ gives smaller bounds than $S_{n}$.

#### Relaxation based on Van Der Corput sequence

We can easily create an approximation sequence
$V:\mathbb{N}\rightarrow\mathsf{UDP}$ that converges monotonically using Var
Der Corput (VDC) sampling [17, Section 5.2]. Let $\mathsf{vdc}(n)$ be the VDC
sequence of $n$ elements in the interval $[0,1]$. The first elements of the
VDC are $\\{0,0.5,0.25,0.75,0.125,\dots\\}$. The sequence is guaranteed to
satisfy $\mathsf{vdc}(n)\subseteq\mathsf{vdc}(n+1)$ and to minimize the
“discrepancy”, a measure of uniform coverage.

The upper bound
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}V_{n}$
is defined as sampling the segment with extrema $\left\langle
0,{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\right\rangle$
and
$\left\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},0\right\rangle$
using the VDC sequence:

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}V_{n}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\mapsto\\{\left\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}x,{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}(1-x)\right\rangle\mid
x\in\mathsf{vdc}(n)\\}.$

The lower bound
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}V_{n}$
is defined by taking meets of successive points, according to the procedure in
Fig. 15.

Figure 17: Approximations to $\overline{+}$ using the Van Der Corput sequence
$V_{n}$. The orange and purple areas are the upper closures of the antichains
represented by the black points.

For this sequence, one can prove that not only
$\overline{+}\preceq_{\mathsf{UDP}}V_{n}$, but also that the convergence is
uniform, in the sense that
$\overline{+}\preceq_{\mathsf{UDP}}V_{n+1}\preceq_{\mathsf{UDP}}V_{n}.$ The
situation is represented graphically in Fig. 19b: the sequence is a descending
chain that converges to $\overline{+}$.

####  VII-C2 Dual of multiplication

The case of multiplication can be treated analogously to the case of addition.
By taking the logarithm, the inequality
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}$
can be rewritten as
$\log({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})\leq\log({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1})+\log({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}).$
So we can repeat the constructions done for addition. The VDC sequence are
shown in Fig. 18.

Figure 18: Van Der Corput relaxations of
${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{1}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}_{2}$
for $n=3,5,10,15.$ The orange and purple areas are the upper closures of the
antichains represented by the black points.

####  VII-C3 Numerical example

This relaxation strategy was applied to the relation
_${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\text{travel
distance}}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{velocity}}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{endurance}}$_
in the MCDP in Fig. 1a. Thanks to the theory, we can obtain estimates of the
solutions using bounded computation, even though that relation has infinite
cardinality.

Fig. 19c shows the result using uniform sampling, and Fig. 19d shows the
result using VDC sampling. As predicted by the theory, uniform sampling does
not give monotone convergence, while VDC sampling does.

(a) Qualitative behavior for $S_{n}$ (b) Qualitative behavior for $V_{n}$

(c) Numerical results for $S_{n}$

(d) Numerical results for $V_{n}$

Figure 19: Solutions to the example in Fig. 1a, applying relaxations for the
relation
_${\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\text{travel\\_distance}}\leq{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{velocity}}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\text{endurance}}$_
using the uniform sampling sequence and the VDC sampling sequence. The uniform
sampling sequence $S_{n}$ does not converge monotonically (panel  _a_);
therefore the progress is not monotonic (panel _c_). Conversely, the Van Der
Corput sequence $V_{n}$ is a descending chain (panel  _b_), which results in
monotonic progress (panel  _d_).

##  VIII Conclusions and future work

Monotone Co-Design Problems (MCDPs) provide a compositional theory of “co-
design” that describes co-design constraints among different subsystems in a
complex system, such as a robotic system.

This paper dealt with the introduction of uncertainty in the framework,
specifically, interval uncertainty. Uncertainty can be used in two roles.
First, it can be used to describe limited knowledge in the models. For
example, in Section VII-A, we have seen how this can be applied to model
mistrust about numbers from Wikipedia. Second, uncertainty allows to generate
relaxations of the problem. We have seen two applications: introducing an
allowed tolerance in one particular variable (Section VII-B), and dealing with
relations with infinite cardinality using bounded computation resources
(Section VII-C).

Future work includes strengthening these results. For example, we are not able
to predict the resulting uncertainty in the solution before actually computing
it; ideally, one would like to know how much computation is needed (measured
by the number of points in the antichain approximation) for a given value of
the uncertainty that the user can accept.

## References

  * [1] Andrea Censi “Monotone Co-Design Problems; or, everything is the same” In _Proceedings of the American Control Conference (ACC)_ , 2016
  * [2] Andrea Censi “A Mathematical Theory of Co-Design” In _CoRR_ abs/1512.08055, 2015 URL: http://arxiv.org/abs/1512.08055
  * [3] A. M. Mehta, J. DelPreto, B. Shaya and D. Rus “Cogeneration of mechanical, electrical, and software designs for printable robots from structural specifications” In _Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)_ , 2014, pp. 2892–2897 DOI: 10.1109/IROS.2014.6942960
  * [4] Ankur M. Mehta et al. “Robot Creation from Functional Specifications” In _The International Symposium on Robotics Research (ISRR)_ , 2015
  * [5] Dimitris Bertsimas, David B. Brown and Constantine Caramanis “Theory and Applications of Robust Optimization.” In _SIAM Review_ 53.3, 2011, pp. 464–501 DOI: 10.1137/080734510
  * [6] Aharon Ben-Tal, Laurent El Ghaoui and Arkadi Nemirovski “Robust Optimization” Walter de Gruyter GmbH, 2009 DOI: 10.1515/9781400831050
  * [7] Andrea Censi “Handling Uncertainty in Monotone Co-Design Problems” Extended version on Arxiv with supplementary materials URL: http://tiny.cc/mcdp_uncertainty_extended
  * [8] B.A. Davey and H.A. Priestley “Introduction to Lattices and Order” Cambridge University Press, 2002 DOI: 10.1017/cbo9780511809088
  * [9] G. Gierz et al. “Continuous Lattices and Domains” Cambridge University Press, 2003 DOI: 10.1017/cbo9780511542725
  * [10] Gerhard Pahl, W. Beitz, Jörg Feldhusen and Karl-Heinrich Grote “Engineering Design: A Systematic Approach” Springer, Hardcover, 2007
  * [11] N.P. Suh “Axiomatic Design: Advances and Applications” Oxford University Press, 2001
  * [12] R.J Duffin “Topology of series-parallel networks” In _Journal of Mathematical Analysis and Applications_ 10.2 Elsevier BV, 1965, pp. 303–318 DOI: 10.1016/0022-247x(65)90125-3
  * [13] Gheorghe Ştefănescu “Network Algebra” Springer Science + Business Media, 2000 DOI: 10.1007/978-1-4471-0479-7
  * [14] André Joyal, Ross Street and Dominic Verity “Traced monoidal categories” In _Math. Proc. Camb. Phil. Soc._ 119.03 Cambridge University Press (CUP), 1996, pp. 447 DOI: 10.1017/s0305004100074338
  * [15] David I. Spivak “Category Theory for the Sciences” MIT, 2014
  * [16] Jarda Jezek “Universal Algebra”, 2008
  * [17] Steven M. LaValle “Planning Algorithms” Cambridge University Press, Hardcover, 2006 URL: http://planning.cs.uiuc.edu/

##  Appendix A Appendix

###  A-A Proofs

####  A-A1 Proofs of well-formedness of 17

As some preliminary business, we need to prove that 17 is well formed, in the
sense that the way the semantics function $\Phi$ is defined, it returns a UDP
for each argument. This is not obvious from 17.

For example, for
$\Phi\llbracket\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rrbracket$,
the definition gives values for
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rrbracket$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rrbracket$
separately, without checking that

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rrbracket.$

The following lemma provides the proof for that.

######  Lemma 20.

17 is well formed, in the sense that

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\langle\mathcal{A},\mathsf{series}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\rangle\rrbracket,$
(9)
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{par}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{par}(\boldsymbol{\mathsf{T}}_{1},\boldsymbol{\mathsf{T}}_{2}),\boldsymbol{v}\right\rangle\rrbracket,$
(10)
${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{loop}(\boldsymbol{\mathsf{T}}),\boldsymbol{v}\right\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\left\langle\mathcal{A},\mathsf{loop}(\boldsymbol{\mathsf{T}}),\boldsymbol{v}\right\rangle\rrbracket.$
(11)

###### Proof:

Proving (LABEL:wf1)—(LABEL:wf3) can be reduced to proving the following three
results, for any $x,y\in\mathsf{UDP}$:

$\displaystyle\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varocircle}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}y\right)$
$\displaystyle\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\mathbin{\varocircle}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right),$
$\displaystyle\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varotimes}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}y\right)$
$\displaystyle\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\mathbin{\varotimes}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right),$
$\displaystyle\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\right)^{\dagger}$
$\displaystyle\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\right)^{\dagger}.$

These are given in 21, 22, 23. ∎

######  Lemma 21.

$\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varocircle}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}y\right)\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\mathbin{\varocircle}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right)$.

###### Proof:

First prove that $\mathbin{\varocircle}$ is monotone in each argument (proved
as 24). Then note that

$\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varocircle}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}y\right)\preceq_{\mathsf{DP}}\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varocircle}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right)\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\mathbin{\varocircle}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right).$

∎

######  Lemma 22.

$\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varotimes}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}y\right)\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\mathbin{\varotimes}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right)$.

###### Proof:

The proof is entirely equivalent to the proof of 21. First prove that
$\mathsf{par}$ is monotone in each argument (proved as 25). Then note that

$\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varotimes}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}y\right)\preceq_{\mathsf{DP}}\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\mathbin{\varotimes}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right)\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\mathbin{\varotimes}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}y\right).$

∎

######  Lemma 23.

$\left({\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}x\right)^{\dagger}\preceq_{\mathsf{DP}}\left({\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}x\right)^{\dagger}$.

###### Proof:

This follows from the fact that $\dagger$ is monotone (27). ∎

####  A-A2 Monotonicity lemmas for DP

These lemmas are used in the proofs above.

######  Lemma 24.

$\mathbin{\varocircle}:\mathsf{DP}\times\mathsf{DP}\rightarrow\mathsf{DP}$ is
monotone on $\langle\mathsf{DP},\preceq_{\mathsf{DP}}\rangle$.

###### Proof:

In 10, $\mathbin{\varocircle}$ is defined as follows for two maps
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{1}$
and
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}\colon{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2}\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}_{2}$:

${\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\mathbin{\varocircle}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}=\operatorname*{Min}_{\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}}}\uparrow\bigcup_{s\in{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}})}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}(s)}.$

It is useful to decompose this expression as the composition of three maps:

${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\mathbin{\varocircle}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}=m\circ
g[{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}]\circ{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1},$

where “$\circ$” is the usual map composition, and $g$ and $m$ are defined as
follows:

$\displaystyle
g[{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}]:\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}$
$\displaystyle\rightarrow\mathsf{U}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2},$
$\displaystyle R$ $\displaystyle\mapsto\uparrow\bigcup_{s\in
R}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}(s),$

and

$\displaystyle
m:\mathsf{U}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}$
$\displaystyle\rightarrow\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2},$
$\displaystyle R$
$\displaystyle\mapsto\operatorname*{Min}_{\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}}}R.$

From the following facts:

  * •

$m$ is monotone.

  * •

$g[{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}]$
is monotone in
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}$.

  * •

$f_{1}\circ f_{2}$ is monotone in each argument if the other argument is
monotone.

Then the thesis follows. ∎

######  Lemma 25.

$\mathbin{\varotimes}:\mathsf{DP}\times\mathsf{DP}\rightarrow\mathsf{DP}$ is
monotone on $\langle\mathsf{DP},\preceq_{\mathsf{DP}}\rangle$.

###### Proof:

The definition of $\mathbin{\varotimes}$ (9) is:

$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\mathbin{\varotimes}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}:({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{1}\times{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathscr{F}}_{2})$
$\displaystyle\rightarrow\mathsf{A}({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}),$
$\displaystyle\left\langle{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}\right\rangle$
$\displaystyle\mapsto{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})\times{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2}).$

Because of symmetry, it suffices to prove that $\mathbin{\varotimes}$ is
monotone in the first argument, leaving the second fixed.

We need to prove that for any two DPs
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a},{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}$
such that

${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b},$
(12)

and for any fixed
$\overline{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}$,
then

${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}\mathbin{\varotimes}\overline{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}\mathbin{\varotimes}\overline{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}.$

Let
$R=\overline{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2})$.
Then we have that

$\displaystyle[{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}\mathbin{\varotimes}\overline{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}]({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2})$
$\displaystyle={\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})\mathbin{\boldsymbol{\times}}R,$
$\displaystyle{}[{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}\mathbin{\varotimes}\overline{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}]({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2})$
$\displaystyle={\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})\mathbin{\boldsymbol{\times}}R.$

Because of (LABEL:Ikno), we know that

${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{a}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})\preceq_{\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{b}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}).$

So the thesis follows from proving that the product of antichains is monotone
(26). ∎

######  Lemma 26.

The product of antichains
$\mathbin{\boldsymbol{\times}}:\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}\times\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2}\rightarrow\mathsf{A}({\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{1}\times{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}_{2})$
is monotone.

######  Lemma 27.

$\dagger:\mathsf{DP}\rightarrow\mathsf{DP}$ is monotone on
$\langle\mathsf{DP},\preceq_{\mathsf{DP}}\rangle$.

###### Proof:

Let
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}$.
Then we can prove that
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}^{\dagger}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}^{\dagger}$.
From the definition of $\dagger$ (11), we have that

$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}^{\dagger}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1})$
$\displaystyle=\mathsf{lfp}(\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}}),$
$\displaystyle{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}^{\dagger}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{2})$
$\displaystyle=\mathsf{lfp}(\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}}),$

with
$\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}$
defined as

$\displaystyle\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}:{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}$
$\displaystyle\rightarrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}},$
$\displaystyle{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}$
$\displaystyle\mapsto\operatorname*{Min}_{\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}}\bigcup_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\in{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}})\
\cap\uparrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}.$

The least fixed point operator $\mathsf{lfp}$ is monotone, so we are left to
check that the map

${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}\mapsto\Psi_{{\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1}}^{{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}}$

is monotone. That is the case, because if
${\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}\preceq_{\mathsf{DP}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}$
then

$\left[\bigcup_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\in{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{1}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}})\
\cap\uparrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\right]\preceq_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{A}{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathscr{R}}}}\left[\bigcup_{{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\in{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}R}}{\color[rgb]{0.000000,0.400000,1.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.000000,0.400000,1.000000}{h}}_{2}({\color[rgb]{0.094869,0.500000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.094869,0.500000,0.000000}\mathsf{f}}_{1},{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}})\
\cap\uparrow{\color[rgb]{0.555789,0.000000,0.000000}\definecolor[named]{pgfstrokecolor}{rgb}{0.555789,0.000000,0.000000}\mathsf{r}}\right].$

∎

####  A-A3 Monotonicity of semantics $\varphi$

######  Lemma 28 ($\varphi$ is monotone in the valuation).

Suppose that
$\boldsymbol{v}_{1},\boldsymbol{v}_{2}:\mathcal{A}\rightarrow\mathsf{DP}$ are
two valuations for which it holds that
$\boldsymbol{v}_{1}(a)\preceq_{\mathsf{DP}}\boldsymbol{v}_{2}(a)$. Then
$\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\right\rangle\rrbracket\preceq_{\mathsf{DP}}\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\right\rangle\rrbracket$.

###### Proof:

Given the recursive definition of 8, we need to prove this just for the base
case and for the recursive cases.

The base case, given in (2), is

$\varphi\llbracket\left\langle\mathcal{A},a,\boldsymbol{v}\right\rangle\rrbracket\doteq\boldsymbol{v}(a),\qquad\text{for
all}\ a\in\mathcal{A}.$

We have

$\displaystyle\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\right\rangle\rrbracket$
$\displaystyle=\boldsymbol{v}_{1}(a)$
$\displaystyle\varphi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\right\rangle\rrbracket$
$\displaystyle=\boldsymbol{v}_{2}(a)$

and $\boldsymbol{v}_{1}(a)\preceq_{\mathsf{DP}}\boldsymbol{v}_{2}(a)$ by
assumption.

For the recursive cases, (3)–(5), the thesis follows from the monotonicity of
$\mathbin{\varocircle}$, $\mathbin{\varotimes}$, $\dagger$, proved in 25, 24,
27. ∎

####  A-A4 Proof of the main result, 19

We restate the theorem.

Theorem 19. _If_

$\boldsymbol{v}_{1}\preceq_{V}\boldsymbol{v}_{2}$

_then_

$\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\right\rangle\rrbracket\preceq_{\mathsf{UDP}}\Phi\llbracket\left\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\right\rangle\rrbracket.$

###### Proof:

From the definition of $\Phi$ and $\varphi$, we can derive that

$\displaystyle{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}\rangle\rrbracket$
$\displaystyle=\varphi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\circ\boldsymbol{v}\rangle\rrbracket.$
(13)

In particular, for $\boldsymbol{v}=\boldsymbol{v}_{1}$,

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket=\varphi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\circ\boldsymbol{v}_{1}\rangle\rrbracket.$
(14)

Because $\boldsymbol{v}_{1}(a)\preceq_{\mathsf{UDP}}\boldsymbol{v}_{2}(a),$
from 28,

$\varphi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\circ\boldsymbol{v}_{1}\rangle\rrbracket\preceq_{\mathsf{DP}}\varphi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\circ\boldsymbol{v}_{2}\rangle\rrbracket.$
(15)

From (LABEL:equiv1) again,

$\varphi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\circ\boldsymbol{v}_{2}\rangle\rrbracket={\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket.$
(16)

From (14), (15), (16) together,

${\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\boldsymbol{\mathsf{L}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket.$

Repeating the same reasoning for
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}$,
we have

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket\preceq_{\mathsf{DP}}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\boldsymbol{\mathsf{U}}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket.$

Therefore

$\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{1}\rangle\rrbracket\preceq_{\mathsf{UDP}}\Phi\llbracket\langle\mathcal{A},\boldsymbol{\mathsf{T}},\boldsymbol{v}_{2}\rangle\rrbracket.$

∎

##  Appendix B Software

###  B-A Source code

The implementation is available at the repository
http://github.com/AndreaCensi/mcdp/, in the branch “uncertainty_sep16”.

###  B-B Virtual machine

A VMWare virtual machine is available to reproduce the experiments at the URL
https://www.dropbox.com/sh/nfpnfgjh9hpcgvh/AACVZfdVXxMoVqTYiHWaOwHAa?dl=0.

To reproduce the figures, log in with user password “mcdp”/”mcdp”. Then
execute the following commands:

[] $ cd ~/mcdp

$ source environment.sh

$ cd libraries/examples/uav_energetics/

droneD_complete_templates.mcdplib

$ make clean

$ make paper-figures

See pages - of mcdp_icra_uncertainty_models.pdf