1549 LABEL:LastPageJun. 18, 2018Nov. 14, 2019

# Flow Logic

Orna Kupferman  School of Computer Science and Engineering, The Hebrew
University, Israel  and  Gal Vardi<EMAIL_ADDRESS>
###### Abstract.

A flow network is a directed graph in which each edge has a capacity, bounding
the amount of flow that can travel through it. Flow networks have attracted a
lot of research in computer science. Indeed, many questions in numerous
application areas can be reduced to questions about flow networks. This
includes direct applications, namely a search for a maximal flow in networks,
as well as less direct applications, like maximal matching or optimal
scheduling. Many of these applications would benefit from a framework in which
one can formally reason about properties of flow networks that go beyond their
maximal flow.

We introduce _Flow Logics_ : modal logics that treat flow functions as
explicit first-order objects and enable the specification of rich properties
of flow networks. The syntax of our logic BFL⋆ (Branching Flow Logic) is
similar to the syntax of the temporal logic CTL⋆, except that atomic
assertions may be _flow propositions_ , like $>\gamma$ or $\geq\gamma$, for
$\gamma\in{\rm I}\\!{\rm N}$, which refer to the value of the flow in a
vertex, and that first-order quantification can be applied both to paths and
to flow functions. For example, the BFL⋆ formula ${\mathcal{E}}((\geq
100)\wedge AG({\mathit{low}}\rightarrow(\leq 20)))$ states that there is a
legal flow function in which the flow is above $100$ and in all paths, the
amount of flow that travels through vertices with low security is at most
$20$.

We present an exhaustive study of the theoretical and practical aspects of
BFL⋆, as well as extensions and fragments of it. Our extensions include flow
quantifications that range over non-integral flow functions or over maximal
flow functions, path quantification that ranges over paths along which non-
zero flow travels, past operators, and first-order quantification of flow
values. We focus on the model-checking problem and show that it is PSPACE-
complete, as it is for CTL⋆. Handling of flow quantifiers, however, increases
the complexity in terms of the network to ${\rm P}^{\rm NP}$, even for the LFL
and BFL fragments, which are the flow-counterparts of LTL and CTL. We are
still able to point to a useful fragment of BFL⋆ for which the model-checking
problem can be solved in polynomial time. Finally, we introduce and study the
query-checking problem for BFL⋆, where under-specified BFL⋆ formulas are used
for network exploration.

###### Key words and phrases:

Flow Network, Temporal Logic

This research has received funding from the European Research Council under
the EU’s 7-th Framework Programme (FP7/2007–2013) / ERC grant agreement no
278410.

##  1\. Introduction

A _flow network_ is a directed graph in which each edge has a capacity,
bounding the amount of flow that can travel through it. The amount of flow
that enters a vertex equals the amount of flow that leaves it, unless the
vertex is a _source_ , which has only outgoing flow, or a _target_ , which has
only incoming flow. The fundamental _maximum-flow problem_ gets as input a
flow network and searches for a maximal flow from the source to the target
[CLR90, GTT89]. The problem was first formulated and solved in the 1950’s
[FF56, FF62]. It has attracted much research on improved algorithms [EK72,
Din70, GT88, Mad16] and applications [AMO93].

The maximum-flow problem can be applied in many settings in which something
travels along a network. This covers numerous application domains, including
traffic in road or rail systems, fluids in pipes, currents in an electrical
circuit, packets in a communication network, and many more [AMO93]. Less
obvious applications involve flow networks that are constructed in order to
model settings with an abstract network, as in the case of scheduling with
constraints [AMO93] or elimination in partially completed tournaments [Sch66].
In addition, several classical graph-theory problems can be reduced to the
maximum-flow problem. This includes the problem of finding a maximum bipartite
matching, minimum path cover, maximum edge-disjoint or vertex-disjoint path,
and many more [CLR90, AMO93]. Variants of the maximum-flow problem can
accommodate further settings, like circulation problems, where there are no
sink and target vertices, yet there is a lower bound on the flow that needs to
be traversed along each edge [Tar85], networks with multiple source and target
vertices, networks with costs for unit flows, networks with multiple
commodities, and more [EIS76].

All the above applications reduce the problem at hand to the problem of
finding a maximal flow in a network. Often, however, one would like to reason
about properties of flow networks that go beyond their maximal flow. This is
especially true when the vertices or edges of the network attain information
to which the properties can refer. For example, the vertices of a network may
be labeled by their security level, and we may want to check whether all legal
flow functions are such that the flow in every low-security vertex is at most
$20$, or check whether there is a flow function in which more than $100$ units
of flow reach the target and still the flow in every low-security vertex is at
most $20$. As another example, assume that each vertex in the network is
labeled by the service provider that owns it, and we want to find a maximal
flow under the constraint that flow travels through vertices owned by at most
two providers.

The challenge of reasoning about properties of systems has been extensively
studied in the context of formal verification. In particular, in _temporal-
logic model checking_ [CE81, QS82], we check whether a system has a desired
property by translating the system into a labeled state-transition graph,
translating the property into a temporal-logic formula, and deciding whether
the graph satisfies the formula. Model checking is one of the notable success
stories of theoretical computer science, with exciting theoretical research
that is being transformed into industrial applications [CGP99, CHVB18]. By
viewing networks as labeled state-transition graphs, we can use existing
model-checking algorithms and tools in order to reason about the structural
properties of networks. We can check, for example, that every path from the
source to the target eventually visits a check-sum vertex. Most interesting
properties of flow networks, however, refer to flows and their values, and not
just to the structural properties of the network. Traditional temporal logics
do not support the specification and verification of such properties.

We introduce and study _Flow Logics_ : modal logics that treat flow functions
as explicit first-order objects and enable the specification of rich
properties of flow networks. The syntax of our logic BFL⋆ (Branching Flow
Logic) is similar to the syntax of the temporal logic CTL⋆, except that atomic
assertions are built from both atomic propositions and _flow propositions_ ,
like $>\gamma$ or $\geq\gamma$, for $\gamma\in{\rm I}\\!{\rm N}$, which refer
to the value of the flow in a vertex, and that first-order quantification can
be applied both to paths and to flow functions. Thus, in addition to the path
quantifiers $A$ (“for all paths”) and $E$ (“there exists a path”) that range
over paths, states formulas may contain the flow quantifiers ${\mathcal{A}}$
(“for all flow functions”) and ${\mathcal{E}}$ (“there exists a flow
function”). For example, the BFL⋆ formula ${\mathcal{E}}((\geq 100)\wedge
AG(\mathit{low}\rightarrow(\leq 20)))$ states the property discussed above,
namely that there is a flow function in which the value of the flow is at
least $100$, and in all paths, the value of flow that travels through in
vertices with low security is at most $20$.

We study the theoretical aspects of BFL⋆ as well as extensions and fragments
of it. We demonstrate their applications in reasoning about flow networks, and
we examine the complexity of their model-checking problem. Below we briefly
survey our results. (1) We show that while maximal flow can always be achieved
by integral flows [FF56], in the richer setting of flow logic, restricting
attention to integral flows may change the satisfaction value of formulas.
Accordingly, our semantics for BFL⋆ considers two types of flow
quantification: one over integral flows and another over _non-integral_ ones.
(2) We prove that bisimulation [Mil71] is not a suitable equivalence relation
for flow logics, which are sensitive to unwinding. We relate this to the
usefulness of _past operators_ in flow logic, and we study additional aspects
of the expressive power of BFL⋆. (3) We consider extensions of BFL⋆ by path
quantifiers that range over paths on which flow travels (rather than over all
paths in the network), and by _first-order quantification on flow values_. (4)
We study the model-checking complexity of BFL⋆, its extensions, and some
natural fragments. We show that algorithms for temporal-logic model-checking
can be extended to handle flow logics, and that the complexity of the BFL⋆
model-checking problem is PSPACE-complete. We study also the _network
complexity_ of the problem, namely the complexity in terms of the network,
assuming that the formula is fixed [LP85, KVW00], and point to a fragment of
BFL⋆ for which the model-checking problem can be solved in polynomial time.

One of the concepts that has emerged in the context of formal verification is
that of _model exploration_. The idea, as first noted by Chan in [Cha00], is
that, in practice, model checking is often used for understanding the system
rather than for verifying its correctness. Chan suggested to formalize model
exploration by means of _query checking_. The input to the query-checking
problem is a system $S$ and a query $\varphi$, where a query is a temporal-
logic formula in which some proposition is replaced by the place-holder “?”. A
solution to the query is a propositional assertion that, when replaces the
place-holder, results in a formula that is satisfied in $S$. For example,
solutions to the query $AG(?\rightarrow AX\mathit{grant})$ are assertions
$\psi$ for which $S\models AG(\psi\rightarrow AX\mathit{grant})$, thus
assertions that trigger a grant in all successive possible futures. A query
checker should return the strongest solutions to the query (strongest in the
sense that they are not implied by other solutions). The work of Chan was
followed by further work on query checking, studying its complexity, cases in
which only a single strongest solution exists, the case of multiple (possibly
related) place-holders, queries on semantic graphs, understanding business
processes through query checking and more [BG01, GC02, CG03, SV03, CGG07,
GRN12, RCM+14]. In the context of flow networks, the notion of model
explorations is of special interest, and there is on-going research on the
development of automatic tools for reasoning about networks and flow-
forwarding strategies (c.f., [BDVV18, ZST+10]). We develop a theory of query
checking for BFL⋆. We distinguish between _propositional queries_ , which, as
in the case of CTL⋆, seek strongest propositional assertions that may replace
a $?$ that serves as a state formula, and _value queries_ , which seek
strongest values that may replace a $?$ that serves as a bound in a flow
proposition. There, the strength of a solution depends on the tightness of the
bound it imposes. We show that while in the propositional case there may be
several partially ordered strongest solutions, in the value case the solutions
are linearly ordered and thus there is at most one strongest solution. The
existence of a single strongest solution has some nice practical applications.
In particular, we show that while for propositional queries, the problem of
finding all strongest solutions is very complex, for value queries its
complexity coincides with that of BFL⋆ model checking.

### Related work

There are three types of related works: (1) efforts to generalize the maximal-
flow problem to richer settings, (2) extensions of temporal logics by new
elements, in particular first-order quantification over new types, and (3)
works on logical aspects of networks and their use in formal methods. Below we
briefly survey them and their relation to our work.

As discussed early in this section, numerous extensions to the classical
maximal-flow problems have been considered. In particular, some works that add
constraints on the maximal flow, like capacities on vertices, or lower bounds
on the flow along edges. Closest to flow logics are works that refer to
labeled flow networks. For example, [GCSR13] considers flow networks in which
edges are labeled, and the problem of finding a maximal flow with a minimum
number of labels. Then, the maximal utilization problem of _capacitated
automata_ [KT14] amounts to finding maximal flow in a labeled flow network
where flow is constrained to travel only along paths that belong to a given
regular language. Our work suggests a formalism that embodies all these
extensions, as well as a framework for formally reasoning about many more
extensions and settings.

The competence of temporal-logic model checking initiated numerous extensions
of temporal logics, aiming to capture richer settings. For example, _real-
time_ temporal logics include clocks with a real-time domain [AH94],
_epistemic temporal logics_ include knowledge operators [HM90], and
_alternating temporal logics_ include game modalities [AHK02]. Closest to our
work is _strategy logic_ [CHP07], where temporal logic is enriched by first-
order quantification of strategies in a game. Beyond the theoretical interest
in strategy logic, it was proven useful in synthesizing strategies in multi-
agent systems and in the solution of rational synthesis [FKL10].

Finally, network verification is an increasingly important topic in the
context of protocol verification [KVM12]. Tools that allow verifying
properties of network protocols have been developed [WBLS09, LBG+15]. These
tools support verification of network protocols in the design phase as well as
runtime verification [KCZ+13]. Some of these tools use a query language called
_Network Datalog_ in order to specify network protocols [LCG+06]. Verification
of _Software Defined Networks_ has been studied widely, for example in
[KZZ+13, KPC+12, CVP+12]. Verification of safety properties in networks with
finite-state middleboxes was studied in [VAP+16]. Network protocols describe
forwarding policies for packets, and are thus related to specific flow
functions. However, the way traffic is transmitted in these protocols does not
correspond to the way flow travels in a flow network. Thus, properties
verified in this line of work are different from these we can reason about
with flow logic.

