DROPS

Document

DOI: 10.4230/LIPIcs.OPODIS.2016.18

WNetKAT: A Weighted SDN Programming and Verification Language

Authors: Kim G. Larsen, Stefan Schmid, and Bingtian Xue

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract

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 (and stateful) network functions and service chains. For example, WNetKAT allows to model flows which need to traverse certain waypoint functions, which can change the traffic rate. This paper also shows the relationship 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 shows the decidability of whether an expression equals to 0, which is sufficient in many practical scenarios, and we initiate the discussion of decidable subsets of the whole language.

Cite as

Kim G. Larsen, Stefan Schmid, and Bingtian Xue. WNetKAT: A Weighted SDN Programming and Verification Language. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:LIPIcs.OPODIS.2016.18,
  author =	{Larsen, Kim G. and Schmid, Stefan and Xue, Bingtian},
  title =	{{WNetKAT: A Weighted SDN Programming and Verification Language}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.18},
  URN =		{urn:nbn:de:0030-drops-70870},
  doi =		{10.4230/LIPIcs.OPODIS.2016.18},
  annote =	{Keywords: Software-Defined Networking, Verification, Reachability, Stateful Processing, Service Chains, Weighted Automata, Decidability, NetKAT}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2016.25

Probabilistic Mu-Calculus: Decidability and Complete Axiomatization

Authors: Kim G. Larsen, Radu Mardare, and Bingtian Xue

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract

We introduce a version of the probabilistic mu-calculus (PMC) built on top of a probabilistic modal logic that allows encoding n-ary inequational conditions on transition probabilities. PMC extends previously studied calculi and we prove that, despite its expressiveness, it enjoys a series of good meta-properties. Firstly, we prove the decidability of satisfiability checking by establishing the small model property. An algorithm for deciding the satisfiability problem is developed. As a second major result, we provide a complete axiomatization for the alternation-free fragment of PMC. The completeness proof is innovative in many aspects combining various techniques from topology and model theory.

Cite as

Kim G. Larsen, Radu Mardare, and Bingtian Xue. Probabilistic Mu-Calculus: Decidability and Complete Axiomatization. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:LIPIcs.FSTTCS.2016.25,
  author =	{Larsen, Kim G. and Mardare, Radu and Xue, Bingtian},
  title =	{{Probabilistic Mu-Calculus: Decidability and Complete Axiomatization}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.25},
  URN =		{urn:nbn:de:0030-drops-68607},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.25},
  annote =	{Keywords: Markov process, probabilistic modal mu-calculus, n-ary (in-)equational modalities, satisfiability, axiomatization}
}

Search Results

Documents authored by Xue, Bingtian

WNetKAT: A Weighted SDN Programming and Verification Language

Abstract

Cite as

Probabilistic Mu-Calculus: Decidability and Complete Axiomatization

Abstract

Cite as

Thanks for your feedback!

Could not send message