minor changes

Author: tfenz

_posts/2020-06-24-aalwines.md

@@ -40,7 +40,7 @@ that generate the routing tables from the control plane specifications.
 Let us consider the verification of forwarding rules in MPLS routing tables as an example.
 In a nutshell, in MPLS, packet labels can be nested 
 in order to provide tunneling through the network or to handle link
-failures by fast-reroute mechanism. This mechanism relies on pushing a new MPLS
+failures by the fast-reroute mechanism. The mechanism relies on pushing a new MPLS
 label on top of the label stack, to redirect the flow 
 to go around the failed link. This mechanism can be applied several times
 in case of multiple link failures, creating larger and larger (in theory: unbounded)
@@ -73,8 +73,8 @@ the regular expressions for the initial header and the final
 header of the query can each be converted to first a
 Nondeterministic Finite Automaton (NFA) and then to a Pushdown
 Automaton (PDA). The path query is converted to an NFA, which can then be used to restrict (by synchronous product)
-the behaviour of the PDA constructed based on the network model.
-The three PDAs can be combined into a single PDA that we can give
+the behavior of the PDA constructed based on the network model.
+The three PDAs can be combined into a single PDA that can be given
 to the backend engine that checks the emptiness of the PDA language. 
 In case the language is nonempty, we can return a witness trace
 to demonstrate the reason why the query is satisfied. All these operations can be performed in polynomial time, 
@@ -85,7 +85,7 @@ leveraging a classic result by J. Büchi.
 As a case study and to explore the feasibility of such an automata-theoretic approach, 
 we developed a framework, the AalWiNes suite, which allows to load an arbitrary network topology 
 (e.g., from the topology zoo dataset) as well as a set of router configurations (e.g., from Juniper routers). 
-The configurations are then put into a standardized, intermediate format which is vendor independent. 
+The configurations are put into a standardized, intermediate format which is vendor independent. 
 The user can then define a query as described above, which leads the tool to prompt with a result 
 (e.g. a trace). AalWiNes is a joint work at Aalborg University and the University of Vienna.
 
@@ -108,8 +108,8 @@ We refer to our [tool website](https://aalwines.cs.aau.dk/) as well as to our
 
 ## Conclusion and future work
 
-We consider providing a low runtime critical for the success of network verification, 
-and reasoning about failures seems particularly challenging. 
+Our aim is to provide a low runtime which is critical for the success of network
+verification, however, reasoning about failures seems particularly challenging with respect to the computational complexity. 
 While not every network may allow for a polynomial-time analysis,
 we see much potential in automata-theoretic approaches,
 and we hope this article can inspire the community to conduct more research 
@@ -119,7 +119,7 @@ We understand our approach as a first step and believe that it opens the door to
 verify many other infinite state systems whose configurations 
 cannot explicitly be represented anymore.
 For example, we have recently extended AalWiNes to support a witness trace generation which 
-accounts for additional metrics, and for example selects (among a possibly infinite number of witness traces) 
+accounts for additional metrics; for example, the tool can now select (among a possibly infinite number of witness traces) 
 the ones that minimize the number of hops, latency, or the stack height that corresponds to the number 
 of MPLS tunnels. This is
 achieved by extending the PDA reachability analysis with multi-dimensional weights.