##  2\. The Flow Logic BFL⋆

A _flow network_ is $N=\langle AP,V,E,c,\rho,s,T\rangle$, where $AP$ is a set
of atomic propositions, $V$ is a set of vertices, $s\in V$ is a source vertex,
$T\subseteq V\setminus\\{s\\}$ is a set of target vertices,
$E\subseteq(V\setminus T)\times(V\setminus\\{s\\})$ is a set of directed
edges, $c:E\rightarrow{\rm I}\\!{\rm N}$ is a capacity function, assigning to
each edge an integral amount of flow that the edge can transfer, and
$\rho:V\rightarrow 2^{AP}$ assigns each vertex $v\in V$ to the set of atomic
propositions that are valid in $v$. Note that no edge enters the source vertex
or leaves a target vertex. We assume that all vertices $t\in T$ are reachable
from $s$ and that each vertex has at least one target vertex reachable from
it. For a vertex $u\in V$, let $E^{u}$ and $E_{u}$ be the sets of incoming and
outgoing edges to and from $u$, respectively. That is,
$E^{u}=(V\times\\{u\\})\cap E$ and $E_{u}=(\\{u\\}\times V)\cap E$.

A _flow_ is a function $f:E\rightarrow{\rm I}\\!{\rm N}$ that describes how
flow is directed in $N$. The capacity of an edge bounds the flow in it, thus
for every edge $e\in E$, we have $f(e)\leq c(e)$. All incoming flow must exit
a vertex, thus for every vertex $v\in V\setminus(\\{s\\}\cup T)$, we have
$\sum_{e\in E^{v}}f(e)=\sum_{e\in E_{v}}f(e)$. We extend $f$ to vertices and
use $f(v)$ to denote the flow that travels through $v$. Thus, for $v\in
V\setminus(\\{s\\}\cup T)$, we define $f(v)=\sum_{e\in E^{v}}f(e)=\sum_{e\in
E_{v}}f(e)$, for the source vertex $s$, we define $f(s)=\sum_{e\in
E_{s}}f(e)$, and for a target vertex $t\in T$, we define $f(t)=\sum_{e\in
E^{t}}f(e)$. Note that the preservation of flow in the internal vertices
guarantees that $f(s)=\sum_{t\in T}f(t)$, which is the amount of flow that
travels from $s$ to all the target vertices together. We say that a flow
function $f$ is _maximal_ if for every flow function $f^{\prime}$, we have
$f^{\prime}(s)\leq f(s)$. A maximal flow function can be found in polynomial
time [FF62]. The maximal flow for $N$ is then $f(s)$ for some maximal flow
function $f$.

The logic BFL⋆ is a _Branching Flow Logic_ that can specify properties of
networks and flows in them. As in CTL⋆, there are two types of formulas in
BFL⋆: _state formulas_ , which describe vertices in a network, and _path
formulas_ , which describe paths. In addition to the operators in CTL⋆, the
logic BFL⋆ has _flow propositions_ , with which one can specify the flow in
vertices, and _flow quantifiers_ , with which one can quantify flow functions
universally or existentially. When flow is not quantified, satisfaction is
defined with respect to both a network and a flow function. Formally, given a
set $AP$ of atomic propositions, a BFL⋆ state formula is one of the following:

  1. (S1):

An atomic proposition $p\in AP$.

  2. (S2):

A flow proposition $>\gamma$ or $\geq\gamma$, for an integer $\gamma\in{\rm
I}\\!{\rm N}$.

  3. (S3):

$\neg\varphi_{1}$ or $\varphi_{1}\vee\varphi_{2}$, for BFL⋆ state formulas
$\varphi_{1}$ and $\varphi_{2}$.

  4. (S4):

$A\psi$, for a BFL⋆ path formula $\psi$ (and $A$ is termed a _path
quantifier_).

  5. (S5):

${\mathcal{A}}\varphi$, for a BFL⋆ state formula $\varphi$ (and
${\mathcal{A}}$ is termed a _flow quantifier_).

A BFL⋆ path formula is one of the following:

  1. (P1):

A BFL⋆ state formula.

  2. (P2):

$\neg\psi_{1}$ or $\psi_{1}\vee\psi_{2}$, for BFL⋆ path formulas $\psi_{1}$
and $\psi_{2}$.

  3. (P3):

$X\psi_{1}$ or $\psi_{1}U\psi_{2}$, for BFL⋆ path formulas $\psi_{1}$ and
$\psi_{2}$.

We say that a BFL⋆ formula $\varphi$ is _closed_ if all flow propositions
appear in the scope of a flow quantifier. The logic BFL⋆ consists of the set
of closed BFL⋆ state formulas. We refer to state formula of the form
${\mathcal{A}}\varphi$ as a _flow state formula_.

The semantics of BFL⋆ is defined with respect to vertices in a flow network.
Before we define the semantics, we need some more definitions and notations.
Let $N=\langle AP,V,E,c,\rho,s,T\rangle$. For two vertices $u$ and $w$ in $V$,
a finite sequence $\pi=v_{0},v_{1},\ldots,v_{k}\in V^{*}$ of vertices is a
_$(u,w)$ -path_ in $N$ if $v_{0}=u$, $v_{k}=w$, and $\langle
v_{i},v_{i+1}\rangle\in E$ for all $0\leq i<k$. If $w\in T$, then $\pi$ is a
_target $u$-path_.

State formulas are interpreted with respect to a vertex $v$ in $N$ and a flow
function $f:E\rightarrow{\rm I}\\!{\rm N}$. When the formula is closed,
satisfaction is independent of the function $f$ and we omit it. We use
$v,f\models\varphi$ to indicate that the vertex $v$ satisfies the state
formula $\varphi$ when the flow function is $f$. The relation $\models$ is
defined inductively as follows.

  1. (S1):

For an atomic proposition $p\in AP$, we have that $v,f\models p$ iff
$p\in\rho(v)$.

  2. (S2):

For $\gamma\in{\rm I}\\!{\rm N}$, we have $v,f\models>\gamma$ iff
$f(v)>\gamma$ and $v,f\models\geq\gamma$ iff $f(v)\geq\gamma$.

  3. (S3a):

$v,f\models\neg\varphi_{1}$ iff $v,f\not\models\varphi_{1}$.

  4. (S3b):

$v,f\models\varphi_{1}\vee\varphi_{2}$ iff $v,f\models\varphi_{1}$ or
$v,f\models\varphi_{2}$.

  5. (S4):

$v,f\models A\psi$ iff for all target $v$-paths $\pi$, we have that
$\pi,f\models\psi$.

  6. (S5):

$v,f\models{\mathcal{A}}\varphi$ iff for all flow functions $f^{\prime}$, we
have $v,f^{\prime}\models\varphi$.

Path formulas are interpreted with respect to a finite path $\pi$ in $N$ and a
flow function $f:E\rightarrow{\rm I}\\!{\rm N}$. We use $\pi,f\models\varphi$
to indicate that the path $\pi$ satisfies the path-flow formula $\psi$ when
the flow function is $f$. The relation $\models$ is defined inductively as
follows. Let $\pi=v_{0},v_{1},\ldots,v_{k}$. For $0\leq i\leq k$, we use
$\pi^{i}$ to denote the suffix of $\pi$ that starts at $v_{i}$, thus
$\pi^{i}=v_{i},v_{i+1},\ldots,v_{k}$.

  1. (P1):

For a state formula $\varphi$, we have that $\pi,f\models\varphi$ iff
$v_{0},f\models\varphi$.

  2. (P2a):

$\pi,f\models\neg\psi$ iff $\pi,f\not\models\psi$.

  3. (P2b):

$\pi,f\models\psi_{1}\vee\psi_{2}$ iff $\pi,f\models\psi_{1}$ or
$\pi,f\models\psi_{2}$.

  4. (P3a):

$\pi,f\models X\psi_{1}$ iff $k>0$ and $\pi^{1},f\models\psi_{1}$.

  5. (P3b):

$\pi,f\models\psi_{1}U\psi_{2}$ iff there is $j\leq k$ such that
$\pi^{j},f\models\psi_{2}$, and for all $0\leq i<j$, we have
$\pi^{i},f\models\psi_{1}$

For a network $N$ and a closed BFL⋆ formula $\varphi$, we say that $N$
satisfies $\varphi$, denoted $N\models\varphi$, iff $s\models\varphi$ (note
that since $\varphi$ is closed, we do not specify a flow function).

Additional Boolean connectives and modal operators are defined from $\neg$,
$\vee$, $X$, and $U$ in the usual manner; in particular, $F\psi\,=\,{\bf
true}U\psi$ and $G\psi\,=\,\neg F\neg\psi$. We also define dual and
abbreviated flow propositions: $(<\gamma)=\neg(\geq\gamma)$,
$(\leq\gamma)=\neg(>\gamma)$, and
$(\gamma)=(=\gamma)=(\leq\gamma)\wedge(\geq\gamma)$, a dual path quantifier:
$E\psi=\neg A\neg\psi$, and a dual flow quantifier:
${\mathcal{E}}\varphi=\neg{\mathcal{A}}\neg\varphi$.

Consider a network $N$ in which target vertices are labeled by an atomic
proposition $\mathit{target}$, and low-security vertices are labeled
$\mathit{red}$. The BFL⋆ formula ${\mathcal{E}}EF(\mathit{target}\wedge(=20))$
states that there is a flow in which $20$ units reach a target vertex, and the
BFL⋆ formula ${\mathcal{A}}((\geq 20)\rightarrow AX(\geq 4))$ states that in
all flow functions in which the flow at the source is at least $20$, all the
successors must have flow of at least $4$. Finally, ${\mathcal{E}}((\geq
100)\wedge AG(\mathit{red}\rightarrow(\leq 20)))$ states that there is a flow
of at least $100$ in which the flow in every low-security vertex is at most
$20$, whereas ${\mathcal{A}}((>200)\rightarrow EF(\mathit{red}\wedge(>20)))$
states that when the flow is above $200$, then there must exist a low-security
vertex in which the flow is above $20$. As an example to a BFL⋆ formula with
an alternating nesting of flow quantifiers, consider the formula
${\mathcal{E}}AG(<10\rightarrow{\mathcal{A}}<15)$, stating that there is a
flow such that wherever the flow is below $10$, then in every flow it would be
below $15$. ∎

######  Remark 1.

Note that while the semantics of CTL⋆ and LTL is defined with respect to
infinite trees and paths, path quantification in BFL⋆ ranges over finite
paths. We are still going to use techniques and results known for CTL⋆ and LTL
in our study. Indeed, for upper bounds, the transition to finite computations
only makes the setting simpler. Also, lower-bound proofs for CTL⋆ and LTL are
based on an encoding of finite runs of Turing machines, and apply also to
finite paths.

Specifying finite paths, we have a choice between a weak and a strong
semantics for the $X$ operator. In the weak semantics, the last vertex in a
path satisfies $X\psi$, for all $\psi$. In particular, it is the only vertex
that satisfies $X{\bf false}$. In the strong semantics, the last vertex does
not satisfy $X\psi$, for all $\psi$. In particular, it does not satisfy $X{\bf
true}$. We use the strong semantics.

##  3\. Properties of BFL⋆

###  3.1. Integral vs. non-integral flow functions

Our semantics of BFL⋆ considers _integral flow functions_ : vertices receive
integral incoming flow and partition it to integral flows in the outgoing
edges. Integral-flow functions arise naturally in settings in which the
objects we transfer along the network cannot be partitioned into fractions, as
is the case with cars, packets, and more. Sometimes, however, as in the case
of liquids, flow can be partitioned arbitrarily. In the traditional maximum-
flow problem, it is well known that the maximum flow can be achieved by
integral flows [FF56]. We show that, interestingly, in the richer setting of
flow logic, restricting attention to integral flows may change the
satisfaction value of formulas.

######  Proposition 2.

Allowing the quantified flow functions in BFL⋆ to get values in ${\rm
I}\\!{\rm R}$ changes its semantics.

