  Programmability and verifiability lie at the heart of the software-defined
networking paradigm. While OpenFlow and its match-action concept provide
primitive operations to manipulate hardware configurations, over the last
years, several more expressive network programming languages have been
developed. This paper presents WNetKAT, the first network programming language
accounting for the fact that networks are inherently weighted, and
communications subject to capacity constraints (e.g., in terms of bandwidth)
and costs (e.g., latency or monetary costs). WNetKAT is based on a syntactic
and semantic extension of the NetKAT algebra. We demonstrate several relevant
applications for WNetKAT, including cost- and capacity-aware reachability, as
well as quality-of-service and fairness aspects. These applications do not only
apply to classic, splittable and unsplittable (s; t)-flows, but also generalize
to more complex network functions and service chains. For example, WNetKAT
allows to model flows which need to traverse certain waypoint functions, which
may change the traffic rate. This paper also shows the relation between the
equivalence problem of WNetKAT and the equivalence problem of the weighted
finite automata, which implies undecidability of the former. However, this
paper also succeeds to prove the decidability of another useful problem, which
is sufficient in many practical scnearios: whether an expression equals to 0.
Moreover, we initiate the discussion of decidable subsets of the whole
language.
