Arithmetic circuits with $\min$, $\max$, and average over $[0,1]$ Consider a circuit that takes as inputs numbers in $[0,1]$, and has gates that consist of the functions $\max(x, y)$, $\min(x, y)$, $1 - x$, and $\frac{x+y}{2}$.
The output of the circuit is then also a number in $[0,1]$.

Does anyone know if this model, or a closely related model, has been studied? 

Specifically, I'm trying to solve the satisfiability problem for this circuit, namely computing the maximum value that can be attained by this circuit (it indeed attains a maximum, as it represents a continuous function in a compact domain).

Remark: my study of this model is via weighted temporal logics, so any models that relate to the latter might also come in handy.
The satisfiability problem for these circuits  (i.e., given a circuit $C$ and $u\in[0,1]$, decide whether there is an input $x$ such that $C(x)\ge u$) is in NP, and therefore NP-complete by Neal Young’s comment and Peter Shor’s answer.

We can construct a nondeterministic reduction of the problem to linear programming in the following way. Let $\{a_i:i&lt;m\}$ be all nodes of $C$ that are min or max gates (here $m\le n$, where $n$ is the size of the circuit), and let $b_i$ and $c_i$ be the input nodes of gate $a_i$. For every $i&lt;m$, choose one of the two additional constraints $b_i\le c_i$ or $c_i\le b_i$ (there are $2^m$ possible choices in total). When such a choice is fixed, we can simplify the circuit by replacing each $a_i$ with $b_i$ or $c_i$ as appropriate, and the resulting circuit can be described by a system of $n$ linear equations whose variables are the original input variables of the circuit, and additional variables corresponding to nodes of the circuit.

We also include $m$ inequalities stating that the extra constraints are satisfied, inequalities bounding the original input variables to $[0,1]$, and an inequality stating that the output node has value $\ge u$. Then this is a linear program of size $O(n)$ depending on the choice of the extra constraints, and the circuit attains value $\ge u$ iff there exists a choice of the constraints such that the associated linear program has a solution. Since linear programming is in P, this shows that the problem is in NP.

Also note that the optimum value of a linear program is attained at a vertex of the polytope. This means that the denominator of the optimal solution can be expressed as a determinant of a square matrix of dimension $O(n)$ whose entries are constant-size integers, and there are only $O(1)$ nonzero entries in each row, and as such it is bounded by $2^{O(n)}$.

Reductions of this kind are often useful to give upper bounds on the complexity of satisfiability in propositional fuzzy logics (such as Łukasiewicz logic) and related systems. (In fact, the original problem is a minor variant of satisfiability in Łukasiewicz, which would correspond to circuits with $\min(1,x+y)$ instead of $(x+y)/2$.) An overview of related results can be found in Chapter X of the Handbook of Mathematical Fuzzy Logic, Vol. II.