######  Proof 3.1.

Consider the network on the right. The BFL⋆ formula
$\varphi={\mathcal{E}}(1\wedge AX(>0))$ states that there is a flow function
in which the flow that leaves the source is $1$ and the flow of both its
successors is strictly positive. It is easy to see that while no integral flow
function satisfies the requirement in $\varphi$, a flow function in which $1$
unit of flow in $s$ is partitioned between $u$ and $v$ does satisfy it.

Proposition 2 suggests that quantification of flow functions that allow non-
integral flows may be of interest. In Section 4.3 we discuss such an
extension.

###  3.2. Sensitivity to unwinding

For a network $N=\langle AP,V,E,c,\rho,s,T\rangle$, let $N_{t}$ be the
unwinding of $N$ into a tree. Formally, $N_{t}=\langle
AP,V^{\prime},E^{\prime},\rho^{\prime},s,T^{\prime}\rangle$, where
$V^{\prime}\subseteq V^{*}$ is the smallest set such that $s\in V^{\prime}$,
and for all $w\cdot v\in V^{\prime}$ with $w\in V^{*}$ and $v\in V\setminus
T$, and all $u\in V$ such that $E(v,u)$, we have that $w\cdot v\cdot u\in
V^{\prime}$, with $\rho^{\prime}(w\cdot v\cdot u)=\rho(u)$. Also, $\langle
w\cdot v,w\cdot v\cdot u\rangle\in E^{\prime}$, with $c^{\prime}(\langle
w\cdot v,w\cdot v\cdot u\rangle)=c(\langle v,u\rangle)$. Finally,
$T^{\prime}=V^{\prime}\cap(V^{*}\cdot T)$. Note that $N_{t}$ may be infinite.
Indeed, a cycle in $N$ induces infinitely many vertices in $N_{t}$.

The temporal logic CTL⋆ is insensitive to unwinding. Indeed, $N$ and $N_{t}$
are bisimilar, and for every CTL⋆ formula $\varphi$, we have $N\models\varphi$
iff $N_{t}\models\varphi$ [Mil71]. We show that this is not the case for BFL⋆.

######  Proposition 3.

The value of the maximal flow is sensitive to unwinding.

######  Proof 3.2.

Consider the network $N$ appearing in Figure 1 (with the target $T=\\{t\\}$),
and its unwinding $N_{t}$ which appears in its right. It is easy to see that
the value of the maximal flow in $N$ is $7$, and the value of the maximal flow
from $s$ to $T^{\prime}$ in $N_{t}$ is $8$.

Figure 1. The flow network $N$ and its unwinding $N_{t}$

######  Corollary 4.

The logic BFL⋆ is sensitive to unwinding.

The sensitivity of BFL⋆ to unwinding suggests that extending BFL⋆ with past
operators can increase its expressive power. In Section 4.4, we discuss such
an extension.

##  4\. Extensions and Fragments of BFL⋆

In this section we discuss useful extensions and variants of BFL⋆, as well as
fragments of it. As we shall show in the sequel, while the extensions come
with no computational price, their model checking requires additional
techniques.

###  4.1. Positive path quantification

Consider a network $N=\langle AP,V,E,c,\rho,s,T\rangle$ and a flow function
$f:E\rightarrow{\rm I}\\!{\rm N}$. We say that a path
$\pi=v_{0},v_{1},\ldots,v_{k}$ is positive if the flow along all the edges in
$\pi$ is positive. Formally, $f(v_{i},v_{i+1})>0$, for all $0\leq i<k$. Note
that it may be that $f(v_{i})>0$ for all $0\leq i<k$ and still $\pi$ is not
positive. It is sometimes desirable to restrict the range of path
quantification to paths along which flow travels. This is the task of the
_positive path quantifier_ $A^{+}$, with the following semantics.

  * •

$v,f\models A^{+}\psi$ iff for all positive target $v$-paths $\pi$, we have
that $\pi,f\models\psi$.

Dually, $E^{+}\psi=\neg A^{+}\neg\psi$.

Let $W$ be a set of workers and $J$ be a set of jobs. Each worker $w\in W$ can
be assigned to perform jobs from a subset $J_{w}\subseteq J$. It is required
to perform all jobs by assigning exactly one worker to each job and at most
two jobs to each worker. This problem can be solved using the flow network
appearing in Figure 2. The vertices on the left column correspond to the
workers, these on the right column correspond to the jobs, and there is an
edge between a worker $w$ and a job $j$ iff $j\in J_{w}$. The capacity of all
edges is $1$, except for these from the source $s$ to the worker vertices,
which have capacity $2$. It is easy to see that a flow of $k$ units in the
network described in Figure 2 corresponds to a legal assignment in which $k$
jobs are performed. Assume now that some jobs should be processed in Location
$a$ and the others in Location $b$. A worker can process jobs only in a single
location, $a$ or $b$. By labeling the job-vertices by their location, the
existence of a legal assignment in which $k$ jobs are processed can be
expressed by the BFL⋆ formula

${\mathcal{E}}(k\wedge AX(A^{+}Xa\vee A^{+}Xb)),$

which uses positive path quantification. ∎

Figure 2. Assigning workers to jobs.

###  4.2. Maximal flow quantification

It is sometimes desirable to restrict the range of flow quantification to
maximal flow functions. This is the task of the _maximal-flow quantifier_
${\mathcal{A}}^{\mathit{max}}$, with the following semantics.

  * •

$v,f\models{\mathcal{A}}^{\mathit{max}}\varphi$ iff for all maximal-flow
functions $f^{\prime}$, we have that $v,f^{\prime}\models\varphi$.

Dually,
${\mathcal{E}}^{\mathit{max}}\varphi=\neg{\mathcal{A}}^{\mathit{max}}\neg\varphi$.

In a similar manner, it is sometimes helpful to relate to the maximal flow in
the network. The max-flow constant $\gamma_{\mathit{max}}\in N$ maintains the
value of the maximal flow from $s$ to $T$. We also allow arithmetic operations
on $\gamma_{\mathit{max}}$.

Recall the job-assignment problem from Example 4.1. The BFL⋆ formula

${\mathcal{E}}^{\mathit{max}}(AX(A^{+}Xa\vee A^{+}Xb))$

states that the requirements about the locations do not reduce the number of
jobs assigned without this requirement. Then, the formula

${\mathcal{E}}((\geq\gamma_{\mathit{max}}-4)\wedge AX(A^{+}Xa\vee A^{+}Xb))$

states that the requirements about the locations may reduce the number of jobs
performed by at most $4$. ∎

###  4.3. Non-integral flow quantification

As discussed in Section 3.1, letting flow quantification range over non-
integral flow functions may change the satisfaction value of a BFL⋆ formula.

Such a quantification is sometimes desirable, and we extend BFL⋆ with a _non-
integral flow quantifier_ ${\mathcal{A}}^{{\rm I}\\!{\rm R}}$, with the
following semantics.

  * •

$v,f\models{\mathcal{A}}^{{\rm I}\\!{\rm R}}\varphi$ iff for all flow
functions $f^{\prime}:E\rightarrow{\rm I}\\!{\rm R}^{+}$, we have that
$v,f^{\prime}\models\varphi$.

Dually, ${\mathcal{E}}^{{\rm I}\\!{\rm R}}\varphi=\neg{\mathcal{A}}^{{\rm
I}\\!{\rm R}}\neg\varphi$.

###  4.4. Past operators

As discussed in Section 3.2, while temporal logics are insensitive to
unwinding, this is not the case for BFL⋆. Intuitively, this follows from the
fact that the flow in a vertex depends on the flow it gets from all its
predecessors. This dependency suggests that an explicit reference to
predecessors is useful, and motivates the extension of BFL⋆ by past operators.

Adding past to a branching logic, one can choose between a linear-past
semantics — one in which past is unique (technically, the semantics is with
respect to an unwinding of the network), and a branching-past semantics — one
in which all the possible behaviors that lead to present are taken into an
account (technically, the semantics is dual to that of future operators, and
is defined with respect to the network) [KPV12]. For flow logics, the
branching-past approach is the suitable one, and is defined as follows.

For a path $\pi=v_{0},v_{1},\ldots,v_{k}\in V^{*}$, a vertex $v\in V$, and
index $0\leq i\leq k$, we say that $\pi$ is a source-target $(v,i)$-path if
$v_{0}=s$, $v_{i}=v$, and $v_{k}\in T$. We add to BFL⋆ two past modal
operators, $Y$ (“Yesterday”) and $S$ (“Since”), and adjust the semantics as
follows. Defining the semantics of logics that refer to the past, the
semantics of path formulas is defined with respect to a path and an index in
it. We use $\pi,i,f\models\psi$ to indicate that the path $\pi$ satisfies the
path formula $\psi$ from position $i$ when the flow function is $f$. For state
formulas, we adjust the semantics as follows.

  1. (S4):

$v,f\models A\psi$ iff for all $i$ and for all source-target $(v,i)$-paths
$\pi$, we have that $\pi,i,f\models\psi$.

Then, for path formulas, we have the following (the adjustment to refer to the
index $i$ in all other modalities is similar).

  * •

$\pi,i,f\models Y\psi_{1}$ iff $i>0$ and $\pi,i-1,f\models\psi_{1}$.

  * •

$\pi,i,f\models\psi_{1}S\psi_{2}$ iff there is $0\leq j<i$ such that
$\pi,j,f\models\psi_{2}$, and for all $j+1\leq l\leq i$, we have
$\pi,l,f\models\psi_{1}$.

Recall the job-assignment problem from Example 4.1. Assume that some of the
workers have cars, which is indicated by an atomic proposition $\mathit{car}$
that may label worker vertices. Also, say that a job is a _transit job_ if it
can be assigned only to workers with cars. Assume that we want to apply the
restriction about the single location only to non-transit jobs. Thus, if all
the predecessors of a job-vertex are labeled by car, then this job can be
served in either locations. Using past operators, we can specify this property
by the formula

${\mathcal{E}}(k\wedge AX(A^{+}X(a\vee AY\mathit{car})\vee A^{+}X(b\vee
AY\mathit{car}))).$

∎

###  4.5. First-Order quantification on flow values

The flow propositions in BFL⋆ include constants. This makes it impossible to
relate the flow in different vertices other than specifying all possible
constants that satisfy the relation. In _BFL ⋆ with quantified flow values_ we
add flow variables $X=\\{x_{1},\ldots,x_{n}\\}$ that can be quantified
universally or existentially and specify such relations conveniently. We also
allow the logic to apply arithmetic operations on the values of variables in
$X$.

For a set of arithmetic operators $O$ (that is, $O$ may include $+,*$, etc.),
let BFL${}^{\star}(O)$ be BFL⋆ in which Rule S2 is extended to allow
expressions with variables in $X$ constructed by operators in $O$, and we also
allow quantification on the variables in $X$. Formally, we have the following:

  1. (S2)

A flow proposition $>g(x_{1},\ldots,x_{k})$ or $\geq~{}g(x_{1},\ldots,x_{k})$,
where $x_{1},\ldots,x_{k}$ are variables in $X$ and $g$ is an expression
obtained from $x_{1},\ldots,x_{k}$ by applying operators in $O$, possibly
using constants in ${\rm I}\\!{\rm N}$. We assume that $g:{\rm I}\\!{\rm
N}^{k}\rightarrow{\rm I}\\!{\rm N}$. That is, $g$ leaves us in the domain
${\rm I}\\!{\rm N}$.

  2. (S6)

$\forall x\varphi$, for $x\in X$ and a BFL${}^{\star}(O)$ formula $\varphi$ in
which $x$ is free.

For a BFL${}^{\star}(O)$ formula $\varphi$ in which $x$ is a free variable,
and a constant $\gamma\in{\rm I}\\!{\rm N}$, let $\varphi[x\leftarrow\gamma]$
be the formula obtained by assigning $\gamma$ to $x$ and replacing expressions
by their evaluation. Then, $v,f\models\forall x\varphi^{\prime}$ iff for all
$\gamma\in{\rm I}\\!{\rm N}$, we have that
$v,f\models\varphi^{\prime}[x\leftarrow\gamma]$.

The logic BFL${}^{\star}(\emptyset)$ includes the formula
${\mathcal{E}}AG\forall x((\mathit{split}\wedge x\>\wedge>0)\rightarrow
EX(>0\>\wedge<x))$, stating that there is a flow in which all vertices that
are labeled split and with a positive flow $x$ have a successor in which the
flow is positive but strictly smaller than $x$. Then, BFL${}^{\star}({\rm
div})$ includes the formula ${\mathcal{E}}AG\forall x(x\rightarrow EX(\geq x\
{\rm div}\ 2))$, stating that there is a flow in which all vertices have a
successor that has at least half of their flow.

Finally, BFL${}^{\star}(+)$ includes the formula $\exists x\exists
y{\mathcal{E}}^{\mathit{max}}AG(\neg(\mathit{source}\vee\mathit{target})\rightarrow
x\vee y\vee(x+y))$, stating that there are values $x$ and $y$, such that it is
possible to attain the maximal flow by assigning to all vertices, except maybe
source and target vertices, values in $\\{x,y,x+y\\}$. ∎

###  4.6. Fragments of BFL⋆

For the temporal logic CTL⋆, researchers have studied several fragments, most
notably LTL and CTL. In this section we define interesting fragments of BFL⋆.

Flow-CTL⋆ and Flow-LTL. The logics _Flow-CTL ⋆_ and _Flow-LTL_ are extensions
of CTL⋆ and LTL in which atomic state formulas may be, in addition to $AP$s,
also the flow propositions $>\gamma$ or $\geq\gamma$, for an integer
$\gamma\in{\rm I}\\!{\rm N}$. Thus, no quantification on flow is allowed, but
atomic formulas may refer to flow. The semantics of Flow-CTL⋆ is defined with
respect to a network and a flow function, and that of Flow-LTL is defined with
respect to a path in a network and a flow function.

Linear Flow Logic. The logic LFL is the fragment of BFL⋆ in which only one
external universal path quantification is allowed. Thus, an LFL formula is a
BFL⋆ formula of the form $A\psi$, where $\psi$ is generated without Rule S4.

Note that while the temporal logic LTL is a “pure linear” logic, in the sense
that satisfaction of an LTL formula in a computation of a system is
independent of the structure of the system, the semantics of LFL mixes linear
and branching semantics. Indeed, while all the paths in $N$ have to satisfy
$\psi$, the context of the system is important. To see this, consider the LFL
formula $\varphi=A{\mathcal{A}}((\geq 10)\rightarrow X(\geq 4))$. The formula
states that in all paths, all flow functions in which the flow at the first
vertex in the path is at least $10$, are such that the flow at the second
vertex in the path is at least $4$. In order to evaluate the path formula
${\mathcal{A}}((\geq 10)\rightarrow X(\geq 4))$ in a path $\pi$ of a network
$N$ we need to know the capacity of all the edges from the source of $N$, and
not only the capacity of the first edge in $\pi$. For example, $\varphi$ is
satisfied in networks in which the source $s$ has two successors, each
connected to $s$ by an edge with capacity $4$, $5$, or $6$. Consider now the
LFL formula $\varphi^{\prime}=A{\mathcal{E}}(10\wedge X(\geq 4))$. Note that
$\varphi^{\prime}$ is not equal to the BFL⋆ formula
$\theta={\mathcal{E}}(10\wedge AX(\geq 4))$. Indeed, in the latter, the same
flow function should satisfy the path formula $X(\geq 4)$ in all paths.

No nesting of flow quantifiers. The logic BFL${}^{\star}_{1}$ contains
formulas that are Boolean combinations of formulas of the form
${\mathcal{E}}\varphi$ and ${\mathcal{A}}\varphi$, for a Flow-CTL⋆ formula
$\varphi$. Of special interest are the following fragments of
BFL${}^{\star}_{1}$:

  * •

$\exists$BFL${}^{\star}_{1}$ and $\forall$BFL${}^{\star}_{1}$, where formulas
are of the form ${\mathcal{E}}\varphi$ and ${\mathcal{A}}\varphi$,
respectively, for a Flow-CTL⋆ formula $\varphi$.

  * •

$\exists$LFL1 and $\forall$LFL1, where formulas are of the form
${\mathcal{E}}A\psi$ and ${\mathcal{A}}A\psi$, respectively, for a Flow-LTL
formula $\psi$, and LFL1, where a formula is a Boolean combination of
$\exists$LFL1 and $\forall$LFL1 formulas.

Conjunctive-BFL⋆. The fragment Conjunctive-BFL⋆ (CBFL⋆, for short) contains
BFL⋆ formulas whose flow state sub-formulas restrict the quantified flow in a
conjunctive way. That is, when we “prune” a CBFL⋆ formula into requirements on
the network, atomic flow propositions are only conjunctively related. This
would have a computational significance in solving the model-checking problem.

Consider an $\exists$BFL${}^{\star}_{1}$ formula
$\varphi={\mathcal{E}}\theta$. We say that an operator
$g\in\\{\vee,\wedge,E,A,X,F,G,U\\}$ has a _positive polarity_ in $\varphi$ if
all the occurrences of $g$ in $\theta$ are in a scope of an even number of
negations. Dually, $g$ has a _negative polarity_ in $\varphi$ if all its
occurrences in $\theta$ are in a scope of an odd number of negations.

In order to define CBFL⋆, let us first define the fragments
$\exists$CBFL${}^{\star}_{1}$ of $\exists$BFL${}^{\star}_{1}$ and
$\forall$CBFL${}^{\star}_{1}$ of $\forall$BFL${}^{\star}_{1}$, which
constitute the inner level of CBFL⋆. The logic $\exists$CBFL${}^{\star}_{1}$
is a fragment of $\exists$BFL${}^{\star}_{1}$ in which the only operators with
a positive polarity are $\wedge$, $A$, $X$, and $G$, and the only operators
with a negative polarity are $\vee$, $E$, $X$, and $F$. Note that $U$ is not
allowed, as its semantics involves both conjunctions and disjunctions. Note
that by pushing negations inside, we make all operators of a positive
polarity; that is, we are left only with $\wedge$, $A$, $X$, and $G$. Then,
since all requirements are universal and conjunctively related, we can push
conjunctions outside so that path formulas do not have internal conjunctions —
for example, transform $AX(\xi_{1}\wedge\xi_{2})$ into $AX\xi_{1}\wedge
AX\xi_{2}$, and can get rid of universal path quantification that is nested
inside another universal path quantification — for example, transform
$AXAX\xi_{1}$ into $AXX\xi$. Finally, since we use the strong semantics to
$X$, we can replace formulas that have $X$ nested inside $G$ by ${\bf false}$.
The logic $\forall$CBFL${}^{\star}_{1}$ is the dual fragment of
$\forall$BFL${}^{\star}_{1}$. In other words, ${\mathcal{A}}\theta$ is in
$\forall$CBFL${}^{\star}_{1}$ iff ${\mathcal{E}}\neg\theta$ is in
$\exists$CBFL${}^{\star}_{1}$.

Intuitively, the logic CBFL⋆ is obtained by going up a hierarchy in which
formulas of lower levels serve as atomic propositions in higher levels. We now
define the syntax of CBFL⋆ formally. For simplicity, we define it in a normal
form, obtained by applying the rules described above. A CBFL${}^{\star}_{0}$
formula is a Boolean assertion over $AP$. For $i\geq 0$, a
CBFL${}^{\star}_{i+1}$ formula is a Boolean assertion over
CBFL${}^{\star}_{i}$ formulas and formulas of the form
${\mathcal{E}}(A\psi_{1}\wedge\cdots\wedge A\psi_{n})$, where $\psi_{j}$ is of
the form $X^{k_{j}}\xi_{j}$ or $X^{k_{j}}G\xi_{j}$, where $k_{j}\geq 0$ and
$\xi_{j}$ is a CBFL${}^{\star}_{i}$ formula or a flow proposition (that is,
$>\gamma$, $<\gamma$, $\geq\gamma$, or $\leq\gamma$, for an integer
$\gamma\in{\rm I}\\!{\rm N}$). Then, a CBFL⋆ formula is a CBFL${}^{\star}_{i}$
formula for some $i\geq 0$. Note that both $\exists$CBFL${}^{\star}_{1}$ and
$\forall$CBFL${}^{\star}_{1}$ are contained in CBFL${}^{\star}_{1}$.

Recall the job-assignment problem from Example 4.1. The CBFL${}^{\star}_{1}$
formula ${\mathcal{A}}(<10\rightarrow EX\leq 0)\wedge{\mathcal{E}}(15\wedge
AX\geq 1)$ states that if less than $10$ jobs are processed, then at least one
worker is unemployed, but it is possible to process $15$ jobs and let every
worker process at least one job.

BFL. The logic BFL is the fragment of BFL⋆ in which every modal operator
($X,U$) is immediately preceded by a path quantifier. That is, it is the flow
counterpart of CTL. As we are going to show, while in temporal logic, the
transition from CTL⋆ to CTL significantly reduces model-checking complexity,
this is not the case for BFL.

######  Remark 5.

As demonstrated in the examples, the extensions of BFL⋆ simplifies the
specification of natural properties. We do not, however, study the expressive
power of the extensions and fragments. For some, results about expressive
power follow from known results about CTL⋆. For example, as proven in [KPV12],
adding past to CTL⋆ with a branching-past semantics strictly increases its
expressive power. The same arguments can be used in order to show that BFL⋆
with past operators is strictly more expressive than BFL⋆.111We note that the
result from [KPV12] does not immediately imply the analogous result for BFL⋆,
as it might be the case that the flow operators somehow cover up for the extra
power of the branching-past temporal operator. In particular, the proof in
[KPV12] is based on the fact that only CTL⋆ with past operators is sensitive
to unwinding and, as we prove in Section 3.2, BFL⋆ is sensitive to unwinding.
Still, since the specific formula used in [KPV12] in order to prove the
sensitivity of CTL⋆ with past to unwinding does not refer to flow, it is easy
to see that it has no equivalent BFL⋆ formula. Likewise, it is easy to show
that BFL⋆ is strictly more expressive than BFL. On the other hand, it is not
hard to see that quantification over the maximum flow can be expressed by
first-order quantification on flow values. Indeed,
${\mathcal{E}}^{\mathit{max}}\psi$ is equivalent to $\exists
x{\mathcal{E}}((=x)\wedge\psi\wedge{\mathcal{A}}(\leq x))$. Likewise, it may
well be that every BFL⋆ formula with non-integral flow quantifiers has an
equivalent one without such quantifiers, or that positive path quantification
can be expressed by first-order quantification on flow values. We leave the
study of the expressive power and relative succinctness of the various logics
to future research.

##  5\. Model Checking

In this section we study the model-checking problem for BFL⋆. The problem is
to decide, given a flow network $N$ and a BFL⋆ formula $\varphi$, whether
$N\models\varphi$.

######  Theorem 6.

BFL⋆ model checking is PSPACE-complete.

######  Proof 5.1.

Consider a network $N$ and a BFL⋆ formula $\varphi$. The idea behind our
model-checking procedure is similar to the one that recursively employs LTL
model checking in the process of CTL⋆ model checking [EL87]. Here, however,
the setting is more complicated. Indeed, the path formulas in BFL⋆ are not
“purely linear”, as the flow quantification in them refers to flow in the
(branching) network. In addition, while the search for witness paths is
restricted to paths in the network, which can be guessed on-the-fly in the
case of LTL, here we also search for witness flow functions, which have to be
guessed in a global manner.

Let $\\{\varphi_{1},\ldots,\varphi_{k}\\}$ be the set of flow state formulas
in $\varphi$. Assume that $\varphi_{1},\ldots,\varphi_{k}$ are ordered so that
for all $1\leq i\leq k$, all the subformulas of $\varphi_{i}$ have indices in
$\\{1,\ldots,i\\}$. Our model-checking procedure labels $N$ by new atomic
propositions $q_{1},\ldots,q_{k}$ so that for all vertices $v$ and $1\leq
i\leq k$, we have that $v\models q_{i}$ iff $v\models\varphi_{i}$ (note that
since $\varphi_{i}$ is closed, satisfaction is independent of a flow
function).

Starting with $i=1$, we model check $\varphi_{i}$, label $N$ with $q_{i}$, and
replace the subformula $\varphi_{i}$ in $\varphi$ by $q_{i}$. Accordingly,
when we handle $\varphi_{i}$, it is an $\exists$BFL${}^{\star}_{1}$ or a
$\forall$BFL${}^{\star}_{1}$ formula. That is, it is of the form
${\mathcal{E}}\xi$ or ${\mathcal{A}}\xi$, for a Flow-CTL⋆ formula $\xi$.
Assume that $\varphi_{i}={\mathcal{E}}\xi$. We guess a flow function
$f:E\rightarrow{\rm I}\\!{\rm N}$, and perform CTL⋆ model-checking on $\xi$,
evaluating the flow propositions in $\xi$ according to $f$. Since guessing $f$
requires polynomial space, and CTL⋆ model checking is in PSPACE, so is
handling of $\varphi_{i}$ and of all the subformulas.

Hardness in PSPACE follows from the hardness of CTL⋆ model checking [SC85].

Since BFL⋆ contains CTL⋆, the lower bound in Theorem 6 is immediate. One may
wonder whether reasoning about flow networks without atomic propositions,
namely when we specify properties of flow only, is simpler. Theorem 7 below
shows that this is not the case. Essentially, the proof follows from our
ability to encode assignments to atomic propositions by values of flow.

######  Theorem 7.

BFL⋆ model checking is PSPACE-complete already for $\forall$LFL1 formulas
without atomic propositions.

######  Proof 5.2.

We describe a reduction from LTL satisfiability, which is PSPACE-hard [SC85].
As discussed in Remark 1, PSPACE-hardness applies already to LTL over finite
computations.

Consider an LTL formula $\psi$. For simplicity, we assume that $\psi$ is over
a single atomic proposition $p$. Indeed, LTL satisfiability is PSPACE-hard
already for this fragment. We construct a flow network $N$ and an
$\forall$LFL1 formula $\varphi$ such that $N$ does not satisfy $\varphi$ iff
some computation in ${\\{p,\neg p\\}}^{*}$ satisfies $\psi$. The network $N$
appears in Figure 3. Note that when $s$ has a flow of $1$, then exactly one of
$v_{p}$ and $v_{\neg p}$ has a flow of $1$. Let $\psi^{\prime}$ be the Flow-
LTL formula obtained from $\psi$ be replacing all occurrences of $p$ by $\geq
1$. We define $\varphi={\mathcal{A}}A(1\rightarrow X\neg\psi^{\prime})$. Thus,
$\neg\varphi={\mathcal{E}}E(1\wedge X\psi^{\prime})$.

Figure 3. The flow network $N$.

We prove that $N$ satisfies ${\mathcal{E}}E(1\wedge X\psi^{\prime})$ iff some
computation in ${\\{p,\neg p\\}}^{*}$ satisfies $\psi$. Assume first that some
computation $\pi$ in ${\\{p,\neg p\\}}^{*}$ satisfies $\psi$. Consider a flow
$f$ in $N$ such that $f(v_{p})=1$ and $f(v_{\neg p})=0$, and consider the path
in $N$ that encodes $\pi$ (starting from the second vertex in the path). For
these flow and path, the formula $X\psi^{\prime}$ holds, and therefore
$N\models{\mathcal{E}}E(1\wedge X\psi^{\prime})$. For the other direction,
assume that $N\models{\mathcal{E}}E(1\wedge X\psi^{\prime})$. Let $f$ and
$\pi$ be the flow function and the path in $N$ that witness the satisfaction
of $X\psi^{\prime}$. The structure of $N$ guarantees that $f(v_{p})+f(v_{\neg
p})=1$. Hence, $\pi$ with $f$ encodes a computation in ${\\{p,\neg p\\}}^{*}$
that satisfies $\psi$, and we are done. Note that we can avoid using edges
with capacities $0$ by changing $\neg\varphi$ to ${\mathcal{E}}E(1\wedge
X0\wedge XX\psi^{\prime})$.

We also note that when the given formula is in BFL, we cannot avoid the need
to guess a flow function, yet once the flow function is guessed, we can verify
it in polynomial time. Accordingly, the model-checking problem for BFL is in
${\rm P}^{\rm NP}$. We discuss this point further below.

In practice, a network is typically much bigger than its specification, and
its size is the computational bottleneck. In temporal-logic model checking,
researchers have analyzed the _system complexity_ of model-checking
algorithms, namely the complexity in terms of the system, assuming the
specification is of a fixed length. There, the system complexity of LTL and
CTL⋆ is NLOGSPACE-complete [LP85, KVW00]. We prove that, unfortunately, this
is not the case of BFL⋆. That is, we prove that while the _network complexity_
of the model-checking problem, namely the complexity in terms of the network,
does not reach PSPACE, it seems to require polynomially many calls to an NP
oracle. Essentially, each evaluation of a flow quantifier requires such a
call. Formally, we have the following.

######  Theorem 8.

The network complexity of BFL⋆ is in $\Delta_{2}^{P}$ (i.e., in ${\rm P}^{\rm
NP}$).

######  Proof 5.3.

Fixing the length of the formula in the algorithm described in the proof of
Theorem 6, we get that $k$ is fixed, and so is the length of each subformula
$\varphi_{i}$. Thus, evaluation of $\varphi_{i}$ involves a guess of a flow
and then model checking of a fixed size Flow-CTL⋆ formula, which can be done
in time polynomial in the size of the network. Hence, the algorithm from
Theorem 6 combined with an NP oracle gives the required network complexity.

While finding the exact network complexity of model checking BFL⋆ and its
fragments is interesting from a complexity-theoretical point of view, it does
not contribute much to our story. Here, we prove NP and co-NP hardness holds
already for very restricted fragments. As good news, in Section 7 we point
that for the conjunctive fragment, model checking can be performed in
polynomial time.222A possible tightening of our analysis is via the complexity
class BH, which is based on a Boolean hierarchy over NP. Essentially, it is
the smallest class that contains NP and is closed under union, intersection,
and complement. The levels of the hierarchy start with BH${}_{1}=$ NP, and
each level adds internal intersections as well as intersection with a co-NP
(even levels) or an NP (odd levels) language [Wec85]. BH is contained in
$\Delta_{2}^{P}$. It is not hard to prove that the network complexity of the
fragment of BFL${}^{\star}_{1}$ that contains at most $k$ flow quantifiers is
in BH${}_{k+1}\cap$ co-BHk+1. Indeed, the latter contain problems that are
decidable in polynomial time with $k$ parallel queries to an NP oracle
[Bei91]. A BHk lower bound can also be shown.

We first show a simple lemma that is needed for the network-complexity
hardness results.

######  Lemma 9.

A CNF formula $\psi$ can be translated to a CNF formula $\psi^{\prime}$ in
polynomial time, such that $\psi$ is satisfiable iff $\psi^{\prime}$ is
satisfiable, and all literals in $\psi^{\prime}$ appear exactly the same
number of times in $\psi^{\prime}$.

######  Proof 5.4.

We consider CNF formulas in which a literal is not allowed to appear more than
once in each clause. Let $|y|_{\psi}$ denote the number of occurrences of the
literal $y$ in $\psi$. Let $x_{1}$ and $x_{2}$ be two variables in $\psi$. We
add some ‘true’ clauses to $\psi$ to obtain $\psi^{\prime}$. First we add
clauses of the form ($x_{1}\vee x_{2}\vee\neg x_{2}$) for $|\neg
x_{1}|_{\psi}-|x_{1}|_{\psi}$ times if $|\neg x_{1}|_{\psi}>|x_{1}|_{\psi}$,
else we add clauses of the form ($\neg x_{1}\vee x_{2}\vee\neg x_{2}$) for
$|x_{1}|_{\psi}-|\neg x_{1}|_{\psi}$ times. Thus we obtain a formula
$\psi_{1}$ with the same number of occurrences for the literals $x_{1}$ and
$\neg x_{1}$.

Now for every variable $x_{i}\neq x_{1}$, we add clauses ($x_{i}\vee
x_{1}\vee\neg x_{1}$) if the number of occurrences of $\neg x_{i}$ in
$\psi_{1}$ is more than that of $x_{i}$, otherwise we add clauses ($\neg
x_{i}\vee x_{1}\vee\neg x_{1}$), possibly multiple times, until the number of
occurrences of $x_{i}$ and the number of occurrences of $\neg x_{i}$ become
the same. Now for each variable $x$, both the literals $x$ and $\neg x$ appear
the same number of times.

As a final step, let $x_{j}$ be a variable such that the number of occurrences
of the literals $x_{j}$ and $\neg x_{j}$ is the maximum over all the
variables. For every variable $x_{i}\neq x_{j}$, we add clauses of the form
($x_{i}\vee\neg x_{i}$) until the number of literals for $x_{i}$ and $x_{j}$
are the same. We call the resultant formula $\psi^{\prime}$.

Note that all the above steps can be done in polynomial time and the size of
$\psi^{\prime}$ is polynomial in the size of $\psi$.

######  Theorem 10.

The network complexity of $\exists$BFL${}^{\star}_{1}$ and
$\forall$BFL${}^{\star}_{1}$ is NP-complete and co-NP-complete, respectively.
Hardness applies already to $\exists$LFL1 and $\forall$LFL1 formulas without
atomic propositions, and to BFL.

######  Proof 5.5.

For the upper bound, it is easy to see that one step in the algorithm
described in the proof of Theorem 6 (that is, evaluating $\varphi_{i}$ once
all its flow state subformulas have been evaluated), when applied to
$\varphi_{i}$ of a fixed length is in NP for $\varphi_{i}$ of the form
${\mathcal{E}}\xi$ and in co-NP for $\varphi_{i}$ of the form
${\mathcal{A}}\xi$.

For the lower bound, we prove NP-hardness for $\exists$LFL1. Co-NP-hardness
for $\forall$LFL1 follows by dualization. We describe a reduction from CNF-
SAT. Let $\theta=C_{1}\wedge\ldots\wedge C_{m}$ be a CNF formula over the
variables $x_{1}\ldots x_{n}$. We assume that every literal in
$x_{1},\ldots,x_{n},\bar{x}_{1},\ldots,\bar{x}_{n}$ appears exactly in $k$
clauses in $\theta$. Indeed, by Lemma 9, every CNF formula can be converted to
such a formula in polynomial time and with a polynomial blowup.

We construct a flow network $N$ and an $\exists$LFL1 formula
${\mathcal{E}}A\psi$ such that $\theta$ is satisfiable iff
$N\models{\mathcal{E}}A\psi$. The network $N$ is constructed as demonstrated
on the right. Let $Z=\\{x_{1},\ldots,x_{n},\bar{x}_{1},\ldots,\bar{x}_{n}\\}$.
For a literal $z\in Z$ and a clause $C_{i}$, the network $N$ contains an edge
$\langle z,C_{i}\rangle$ iff the clause $C_{i}$ contains the literal $z$.
Thus, each vertex in $Z$ has exactly $k$ outgoing edges. The capacity of each
of these edges is $1$. The flow-LTL formula $\psi=kn\wedge XX(k\vee 0)\wedge
XXX(\geq 1)$. We now prove that $\theta$ is satisfiable iff
$N\models{\mathcal{E}}A\psi$.

Assume first that $\theta$ is satisfiable. Consider the flow function $f$
where for every $1\leq i\leq n$, if $x_{i}$ holds in the satisfying
assignment, then $f(x_{i})=k$ and $f(\bar{x}_{i})=0$, and otherwise
$f(x_{i})=0$ and $f(\bar{x}_{i})=k$. For such $f$, all the paths in $N$
satisfy $\psi$.

Assume now that there is a flow function $f$ with which $N$ satisfies $A\psi$.
For every $1\leq i\leq n$, either we have $f(x_{i})=k$ and $f(\bar{x}_{i})=0$
or we have $f(x_{i})=0$ and $f(\bar{x}_{i})=k$. Consider the assignment $\tau$
to the variables $x_{1},\ldots,x_{n}$ induced by $f$, where a literal $z\in Z$
holds in $\tau$ iff the flow in the corresponding vertex is positive. Since
according to $\psi$ for every $i$ the flow in the vertex $C_{i}$ is positive,
then every clause in $\theta$ contains at least one literal whose
corresponding vertex has a positive flow. Hence, the assignment $\tau$
satisfies $\theta$. Finally, note that $\psi$ does not contain atomic
propositions. Also, the same proof holds with the BFL formula $\psi=kn\wedge
AXEXk\wedge AXAXAX(\geq 1)$.

###  5.1. Flow synthesis

In the flow-synthesis problem, we are given a network $N$ and an
$\exists$BFL${}^{\star}_{1}$ formula ${\mathcal{E}}\varphi$, and we have to
return a flow function $f$ with which $\varphi$ is satisfied in $N$, or
declare that no such function exists. The corresponding decision problem,
namely, deciding whether there is a flow function with which $\varphi$ is
satisfied in $N$, is clearly at least as hard as CTL⋆ model checking. Also, by
guessing $f$, its complexity does not go beyond CTL⋆ model-checking
complexity. The network complexity of the problem coincides with that of
$\exists$BFL${}^{\star}_{1}$ model checking. Thus, we have the following.

######  Theorem 11.

The flow-synthesis problem for $\exists$BFL${}^{\star}_{1}$ is PSPACE-
complete, and its network complexity is NP-complete.

##  6\. Model Checking Extensions of BFL⋆

In Section 4, we defined several extensions of BFL⋆. In this section we study
the model-checking complexity for each of the extensions, and show that they
do not require an increase in the complexity. The techniques for handling them
are, however, richer: For positive path quantification, we have to refine the
network and add a path-predicate that specifies positive flow, in a similar
way fairness is handled in temporal logics. For maximal-flow quantification,
we have to augment the model-checking algorithm by calls to a procedure that
finds the maximal flow. For non-integral flow quantification, we have to
reduce the model-checking problem to a solution of a linear-programming
system. For past operators, we have to extend the model-checking procedure for
CTL⋆ with branching past. Finally, for first-order quantification over flow
values, we have to first bound the range of relevant values, and then apply
model checking to all relevant values.

###  6.1. Positive path quantification

Given a network $N$, it is easy to generate a network $N^{\prime}$ in which we
add a vertex in the middle of each edge, and in which the positivity of paths
correspond to positive flow in the new intermediate vertices. Formally,
assuming that we label the new intermediate vertices by an atomic proposition
$\mathit{edge}$, then the BFL⋆ path formula
$\xi_{\mathit{positive}}=G(\mathit{edge}\rightarrow>0)$ characterizes positive
paths, and replacing a state formula $A\psi$ by the formula
$A(\xi_{\mathit{positive}}\rightarrow\psi)$ restricts the range of path
quantification to positive paths. Now, given a BFL⋆ formula $\varphi$, it is
easy to generate a BFL⋆ formula $\varphi^{\prime}$ such that $N\models\varphi$
iff $N^{\prime}\models\varphi^{\prime}$. Indeed, we only have to (recursively)
modify path formulas so that vertices labeled $\mathit{edge}$ are ignored:
$X\xi$ is replaced by $XX\xi$, and $\xi_{1}U\xi_{2}$ is replaced by
$(\xi_{1}\vee\mathit{edge})U(\xi_{2}\wedge\neg\mathit{edge})$. Hence, the
complexity of model-checking is similar to BFL⋆.

###  6.2. Maximal flow quantification

The maximal flow $\gamma_{\mathit{max}}$ in a flow network can be found in
polynomial time. Our model-checking algorithm for BFL⋆ described in the proof
of Theorem 6 handles each flow state subformula ${\mathcal{E}}\varphi$ by
guessing a flow function $f:E\rightarrow{\rm I}\\!{\rm N}$ with which the
Flow-CTL⋆ formula $\varphi$ holds. For an ${\mathcal{E}}^{\mathit{max}}$
quantifier, we can guess only flow functions for which the flow leaving the
source vertex is $\gamma_{\mathit{max}}$. In addition, after calculating the
maximal flow, we can substitute $\gamma_{\mathit{max}}$, in formulas that
refer to it, by its value. Hence, the complexity of model-checking is similar
to that of BFL⋆.

###  6.3. Non-integral flow quantification

Recall that our BFL⋆ model-checking algorithm handles each flow state
subformula ${\mathcal{E}}\varphi$ by guessing a flow function
$f:E\rightarrow{\rm I}\\!{\rm N}$ with which the Flow-CTL⋆ formula holds.
Moving to non-integral flow functions, the guessed function $f$ should be
$f:E\rightarrow{\rm I}\\!{\rm R}$, where we cannot bound the size or range of
guesses.

Accordingly, in the non-integral case, we guess, for every vertex $v\in V$, an
assignment to the flow propositions that appear in $\varphi$. Then, we perform
two checks. First, that $\varphi$ is satisfied with the guessed assignment —
this is done by CTL⋆ model checking, as in the case of integral flows. Second,
that there is a non-integral flow function that satisfies the flow constraints
that appear in the vertices. This can be done in polynomial time by solving a
system of linear inequalities [Sch03]. Thus, as in the integral case, handling
each flow state formula ${\mathcal{E}}\varphi$ can be done in PSPACE, and so
is the complexity of the entire algorithm.

###  6.4. Past operators

Recall that our algorithm reduces BFL⋆ model checking to a sequence of calls
to a CTL⋆ model-checking procedure. Starting with a BFL⋆ formula with past
operators, the required calls are to a model-checking procedure for CTL⋆ with
past. By [KPV12], model checking CTL⋆ with branching past is PSPACE-complete,
and thus so is the complexity of our algorithm.

###  6.5. First-Order quantification on flow values

For a flow network

$N=\langle AP,V,E,c,\rho,s,T\rangle,$

let $C_{N}=1+\Sigma_{e\in E}c(e)$. Thus, for every flow function $f$ for $N$
and for every vertex $v\in V$, we have $f(v)<C_{N}$. We claim that when we
reason about BFL⋆ formulas with quantified flow values, we can restrict
attention to values in $\\{0,1,\ldots,C_{N}\\}$.

######  Lemma 12.

Let $N$ be a flow network and let $\theta=\forall x_{1}\varphi$ be a
BFL${}^{\star}(\\{+,*\\})$ formula over the variables
$X=\\{x_{1},\ldots,x_{n}\\}$, and without free variables. Then,
$N\models\theta$ iff $N\models\varphi[x_{1}\leftarrow\gamma]$, for every
$0\leq\gamma\leq C_{N}$.

######  Proof 6.1.

We show that for every $\gamma>C_{N}$ we have
$N\models\varphi[x_{1}\leftarrow\gamma]$ iff $N\models\varphi[x_{1}\leftarrow
C_{N}]$. Every expression $g(X)$ in $\varphi$ is obtained from the variables
in $X$ by applying the operators $+,*$, and possibly by using constants in
${\rm I}\\!{\rm N}$. Hence, every such $g$ is monotonically increasing for
every variable $x_{i}$. Let $\gamma_{2},\ldots,\gamma_{n}$ be an assignment
for the variables $x_{2},\ldots,x_{n}$, respectively. Let
$g_{1}(x_{1})=g(x_{1},\gamma_{2},\ldots,\gamma_{n})$. Let $\gamma_{1}$ be an
integer bigger than $C_{N}$. Since $g_{1}$ is monotonically increasing, we
have $g_{1}(C_{N})\leq g_{1}(\gamma_{1})$. If
$g_{1}(C_{N})<g_{1}(\gamma_{1})$, then $g_{1}$ is not a constant function, and
since it contains only the operators $+,*$ and constants in ${\rm I}\\!{\rm
N}$, we have $g_{1}(C_{N})\geq C_{N}$. Therefore, if $g_{1}(C_{N})\neq
g_{1}(\gamma_{1})$, then $g_{1}(\gamma_{1})>g_{1}(C_{N})\geq C_{N}$. Recall
that for every flow function $f$ in $N$ and for every vertex $v\in V$, we have
$f(v)<C_{N}$. Therefore, every state subformula $>g_{1}(x_{1})$ and every
state subformula $\geq g_{1}(x_{1})$ holds for $\gamma_{1}$ iff it holds for
$C_{N}$. Therefore, $N\models\varphi[x_{1}\leftarrow\gamma]$ iff
$N\models\varphi[x_{1}\leftarrow C_{N}]$. Hence, we have $N\models\forall
x_{1}\varphi$ iff $N\models\varphi[x_{1}\leftarrow\gamma]$ for every
$0\leq\gamma\leq C_{N}$.

By Lemma 12, the model-checking problem for BFL${}^{\star}(\\{+,*\\})$ is
PSPACE-complete.

##  7\. A Polynomial Fragment

The upper bounds to the complexity of the model-checking problem that are
given in Sections 5 and 6 refer to worst-case complexity. As has been the case
of CTL⋆, in practice the complexity is often lower. In particular, there are
fragments of CTL⋆, and hence also BFL⋆ and its extensions for which we can
show that the described model-checking algorithms perform better, say by
showing that the particular syntax guarantees a bound on the size of the
automata associated with path formulas. In this section we show that the
model-checking problem for CBFL⋆ (see Section 4.6) can be solved in polynomial
time. The result is not based on a tighter complexity analysis for the case
the specification is in CBFL⋆ but rather on a different model-checking
algorithm for this logic.

Our model-checking algorithm reduces the evaluation of a CBFL⋆ formula into a
sequence of solutions to the _vertex-constrained flow problem_. In this
problem, we are given a flow network $N=\langle AP,V,E,c,\rho,s,T\rangle$ in
which each vertex $v\in V$ is attributed by a range
$[\gamma_{l},\gamma_{u}]\in{\rm I}\\!{\rm N}\times({\rm I}\\!{\rm
N}\cup\\{\infty\\})$. The problem is to decide whether there is a flow
function $f:E\rightarrow{\rm I}\\!{\rm R}$ such that for all vertices $v\in
V$, we have $\gamma_{l}\leq f(v)\leq\gamma_{u}$.

######  Lemma 13.

The vertex-constrained flow problem can be solved in polynomial time. If there
is a solution that is a non-integral flow function, then there is also a
solution that is an integral flow function, and the algorithm returns such a
solution.

######  Proof 7.1.

Given $N$, we construct a new flow network $N^{\prime}$ in which the
attributions are on the edges. Thus, $N^{\prime}$ is a flow network with lower
bounds on the flow. We construct $N^{\prime}$ by splitting every vertex $v\in
V$ with attribution $[\gamma_{l},\gamma_{u}]$ into two vertices in
$N^{\prime}$: $v_{in}$ and $v_{out}$. The vertices are connected by an edge
$\langle v_{in},v_{out}\rangle$ with attribution $[\gamma_{l},\gamma_{u}]$.
For every edge $\langle u,v\rangle\in E$, we add to $N^{\prime}$ an edge
$\langle u_{out},v_{in}\rangle$ with attribution $[0,c(\langle u,v\rangle)]$.
It is well known that deciding whether there exists a feasible flow and
finding such a flow in a flow network with lower bounds can be done in
polynomial time (see, for example, Chapter 6.7 in [AMO93]). Also, the
algorithm for finding such a feasible flow reduces the problem to a maximum-
flow problem. Accordingly, if there is a feasible flow then the algorithm
returns an integral one.

######  Theorem 14.

CBFL⋆ model checking can be solved in polynomial time.

######  Proof 7.2.

Let $N=\langle AP,V,E,c,\rho,s,T\rangle$, and consider a CBFL⋆ formula
$\varphi$. If $\varphi$ is in CBFL${}^{\star}_{0}$, we can clearly label in
linear time all the vertices in $N$ by a fresh atomic proposition
$p_{\varphi}$ that maintains the satisfaction of $\varphi$. That is, in all
vertices $v\in V$, we have that $p_{\varphi}\in\rho(v)$ iff $v\models\varphi$.
Otherwise, $\varphi$ is a CBFL${}^{\star}_{i+1}$ formula for some $i\geq 0$.
We show how, assuming that the vertices of $N$ are labeled by atomic
propositions that maintain satisfaction of the subformulas of $\varphi$ that
are CBFL${}^{\star}_{i}$ formulas, we can label them, in polynomial time, by a
fresh atomic proposition that maintains the satisfaction of $\varphi$.

Recall that $\varphi$ is a Boolean assertion over CBFL${}^{\star}_{i}$
formulas and flow formulas of the form
${\mathcal{E}}(A\psi_{1}\wedge\cdots\wedge A\psi_{n})$, where each $\psi_{j}$
is of the form $X^{k_{j}}\xi_{j}$ or $X^{k_{j}}G\xi_{j}$, where $k_{j}\geq 0$
and $\xi_{j}$ is a CBFL${}^{\star}_{i}$ formula or a flow proposition (that
is, $>\gamma$, $<\gamma$, $\geq\gamma$, or $\leq\gamma$, for an integer
$\gamma\in{\rm I}\\!{\rm N}$).

Since CBFL${}^{\star}_{i}$ subformulas have already been evaluated, we
describe how to evaluate subformulas of the form
$\theta={\mathcal{E}}(A\psi_{1}\wedge\cdots\wedge A\psi_{n})$. Intuitively,
since the formulas in $\theta$ include no disjunctions, they impose
constraints on the vertices of $N$ in a deterministic manner. These
constraints can be checked in polynomial time by solving a vertex-constrained
flow problem. Recall that for each $1\leq j\leq n$, the formula $\psi_{j}$ is
of the form $X^{k_{j}}\xi_{j}$ or $X^{k_{j}}G\xi_{j}$, for some $k_{j}\geq 0$,
and a CBFL${}^{\star}_{i}$ formula or a flow proposition $\xi_{j}$. In order
to evaluate $\theta$ in a vertex $v\in V$, we proceed as follows. For each
$1\leq j\leq n$, the formula $\xi_{j}$ imposes either a Boolean constraint (in
case $\xi_{j}$ is a CBFL${}^{\star}_{i}$ formula) or a flow constraint (in
case $\xi_{j}$ is a flow proposition) on a finite subset $V^{v}_{j}$ of $V$.
Indeed, if $\psi_{j}=X^{k_{j}}\xi_{j}$, then $V^{v}_{j}$ includes all the
vertices reachable from $v$ by a path of length $k_{j}$, and if
$\psi_{j}=X^{k_{j}}G\xi_{j}$, then $V^{v}_{j}$ includes all the vertices
reachable from $v$ by a path of length at least $k_{j}$. We attribute each
vertex by the constraints imposed on it by all the conjuncts in $\theta$. If
one of the Boolean constrains does not hold, then $\theta$ does not hold in
$v$. Otherwise, we obtain a set of flow constraints for each vertex in $V$.
For example, if $\theta={\mathcal{E}}(AXXp\wedge AXX>5\wedge AG\leq 8)$, then
in order to check whether $\theta$ holds in $s$, we assign the flow constraint
$\leq 8$ to all the vertices reachable from $s$, and assign the flow
constraint $>5$ to all the successors of the successors of $s$. If one of
these successors of successors does not satisfy $p$, we can skip the check for
a flow and conclude that $s$ does not satisfy $\theta$. Otherwise, we search
for such a flow, as described below.

The flow constrains for a vertex induce a closed, open, or half-closed range.
The upper bound in the range may be infinity. For example, the constrains
$>6$, $<10$, $\leq 8$ induce the half-closed range $(6,8]$. Note that it may
be that the induced range is empty. For example, the constraints $\leq 6$ and
$>8$ induce an empty range. Then, $\theta$ does not hold in $v$. Since we are
interested in integral flows, we can convert all strict bounds to non-strict
ones. For example, the range $(6,8]$ can be converted to $[7,8]$. Note that
since we are interested in integral flow, a non-empty open range may not be
satisfiable, and we refer to it as an empty range. For example, the range
$(6,7)$ is empty. Hence, the satisfaction of $\theta$ in $v$ is reduced to an
instance of the vertex-constrained flow problem. By Lemma 13, deciding whether
there is a flow function that satisfies the constraints can be solved in
polynomial time.

######  Remark 15.

Note that the same algorithm can be applied when we consider non-integral flow
functions, namely in CBFL⋆ with the ${\mathcal{A}}^{{\rm I}\\!{\rm R}}$ flow
quantifier. There, the induced vertex-constrained flow problem may include
open boundaries. The solution need not be integral, but can be found in
polynomial time by solving a system of inequalities [Sch03].

##  8\. Query Checking

As discussed in Section 1, query checking is a useful methodology for system
exploration. A query is a specification with the place-holder “$?$”, and the
goal is to find replacements to $?$ with which the specification holds. In
this section we extend the methodology to BFL⋆. We first need some
definitions.

A _propositional BFL ⋆ query_ (propositional query, for short) is a BFL⋆
formula in which a single state formula is “$?$”. For a propositional query
$\psi$ and a propositional assertion $\theta$ over $AP$, we denote by
$\psi[?\leftarrow\theta]$ the formula obtained from $\psi$ by replacing $?$ by
$\theta$. Given a network $N$ and a query $\psi$, a _solution_ to $\psi$ in
$N$ is a propositional assertion $\theta$ over $AP$ such that
$N\models\psi[?\leftarrow\theta]$. For example, the propositional query
${\mathcal{E}}E((?\wedge\geq 5)U\mathit{target})$ asks which propositional
assertions $\theta$ are such that the network satisfies
${\mathcal{E}}E((\theta\wedge\geq 5)U\mathit{target})$, namely propositional
assertions $\theta$ such that there is a flow and there is a path to the
target in which all vertices satisfy $\theta$ and the flow in them is at least
$5$. Note that we do not allow the solution $\theta$ to include flow
propositions. Note also that only a single occurrence of $?$ is allowed in the
query. Richer settings in CTL⋆ query checking allow queries with several place
holders, namely $?_{1},?_{2},\ldots,?_{m}$, possibly with multiple appearances
to each of them [GC02]. The focus on queries with a single $?$ enables the
query checker to refer to the _polarity_ of queries. Formally, we say that a
propositional query $\psi$ is positive (_negative_) if the single $?$ in it is
in the scope of an even (respectively, odd) number of negations. The polarity
of queries implies monotonicity, in the following sense (the proof proceeds by
an easy induction on the structure of the query).

######  Lemma 16.

Consider a positive (negative) BFL⋆ query $\psi$. Let $\theta$ and
$\theta^{\prime}$ be propositional formulas such that $\theta$ implies
$\theta^{\prime}$ ($\theta^{\prime}$ implies $\theta$, respectively). Then,
$\psi[?\leftarrow\theta]$ implies $\psi[?\leftarrow\theta^{\prime}]$.

######  Corollary 17.

Consider a network $N$. Let $\psi$ be a positive (negative) BFL⋆ query, let
$\theta$ be a solution for $\psi$ in $N$, and let $\theta^{\prime}$ be a
propositional formula such that $\theta$ implies $\theta^{\prime}$
($\theta^{\prime}$ implies $\theta$, respectively). Then, $\theta^{\prime}$ is
a solution for $\psi$ in $N$.

It is not hard to see that a propositional BFL⋆ query may have multiple
solutions. Corollary 17 enables us to partially order them. Then, given a
query $\psi$, we say that a solution $\theta$ is _strongest_ if there is no
solution $\theta^{\prime}$ such that $\theta^{\prime}$ is not equivalent to
$\theta$ and either $\psi$ is positive, in which case $\theta^{\prime}$
implies $\theta$, or $\psi$ is negative, in which case $\theta$ implies
$\theta^{\prime}$. A query, however, may not only have multiple solutions, but
may also have multiple strongest solutions. Accordingly, as is the case with
CTL⋆, a search for all strongest solutions has to examine all possible
solutions [BG01]. Consider a network $N$ and a propositional BFL⋆ query
$\psi$. Each solution to $\psi$ in $N$ corresponds to an assignment to all
subsets of atomic propositions, thus there are $2^{2^{|AP|}}$ assertions to
check. For each we need to model check the formula $\psi[?\leftarrow\theta]$,
for an assertion $\theta$. Accordingly, the length of
$\psi[?\leftarrow\theta]$ is $O(|\psi|+2^{|AP|})$. Thus, finding all strongest
solutions to a propositional query is a very complex task, involving
$2^{2^{|AP|}}$ executions of the algorithm described in Theorem 6 for a
formula of length $O(|\psi|+2^{|AP|})$.

Fortunately, in the context of BFL⋆, we are able to point to a class of
interesting queries for which query checking is not more complex than model
checking: queries in which the place holder is the value in a flow
proposition. Formally, a _value BFL ⋆ query_ (value query, for short) is a
BFL⋆ formula in which a single flow proposition is of the form $>?$, $\geq?$,
$<?$, or $\leq?$. Each value query $\psi$ is either a _lower-bound query_ , in
case $\psi$ is positive iff the flow proposition with $?$ is $>?$ or $\geq?$
(that is, either $\psi$ is positive and the flow proposition with $?$ is $>?$
or $\geq?$, or $\psi$ is negative and the flow proposition with $?$ is $<?$ or
$\leq?$), or an _upper-bound query_ , in case $\psi$ is positive iff the flow
proposition with $?$ is $<?$ or $\leq?$. For a value query $\psi$ and an
integer $\gamma\in{\rm I}\\!{\rm N}$, we denote by $\psi[?\leftarrow\gamma]$
the BFL⋆ formula obtained from $\psi$ by replacing $?$ by $\gamma$. Given a
network $N$ and a value query $\psi$, a _solution_ to $\psi$ in $N$ is an
integer $\gamma\in{\rm I}\\!{\rm N}$ such that
$N\models\psi[?\leftarrow\gamma]$. For example, the value query
${\mathcal{E}}EF(\mathit{target}\wedge(\geq?))$ asks which values of flow can
reach a target vertex.

For a value query $\psi$, we say that a solution $\gamma$ to $\psi$ in $N$ is
_strongest_ if $\psi$ is a lower-bound query and there is no solution
$\gamma^{\prime}$ to $\psi$ in $N$ such that $\gamma^{\prime}>\gamma$, or
$\psi$ is an upper-bound query and there is no solution $\gamma^{\prime}$ to
$\psi$ in $N$ such that $\gamma^{\prime}<\gamma$. Since a strongest solution
in a value query is either a maximum or a minimum of a set in ${\rm I}\\!{\rm
N}$, there is at most one strongest solution.333Note that if we allow
solutions in ${\rm I}\\!{\rm R}$, then flow propositions with strict
inequality do not have unique strongest solutions. In the case of solutions in
${\rm I}\\!{\rm N}$, however, the flow propositions $<\gamma$ and $>\gamma$
are equivalent to $\leq\gamma-1$ and $\geq\gamma+1$, respectively. Hence the
following lemma.

######  Lemma 18.

Consider a network $N$. Let $\gamma$ be the strongest solution for a value
BFL⋆ query $\psi$. If $\psi$ is a lower-bound query, then the set of solutions
is ${\rm I}\\!{\rm N}\cap[\gamma,\infty)$. If $\psi$ is an upper-bound query
then the set of solutions is ${\rm I}\\!{\rm N}\cap[0,\gamma]$.

######  Remark 19.

Note that in our definition of a value query, we do not allow a flow
proposition of the form $=?$. Indeed, such a flow proposition encodes a
conjunction of two flow propositions of different polarities. If we decide to
allow such value queries then the set of solutions does not satisfy a property
as in Lemma 18. For example, the set of solutions for the query
${\mathcal{E}}[(=?)\wedge((\geq 2\,\wedge\leq 4)\vee(\geq 6\,\wedge\leq 9))]$
and a network with a maximal flow of $9$, is $\\{2,3,4,6,7,8,9\\}$.

Thus, unlike the case of propositional queries, in the case of value queries
we can talk about the strongest solution, and study the complexity of finding
it. The lower bound in the following theorem corresponds to the problem of
deciding whether there is a solution to a given value BFL⋆ query.

######  Theorem 20.

The problem of finding the strongest solution to a value BFL⋆ query is PSPACE-
complete. Furthermore, the network complexity is in $\Delta_{2}^{P}$.

######  Proof 8.1.

Model checking of a BFL⋆ formula $\psi$ can be reduced to deciding whether
there is a solution for the value query $\psi\wedge({\mathcal{A}}\leq?)$.
Hence the PSPACE-hardness.

Lemma 18 implies that in order to find the strongest solution for a value
query $\psi$, we can run a binary search on the values, and for each value
$\gamma$ to check whether $\psi[?\leftarrow\gamma]$ holds using BFL⋆ model-
checking. Thus, the number of calls to the BFL⋆ model checker is logarithmic
in $\sum_{e\in E}c(e)$, and hence polynomial in $|N|$. The PSPACE upper bound
then follows from the PSPACE upper bound for BFL⋆ model checking. The
$\Delta_{2}^{P}$ upper bound for the network complexity follows from the
$\Delta_{2}^{P}$ upper bound for the network complexity of BFL⋆ model
checking.

##  9\. Discussion

We introduced the flow logic BFL⋆ and studied its theoretical and practical
aspects, as well as extensions and fragments of it. Below we discuss possible
directions for future research.

At the more theoretical front, an important aspect that we left open in this
work is the _expressive power_ of the different extensions and fragment of
BFL⋆. As discussed in Remark 5, some cases follow easily from known
expressiveness results for CTL⋆, yet the full picture is open. Also, as has
been the case in traditional temporal logics, questions of _succinctness_ are
of interest too.

Another natural problem regarding BFL⋆ is the _satisfiability_ problem. That
is, given a BFL⋆ formula, decide whether there is a flow network that
satisfies it. In Section 3.2, we showed that, unlike CTL⋆, the logic BFL⋆ is
sensitive to unwinding. Thus, the standard algorithm for the satisfiability
problem of CTL⋆, which is based on checking emptiness of tree automata, is not
useful in the case of BFL⋆. Moreover, the satisfiability problem is
challenging already to the linear fragment LFL of BFL⋆. Indeed, as discussed
in Section 4.6, the semantics of LFL mixes linear and branching semantics, and
there is no simple reduction of the satisfiability problem for LFL into the
emptiness of word automata.

In the algorithmic side, the relation between maximum flows and minimum cuts
has been significant in the context of the traditional maximum-flow problem.
It would be interesting to study the relation between cuts and BFL⋆. In
particular, the notion of cuts that satisfy some structural property that can
be expressed with BFL⋆ seems interesting.

Finally, many problems in various domains are solved using a reduction to the
maximum-flow problem [CLR90, AMO93]. Flow logics allow reasoning about
properties of flow networks that go beyond their maximal flow. An interesting
direction for future research is to study applications of flow logics for rich
variants of such problems. For example, using flow logics we can solve
variants of matching or scheduling problems that involve restrictions on the
allowed matches or variants of schedules.

## References

  * [AH94] R. Alur and T.A. Henzinger.  A really temporal logic.  Journal of the ACM, 41(1):181–204, 1994.
  * [AHK02] R. Alur, T.A. Henzinger, and O. Kupferman.  Alternating-time temporal logic.  Journal of the ACM, 49(5):672–713, 2002.
  * [AMO93] R.K. Ahuja, T.L. Magnanti, and J.B. Orlin.  Network flows: Theory, algorithms, and applications.  Prentice Hall Englewood Cliffs, 1993.
  * [BDVV18] R. Birkner, D. Drachsler-Cohen, L. Vanbever, and M.T. Vechev.  Net2Text: Query-guided summarization of network forwarding behaviors.  In 15th USENIX Symposium on Networked Systems Design and Implementation, pages 609–623, 2018.
  * [Bei91] R. Beigel.  Bounded queries to sat and the boolean hierarchy.  Theoretical Computer Science, 84(2):199–223, 1991.
  * [BG01] G. Bruns and P. Godefroid.  Temporal logic query checking.  In Proc. 16th IEEE Symp. on Logic in Computer Science, pages 409–420. IEEE Computer Society, 2001.
  * [CE81] E.M. Clarke and E.A. Emerson.  Design and synthesis of synchronization skeletons using branching time temporal logic.  In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer, 1981.
  * [CG03] M. Chechik and A. Gurfinkel.  TLQSolver: A temporal logic query checker.  In Proc. 15th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science, pages 210–214. Springer, 2003.
  * [CGG07] M. Chechik, M. Gheorghiu, and A. Gurfinkel.  Finding state solutions to temporal queries.  In Proc. Integrated Formal Methods, pages 273–292, 2007.
  * [CGP99] E.M. Clarke, O. Grumberg, and D. Peled.  Model Checking.  MIT Press, 1999.
  * [Cha00] W. Chan.  Temporal-logic queries.  In Proc. 12th Int. Conf. on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 450–463. Springer, 2000\.
  * [CHP07] K. Chatterjee, T. A. Henzinger, and N. Piterman.  Strategy logic.  In Proc. 18th Int. Conf. on Concurrency Theory, pages 59–73, 2007\.
  * [CHVB18] E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem.  Handbook of model checking.  Springer, 2018.
  * [CLR90] T.H. Cormen, C.E. Leiserson, and R.L. Rivest.  Introduction to Algorithms.  MIT Press and McGraw-Hill, 1990.
  * [CVP+12] M. Canini, D. Venzano, P. Perešíni, D. Kostić, and J. Rexford.  A nice way to test openflow applications.  In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 127–140, 2012.
  * [Din70] E.A. Dinic.  Algorithm for solution of a problem of maximum flow in a network with power estimation.  Soviet Math. Doll, 11(5):1277–1280, 1970.  English translation by RF. Rinehart.
  * [EIS76] S. Even, A. Itai, and A. Shamir.  On the complexity of timetable and multicommodity flow problems.  SIAM Journal on Computing, 5(4):691–703, 1976.
  * [EK72] J. Edmonds and R.M. Karp.  Theoretical improvements in algorithmic efficiency for network flow problems.  Journal of the ACM, 19(2):248–264, 1972.
  * [EL87] E.A. Emerson and C.-L. Lei.  Modalities for model checking: Branching time logic strikes back.  Science of Computer Programming, 8:275–306, 1987.
  * [FF56] L.R. Ford and D.R. Fulkerson.  Maximal flow through a network.  Canadian journal of Mathematics, 8(3):399–404, 1956.
  * [FF62] L.R. Ford and D.R. Fulkerson.  Flows in networks.  Princeton Univ. Press, Princeton, 1962.
  * [FKL10] D. Fisman, O. Kupferman, and Y. Lustig.  Rational synthesis.  In Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 190–204. Springer, 2010.
  * [GC02] A. Gurfinkel and M. Chechik.  Temporal logic query checking through multi-valued model checking.  Technical report, CSRG Technical Report 457, University of Toronto, Department of Computer Science, 2002.
  * [GCSR13] D. Granata, R. Cerulli, M.G. Scutellá, and A. Raiconi.  Maximum flow problems and an NP-complete variant on edge-labeled graphs.  In Handbook of Combinatorial Optimization, pages 1913–1948. Springer, 2013.
  * [GRN12] M. Gueffaz, S. Rampacek, and C. Nicolle.  Temporal logic to query semantic graphs using the model checking method.  Journal of Software, 7(7), 2012.
  * [GT88] A.V. Goldberg and R.E. Tarjan.  A new approach to the maximum-flow problem.  Journal of the ACM, 35(4):921–940, 1988.
  * [GTT89] A.V. Goldberg, É. Tardos, and R.E. Tarjan.  Network flow algorithms.  Technical report, DTIC Document, 1989.
  * [HM90] J.Y. Halpern and Y. Moses.  Knowledge and common knowledge in a distributed environment.  Journal of the ACM, 37(3):549–587, 1990.
  * [KCZ+13] P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte.  Real time network policy checking using header space analysis.  In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 99–111, 2013.
  * [KPC+12] M. Kuzniar, P. Peresini, M. Canini, D. Venzano, and D. Kostic.  A soft way for openflow switch interoperability testing.  In Proceedings of the 8th international conference on Emerging networking experiments and technologies, pages 265–276. ACM, 2012.
  * [KPV12] O. Kupferman, A. Pnueli, and M.Y. Vardi.  Once and forall.  Journal of Computer and Systems Science, 78(3):981–996, 2012.
  * [KT14] O. Kupferman and T. Tamir.  Properties and utilization of capacitated automata.  In Proc. 34th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 29 of LIPIcs, pages 33–44. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2014.
  * [KVM12] P. Kazemian, G. Varghese, and N. McKeown.  Header space analysis: Static checking for networks.  In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 113–126, 2012.
  * [KVW00] O. Kupferman, M.Y. Vardi, and P. Wolper.  An automata-theoretic approach to branching-time model checking.  Journal of the ACM, 47(2):312–360, 2000.
  * [KZZ+13] A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P.B. Godfrey.  Veriflow: verifying network-wide invariants in real time.  In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 15–27, 2013.
  * [LBG+15] N.P. Lopes, N. Bjørner, P. Godefroid, K. Jayaraman, and G. Varghese.  Checking beliefs in dynamic networks.  In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 499–512, 2015.
  * [LCG+06] B.T. Loo, T. Condie, M. Garofalakis, D.E. Gay, J.M. Hellerstein, P. Maniatis, R. Ramakrishnan, T. Roscoe, and I. Stoica.  Declarative networking: language, execution and optimization.  In Proceedings of the 2006 ACM SIGMOD international conference on Management of data, pages 97–108. ACM, 2006.
  * [LP85] O. Lichtenstein and A. Pnueli.  Checking that finite state concurrent programs satisfy their linear specification.  In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 97–107, 1985.
  * [Mad16] A. Madry.  Computing maximum flow with augmenting electrical flows.  In Foundations of Computer Science (FOCS), 2016 IEEE 57th Annual Symposium on, pages 593–602. IEEE, 2016.
  * [Mil71] R. Milner.  An algebraic definition of simulation between programs.  In Proc. 2nd Int. Joint Conf. on Artificial Intelligence, pages 481–489. British Computer Society, 1971.
  * [QS82] J.P. Queille and J. Sifakis.  Specification and verification of concurrent systems in Cesar.  In Proc. 9th ACM Symp. on Principles of Programming Languages, volume 137 of Lecture Notes in Computer Science, pages 337–351. Springer, 1982.
  * [RCM+14] M. Räim, C. Di Ciccio, F.M. Maggi, M. Mecella, and J. Mendling.  Log-based understanding of business processes through temporal logic query checking.  In OTM Confederated International Conferences” On the Move to Meaningful Internet Systems”, pages 75–92. Springer, 2014.
  * [SC85] A.P. Sistla and E.M. Clarke.  The complexity of propositional linear temporal logic.  Journal of the ACM, 32:733–749, 1985.
  * [Sch66] B.L. Schwartz.  Possible winners in partially completed tournaments.  SIAM Review, 8(3):302–308, 1966.
  * [Sch03] A. Schrijver.  Combinatorial Optimization.  Springer, 2003.
  * [SV03] M. Samer and H. Veith.  Validity of ctl queries revisited.  In Proc. 12th Annual Conf. of the European Association for Computer Science Logic, volume 2803, pages 470–483. Springer, 2003.
  * [Tar85] É. Tardos.  A strongly polynomial minimum cost circulation algorithm.  Combinatorica, 5(3):247–255, 1985.
  * [VAP+16] Y. Velner, K. Alpernas, A. Panda, A. Rabinovich, M. Sagiv, S. Shenker, and S. Shoham.  Some complexity results for stateful network verification.  In Proc. 23rd Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 811–830. Springer, 2016.
  * [WBLS09] A. Wang, P. Basu, B.T. Loo, and O. Sokolsky.  Declarative network verification.  In International Symposium on Practical Aspects of Declarative Languages, pages 61–75. Springer, 2009.
  * [Wec85] G. Wechsung.  On the boolean closure of np.  In Proceedings of the International Conference on Fundamentals of Computation Theory, volume 199 of Lecture Notes in Computer Science, pages 485–493. Springer, 1985.
  * [ZST+10] W. Zhou, M. Sherr, T. Tao, X. Li, B.T. Loo, and Y. Mao.  Efficient querying and maintenance of network provenance at internet-scale.  In Proceedings of the 2010 ACM SIGMOD International Conference on Management of data, pages 615–626. ACM, 2010.