We consider the problem of computing minimum and maximum probabilities of satisfying an $\omega$-regular property in a bounded-parameter Markov decision process (BMDP).
BMDP arise from Markov decision processes (MDP) by allowing for uncertainty on the transition probabilities in the form of intervals where the actual probabilities are unknown.
$\omega$-regular languages form a large class of properties, expressible as, e.g., Rabin or parity automata, encompassing rich specifications such as linear temporal logic.
In a BMDP the probability to satisfy the property depends on the unknown transitions probabilities as well as on the policy.
In this paper, we compute the extreme values.
This solves the problem specifically suggested by Dutreix and Coogan in CDC 2018, extending their results on interval Markov chains with no adversary.
The main idea is to reinterpret their work as analysis of interval MDP and accordingly the BMDP problem as analysis of an $\omega$-regular stochastic game, where a solution is provided.
This method extends smoothly further to bounded-parameter stochastic games.

§ INTRODUCTION

Markov decision processes (MDP) are a classical formalism encompassing both probabilistic and non-deterministic features: in each state some actions are enabled and each action is assigned a distribution over the successor states.
In other words, each action corresponds to a set of transitions, each of which is assigned a transition probability.
Bounded-parameter MDP (BMDP) [18] are like MDP, but to each transition is instead assigned an interval of possible transition probabilities.
Thus each BMDP specifies a set of MDP.
There are two interpretations of these intervals.
Firstly, in the uncertain interpretation, the BMDP specifies MDP with unknown but constant transition probabilities in the intervals.
An MDP is thus derived from the BMDP by picking a value in each interval once for all.
Secondly, in the adversarial interpretation, the BMDP specifies a decision process where the transition probabilities may be different numbers (in the intervals) every time we come to a state.
Each interpretation found its use.
The former can model, for instance, various degrees of uncertainty for each action or confidence intervals for the transition probabilities learnt from experience.
In this case there is one true transition probability, however unknown.
The latter can be used as a formalism for abstracting MDP: states with different outgoing transition probabilities can be abstracted into a single state with an interval covering all the values [18].
In this case, the interval can stand for any of the values whenever visiting the state.
As such BMDP extend interval Markov chains (IMC) [23, 26] by an adversary (or an underspecified/non-deterministic controller).
The uncertain interpretation of IMC then yields uncertain Markov chains (UMC), while the adversarial interpretation of IMC yields interval MDP (IMDP), as distinguished in [37].

$\omega$-regular languages, e.g. [40], form a robust class of rich specifications, which can be represented in various ways, e.g., by formulae of monadic second-order logic or by automata over infinite words.
In the setting of probabilistic systems, it is often advantageous to use deterministic Rabin automata (DRA) or their variations.
In particular, this class encompasses properties expressible in linear temporal logic (LTL) [31] and there are efficient ways of translating LTL to DRA [27].
Control of MDP with LTL specifications is widely studied, e.g. [39, 25, 44, 34, 46], and typically uses the DRA representation.

In [15], Dutreix and Coogan argue for computing minimum and maximum probabilities of satisfying an $\omega$-regular property in an IMC interpreted as IMDP.

In future work, they wish to apply the technique to solve the problem for BMDP, the controllable counterpart of IMC.
In this paper, we re-interpret their technique in a different light and using that perspective give a solution to BMDP, in both the uncertain and the adversarial understanding of the intervals.
We consider both the upper bound (also called design choice of values in intervals [15]) and the lower bound (
antagonistic in [15]).
We present the results for controllers that try to maximize the probability to satisfy the $\omega$-regular property; minimization is analogous as $\omega$-regular languages are closed under complement.

The main idea of our approach is to not only view the IMC as an IMDP, but also as an MDP, since an IMDP is a special case of MDP where the adversary chooses the transition probabilities.
We show the standard analysis on the respective MDP coincides with the tailored algorithm of [15] applied to the IMC.
Our main contribution is taking this perspective on BMDP, yielding a stochastic game.
Since we can solve the stochastic game with an $\omega$-regular objective we can obtain also the solutions.
Moreover, for the upper bound, the two players play cooperatively and we can solve the problem in polynomial time using adapted MDP techniques.
Finally, we show how the game extension of IMC with two competing agents can be solved analogously to BMDP, this time without the need of introducing an additional agent.

*Further related work
The general model of MDP with imprecise parameters (MDPIP) was introduced in [36].
BMDP [18] are then a subclass where the parametrization is limited to independent intervals.
BMDP have been investigated with respect to various objectives, such as stochastic shortest path (minimum expected reward) [4], expected total reward [30, 45, 20], discounted reward [30, 17], LTL [43], PCTL [32, 21], or mean payoff

The special non-controlled case of IMC has also been investigated for various objectives, e.g. PCTL [37, 5], LTL [3] ([2] observes this algorithm may not converge to the optimum) or $\omega$-regular properties [9].

Recent improvements include importance sampling techniques for IMC [22] or topological policy iteration for BMDP [35].
IMC and BMDP are used as abstractions of systems in [29].

*Organization of the paper
After recalling the used formalisms in <ref>, we state our problem in <ref>.
We provide the solution in <ref> and an illustrative case study (adjusted from [15]) in <ref>.
<ref> concludes and presents ideas for future work.

§.§ Related Work - With some structure

[36] oldest often used citation to work with MDPIP (imprecise parameter).

[41] is some basic work of probabilistic interval reasoning.
[26] uses it to define probabilities on paths in IMCs, sometimes referred as "they introduced IMC".

[23] introduced IMCs according to several papers (formal verification community, Larsen).
[18] introduced BMDPs, AI paper.

The table shows lots of related work, ordered by year.
Generally, IMC and BMDP are the prevailing names;
there are no guaranteed algorithms I found.
RTDP has been tried for some things.
$\omega$-regular for BMDP has not been done before.
Going for coop/adv semantics should capture all relevant things.

Name 			    	Model 	    	Semantics			   	Property 			    Method 	    Comment
[18]	   	BMDP	   	adv/coop (opt/pes)	    Discounted reward		   	VI		    Introduce BMDP, AI paper

[24]	   	CTMDP	   	Robust(maxmin)		    Mean payoff			    LP or PI	   	Uncertain transition rates as compact sets

[4]		   	BMDP	   	Robust (adv)		    SSP (min exp rew)		   	RTDP	    Checks for goal reachability for preprocessing

[30]		    uncer. MDP   	Robust				    Fin. exp tot cost, disc cost    Complexity     Uncertainty handling comes at little extra cost

[37]	    IMC (IDTMC)   	rand/pes (UMC,IMDP)	    PCTL					    Complexity     UMC $\in$ NP $\cap$ coNP, IMDP P-hard

[38]		    BMDP		    adv/coop (opt/pes)	   	Mean payoff (avg rew)    VI

[45]		    BMDP		    adv/coop				   	Exp tot rew			   	VI		   Called control community by [20], defintely AI people

[9]	    IMC		   	rand/pes (UMC/IMDP)	   	omega-regular		    Complexity   No direct algorithms, but basis for all the other papers

[43]	    uncer. MDP    robust				    LTL			    ?		    CDC paper

[3]    IMC	    IMDP	    LTL	   Complexity+Algo   [2] says algo needn't converge to opt; sth about their sematics was weird

[32]   conv.uncer.MDP   rand/adv(nature/adv)   PCTL   Complexity+Algo    Compl. better than [9], large case studies

[17]   BMDP     robust(maxmin)     exp disc rew     (L/B)RTDP     conclude BRTDP is awesome

[5]   IMC   not sure     PCTL     algo     Handle open intervals

[29]   IMC/BMDP   not sure     PCTL     algo     Pattern match this, generate from realistic systems, verification+synthesis

[21]   BMDP(IMDP here)   not sure    PCTL     bisimulation     MDP with conv. uncer. Diff of static or dynamic resolving of intervals

[2]   parametric IMC   o-a-f-a or a-e-s    reach     algo     semantics are equiv for reach. pIMC > IMC,pMC; similar to [11]

[20]   BMDP(IMDP here)   robust(adv)   exp tot rew     Compl/algo     intervals in (0,1]. No guar. Good overview of related work.

[11]   augmented IMC    not sure     reach(qual,quant,appr)     complexity     aug means some trans have same. Similar to [2]

[15]    IMC   adv.   $\omega$-reg   algo   CDC, this got is here

[22]   IMC   not sure   reach I guess     SMC     Importance sampling for IMC

[35]   BDMP   not sure   not sure    topol. pol. it     can't access paper

[28, 42] are for the "precise parameters are often unrealistic in practice" argument.

[14] (Larsen) gives some decision problems for IMC, that are not relevant for our setting.

[8] is the survey of omega-regular games, where we delegate all the work.

§.§ Related Work - Comment to each paper, sorted by year

[36]: General MDPIP, nested policy iteration for controller and nature.

[23]: Refered to as "introduced IMCs". Calls it "interval specification systems". Also talks about modal specification system (may and must). UMC interpretation, study bisimulation and simulation preorders.

[41]: Used by KU02 as basically only reference, apparently basic work of probabilistic interval reasoning (over 3k citations, but could not find paper).

[28]: Used for saying that knowing precise probs is often not true in practice. Talks about how to handle the uncertainty of measurements, and how to get the intervals.

[42]: Citation for the "stuff is uncertain in reality" argument. Discusses 4 measures of uncertainty, one of which is upper and lower probability.

[18]: Introduce BMDP (AI paper), as subclass of MDPIP (imprecise parameter). Aggregate states argument for why we need them. Interval value functions, (interval policy evaluation), optimistic pessimistic criteria (adv and coop), interval value iteration for discounted reward (polynomial by handwaving that things are LPs :/).
15,17 and 18 (SatiaLave78 and WhiteEldeib68/94) in here are MDPIP references. After reading related work of this paper(GLD00), I conclude they are not really interesting for us.
What is interesting is that already here they realized that they are basically an SG and cite Shapley53.
Called "control community" by HHH+17. Definitely AI people.

[24]: CTMDP (cont time) with uncertain transition rates; mean payoff (different assumptions on how to resolve uncertainty) solved by LP or policy iteration.

[26]: Mathematical analysis of IMCs. Calls it interval-valued Markov chains. Might be useful for rigorous proofs, but otherwise seems unsurprising. Refered as "They introduced IMCs". IMDP interpretation, compute probability distribution after t steps.

[4]: Stochastic shortest path (min expected reward) in BMDP (called uncertain SSP). Uses RTDP.

[30]: Uncertain MDP, finite horizon expected total cost, or discounted total cost, robust.
Complexity results, implying that handling uncertainty comes at little extra cost.

[37]: IDTMC (IMC); PCTL is in PSPACE. Also prove lower complexity bounds for the problem. Differentiate UMC and IMDP semantics (UMC is NP and co-NP-hard; IMDP is P-hard). Use reduction based on BFS, give iterative algorithm. (model checking guys).

[38]: Mean payoff (average reward) BMDP, extending GLD99 (VI).

[45]: Reachability for BMDP (based on expected total reward, not sure whether they also solve that). They call it interval value iteration, but it does not give guarantees (only convergence from below).
They say it takes polynomial number of steps, but I don't get the proof.
11 here is a case study that we could look at and maybe use.
This also cites SatiaLave(53 instead of 78, but same title; scholar and dblp only know a 73 version) and WhiteEldeib94.
State that BMDPs differ from what [37] do, because SVA06 allows nondeterminism at every step. I think they are wrong here, as BMDPs as they use them (optimistic and pessimistic = adv and coop) are also IMDP semantics.
Called "control community" by HHH+17. Definitely AI people.

[9]: Solves omega-regular IMCs in IMDP and UMC semantics; gives complexity results, but no direct algorithms.

[14]: Decision problems on IMCs, that are not really interesting for us right now.

[8]: Survey of omega-regular SG. This is where we delegate all our problems.

[43]: A CDC paper. They define MDP and everything, we can maybe use their terminology.
Uncertain MDP (any set of transition probabilities is allowed, so IMDP is a special case; method should stay the same, as we know max/min prob), robust/worst-case semantics, LTL.
Feels similar in style as DC18.
Note that BLW13 also gives an algorithm for LTL adversarial, but for IMCs.

[3]: IMC with IMDP semantics
(though they state: Since IMC is history independent, it is different from MDP; I disagree, as the optimal policy always is positional for the properties they consider however, they also state it in the conclusion, so I might have missunderstood)
They give complexity for omega regular properties
(Reach is P-complete, unambiguous Büchi automata is $NP_{\Reals}$-complete, LTL is in EXPSPACE and PSPACE-hard. For fixed parameters or qualitative checking, it is PSPACE-complete).
They also give an algorithm for LTL model checking of IMCs, based on expectation maximization.
[2] says that it converges, but not necessarily to the global optimum.

[32]: PCTL for convex uncertain MDPs (includes IMDPs).
Complexity is PTIME (improve CSH08).
Differentiate nature and adversary for the second player.
Give algorithm.
Large case studies (zeroconf, consensus).

[17]: BMDP, expected discounted reward, robust/maximin.
Does RTDP, considers labelling and bounded version.
Conclude that BRTDP is awesome (have implementation, beat some state-of-the-art thing).

[5]: IMCs, PCTL, but open intervals. Show how to handle the problem.

[29]: Jan said we should pattern match this.
How to generate IMCs and BMDP from realistic systems.
Check them against PCTL, both for Verification (which states satisfy) and controller synthesis (how to behave to maximize prob to satisfy).

[21]: Interval MDP (called IMDP); model checking probabilistic CTL properties of MDP with convex uncertainties; use bisumlation to reduce size. They state (Sec 3) that there is a difference between static and dynamic resolving of intervals; dynamic is easier to work with algorithmically and is relaxation of static approach, that is often intractable [3, 9]. I do not understand why.

[2]: parametric IMC, seems similar to AIMC.
Differentiates the semantics "once-and-for-all" or "at-every-step"; proves that for reachability in pIMC and IMC, they are equivalent.
pIMCs can express everything that pMCs and IMCs can express.
They show how to check consistency of pIMCs as well as how to synthesize parameters s.t. a qual/quant reach query is satisfied.
They have another paper where they synthesize parameters for pIMCs, but this paper here is better.
(Also, there is a journal version of this, probably should cite that)

[20]: IMDP, adverserial semantics (robust strategies).
Give an overview of uncertain transitions studied in literature in related work.
Show that multi-obj exp tot rew (hence also reach) is PSPACE-hard.
Note: They assume intervals to be in (0,1], which makes things a lot easier, and allows them to preprocess their IMDP and remove infinite rewards (reward cycles).
Compute pareto curve of the query, but without guarantees (bad stopping criterion).

[11]: Introduces AIMCs (augmented), which allows for saying that some transitions have to have the same probability. Gives complexity bounds for several versions of reachability (qual, quant, appr).

[15]: The CDC paper that got us here.
IMC, adversarial semantics, $\omega$-regular properties.

[22]: Importance sampling for IMCs. (SMC approach).

[35]: BMDP, topological policy iteration algorithm, don't know which property. Can't access the paper.

§ PRELIMINARIES

In this section, we recall basics of probabilistic systems and set up the notation.
As usual, $\Naturals$ refers to the natural numbers (including 0).
A probability distribution on a finite set $X$ is a mapping $\distribution : X \to [0,1]$, such that $\sum_{x\in X} \distribution(x) = 1$.

We use $\Distributions(X)$ to denote the set of all probability distributions on the set $X$.

Given some set $S$, we use $S^\star$ and $S^\omega$ to denote the set of all finite and infinite sequences comprising elements of $S$, respectively.

[Example BMDP]
[auto,initial text=]
[state,initial left] at (-0.5,0) (q0) $q_0, x$;
[actionnode] at (0.5,0) (q0a) ;

[state] at (2,-1) (q1) $q_1, y$;
[actionnode] at (2,-1.7) (q1a) ;
[actionnode] at (2.5,0) (q1b) ;

[state] at (2,1) (q2) $q_2, z$;
[actionnode] at (0.5,1.5) (q2a) ;

(q0) edge node[actiontext] $a$ (q0a)
(q1) edge[out=-60,in=0] node[actiontext] $b$ (q1a)
(q1) edge[in=180,out=90] node[actiontext] $c$ (q1b)
(q2) edge node[actiontext] $d$ (q2a)

(q0a) edge node[probtext,sloped,anchor=north,pos=0.5] $[0.5, 1.0]$ (q1)
(q0a) edge node[probtext,sloped,anchor=south,pos=0.5] $[0.0, 1.0]$ (q2)

(q1a) edge[out=-180,in=-120] node[probtext] $[0.7, 1.0]$ (q1)
(q1b) edge[out=0,in=30] node[probtext,sloped,anchor=north,pos=0.7] $[0.25, 1.0]$ (q1)
(q1b) edge[out=0,in=-30] node[probtext,sloped,anchor=south,pos=0.7] $[0.5, 1.0]$ (q2)

(q2a) edge[out=160,in=90,sloped] node[probtext,pos=0.5,anchor=south] $[0.0, 1.0]$ (q0)
(q2a) edge[out=160,in=100] node[probtext] $[0.5, 1.0]$ (q2)

[MDPs consistent with the BMDP]
[auto,initial text=]
[state,initial left] at (-0.5,0) (q0) $q_0$;
[actionnode] at (0.5,0) (q0a) ;

[state] at (2,-1) (q1) $q_1$;
[actionnode] at (2,-1.7) (q1a) ;
[actionnode] at (2.5,0) (q1b) ;

[state] at (2,1) (q2) $q_2$;
[actionnode] at (0.5,1.5) (q2a) ;

(q0) edge node[actiontext] $a$ (q0a)
(q1) edge[out=-60,in=0] node[actiontext] $b$ (q1a)
(q1) edge[in=180,out=90] node[actiontext] $c$ (q1b)
(q2) edge node[actiontext] $d$ (q2a)

(q0a) edge node[probtext,sloped,anchor=north] $1.0$ (q1)

(q1a) edge[out=-180,in=-120] node[probtext] $1.0$ (q1)
(q1b) edge[out=0,in=30] node[probtext,sloped,anchor=north,pos=0.6] $0.5$ (q1)
(q1b) edge[out=0,in=-30] node[probtext,sloped,anchor=south,pos=0.6] $0.5$ (q2)

(q2a) edge[out=160,in=90,sloped] node[probtext,anchor=south] $0.5$ (q0)
(q2a) edge[out=160,in=100] node[probtext] $0.5$ (q2)

[auto,initial text=]
[state,initial left] at (-0.5,0) (q0) $q_0$;
[actionnode] at (0.5,0) (q0a) ;

[state] at (2,-1) (q1) $q_1$;
[actionnode] at (2,-1.7) (q1a) ;
[actionnode] at (2.5,0) (q1b) ;

[state] at (2,1) (q2) $q_2$;
[actionnode] at (0.5,1.5) (q2a) ;

(q0) edge node[actiontext] $a$ (q0a)
(q1) edge[out=-60,in=0] node[actiontext] $b$ (q1a)
(q1) edge[in=180,out=90] node[actiontext] $c$ (q1b)
(q2) edge node[actiontext] $d$ (q2a)

(q0a) edge node[probtext,sloped,anchor=north] $0.5$ (q1)
(q0a) edge node[probtext,sloped,anchor=south] $0.5$ (q2)

(q1a) edge[out=-180,in=-120] node[probtext] $1.0$ (q1)
(q1b) edge[out=0,in=30] node[probtext,sloped,anchor=north,pos=0.6] $0.25$ (q1)
(q1b) edge[out=0,in=-30] node[probtext,sloped,anchor=south,pos=0.6] $0.75$ (q2)

(q2a) edge[out=160,in=100] node[probtext] $1.0$ (q2)

Examples of an BMDP and its instantiations.
The acceptance is $\RabinAcc = \{\rabinpair{q_2}{q_1}\}$.

§.§ Markov Decision Processes

A Markov decision process (MDP) is a tuple $\MDP = (\States, \initialstate, \Actions, \stateactions, \mdpTransitions, \RabinAcc)$, where
$\States$ is a finite set of states,
$\initialstate \in \States$ is the initial state,
$\Actions$ is a finite set of actions,
$\stateactions: \States \to 2^{\Actions} \setminus \{\emptyset\}$ assigns to every state a non-empty set of available actions,
$\mdpTransitions: \States \times \Actions \to \Distributions(\States)$ is a transition function that for each state $s$ and (available) action $a \in \stateactions(s)$ yields a probability distribution over successor states, and
$\RabinAcc \in 2^\States \times 2^\States$ is the Rabin acceptance.
Furthermore, for ease of notation we assume w.l.o.g. that actions are unique for each state, i.e. $\stateactions(s) \intersection \stateactions(s') = \emptyset$ for $s \neq s'$.[The usual procedure to achieve this in general is to replace $\Actions$ by $\States \times \Actions$ and to adapt $\stateactions$ and $\mdpTransitions$ appropriately.]
An element $(\RabinFin_i, \RabinInf_i) \in \RabinAcc$ is called Rabin pair.
We assume w.l.o.g. that $\RabinFin_i \intersection \RabinInf_i = \emptyset$ for all pairs.

In figures, we denote a Rabin pair $(\RabinFin, \RabinInf)$ by $\rabinpair{\RabinFin}{\,\RabinInf}$.

An MDP with $\cardinality{\stateactions(s)} = 1$ for all $s \in \States$ is called Markov chain (MC).
For ease of notation, we overload functions that map to distributions $f: Y \to \Distributions(X)$ by $f: Y \times X \to [0, 1]$, where $f(y, x) := f(y)(x)$.
For example, instead of $\mdpTransitions(s, a)(s')$ we write $\mdpTransitions(s, a, s')$ for the probability of transitioning from state $s$ to $s'$ using action $a$.

An infinite path in an MDP is an infinite sequence $\infinitepath = s_0 a_0 s_1 a_1 \cdots$, such that $a_i \in \stateactions(s_i)$ and $\mdpTransitions(s_i,a_i, s_{i+1}) > 0$ for every $i \in \Naturals$.
We use $\infinitepath_i$ to refer to the $i$-th state $s_i$ in a given path.
A finite path
is a finite prefix of an infinite path.
$\Inf(\infinitepath) \subseteq \States$ denotes the set of all states which are visited infinitely often in the path $\infinitepath$.

A path $\infinitepath$ is accepted, denoted $\infinitepath \accepted \RabinAcc$, if an only if there exists a Rabin pair $(\RabinFin_i, \RabinInf_i) \in \RabinAcc$ such that all states in $\RabinFin_i$ are visited finitely often, i.e. $\RabinFin_i \intersection \Inf(\infinitepath) = \emptyset$, and at least one state of $\RabinInf_i$ is visited infinitely often, i.e. $\RabinInf_i \intersection \Inf(\infinitepath) \neq \emptyset$.
We call such a Rabin pair accepting for $\infinitepath$.

Often, system and specification are modelled separately, e.g., by a labelled MDP together with a description of an $\omega$-regular property such as an LTL formula [31] or an automaton.
The common approach then is to build the product of the system, the BMDP, and an automaton describing the specification;
this results in a system as described in <ref>.
Since our work is largely independent of this construction's details we omit this step for simplicity.
We highlight that indeed [15] only refers to the product throughout the main body of their work.
Details can be found in <ref> and, e.g., [1].

A policy (also called controller, strategy) on an MDP is a function $\strategy : (\States \times \Actions)^*\times S \to \Distributions(\Actions)$ which given a finite path $\finitepath = s_0 a_0 s_1 a_1 \dots s_n$ yields a probability distribution $\strategy(\finitepath) \in \Distributions(\stateactions(s_n))$ on the actions to be taken next.
We call a policy memoryless randomized (or stationary) if it is of the form $\strategy: \States \to \Distributions(\Actions)$, and memoryless deterministic (or positional) if it is of the form $\strategy: \States \to \Actions$.
Later in the paper, we prove that positional strategies are indeed sufficient for all considered problems.
We denote the set of all policies of an MDP by $\Strategies$.
By fixing the policy $\strategy$ in an MDP $\MDP$, we naturally obtain a MC and thus a probability measure $\Probability[\MDP]<\strategy>$ over potential runs [33].
Throughout this work, we are interested in finding policies which maximize the probability of accepting runs, i.e. $\sup_{\strategy \in \Strategies} \Probability[\MDP]<\strategy>[\infinitepath \accepted \RabinAcc]$.

An end component in an MDP is a pair $(T, A)$ of a set of states $T$ and a set of actions $A$ such that the system can remain within the states $T$ indefinitely, using only actions from $A$.
Formally, a pair $(T, A)$, where $\emptyset \neq T \subseteq \States$ and $\emptyset \neq A \subseteq \Union_{s \in T} \stateactions(s)$, is an end component of an MDP $\MDP$ if
(i) for all $s \in T, a \in A \intersection \stateactions(s)$ we have $\{s' \mid \mdpTransitions(s, a, s') > 0\} \subseteq T$, and
(ii) for all $s, s' \in T$ there is a finite path $\finitepath = s a_0 \dots a_n s' \in (T \times A)^* \times T$, i.e. the path stays inside $T$ and only uses actions in $A$.
An end component $(T, A)$ is a maximal end component (MEC) if there is no other end component $(T', A')$ such that $T \subseteq T'$ and $A \subseteq A'$.
The set of MECs of an MDP $\MDP$ is denoted by $\Mecs(\MDP)$ and can be obtained in polynomial time [13].
For further detail, see <cit.>.

§.§ Bounded-parameter Markov Decision Processes

A bounded-parameter Markov decision process (BMDP) is a tuple $\BMDP = (\States, \initialstate, \Actions, \stateactions, \bmdpTransitionsLower, \bmdpTransitionsUpper, \RabinAcc)$, where
$\States$, $\initialstate$, $\Actions$, $\stateactions$ and $\RabinAcc$ are as in the definition of MDP, and
$\bmdpTransitionsLower, \bmdpTransitionsUpper: \States \times \Actions \times \States \to [0, 1]$ are lower and upper bounds on the transition probability in each state.
Again, we assume that actions are unique for each state.
For consistency, we require that $\sum_{s' \in \States} \bmdpTransitionsLower(s, a, s') \leq 1 \leq \sum_{s' \in \States} \bmdpTransitionsUpper(s, a, s')$ for each state $s$ and action $a \in \stateactions(s)$.

Given a BMDP $\BMDP = (\States, \initialstate, \Actions, \stateactions, \bmdpTransitionsLower, \bmdpTransitionsUpper, \RabinAcc)$, we call a Markov decision process $\MDP = (\States, \initialstate, \Actions, \stateactions, \mdpTransitions, \RabinAcc)$ consistent with $\BMDP$, denoted $\MDP \in \BMDP$, if and only if $\MDP$'s transition probabilities satisfy $\BMDP$'s bounds, i.e. $\bmdpTransitionsLower(s, a, s') \leq \mdpTransitions(s, a, s') \leq \bmdpTransitionsUpper(s, a, s')$ for all states $s, s' \in \States$ and actions $a \in \stateactions(s)$.
Note that in general there are uncountably many MDPs consistent with a BMDP $\BMDP$.

A BMDP with $\cardinality{\stateactions(s)} = 1$ for all $s \in \States$ is called Interval Markov chain (IMC) (e.g., [9]).

See <ref> for an example BMDP and <ref> for two MDPs consistent with this BMDP.

§.§ Stochastic Games

For our analysis, we additionally need the concept of stochastic games.
These can be understood as an MDP where, instead of a single agent controlling the process, we have two antagonistic players.
Intuitively, the first player's aim is to obtain an accepted path, while the second player aims to stop the first player from doing so.
Each state in the game is owned by one of the two players and the owner of a particular state can decide which action to take in that state.

A stochastic game (SG) is a tuple $\SG = (\States, \initialstate, \Actions, \stateactions, \sgTransitions, \RabinAcc, \ownerFunction)$, where
$(\States, \initialstate, \Actions, \stateactions, \sgTransitions, \RabinAcc)$ is an MDP and
$\ownerFunction : \States \to \{\systemPlayer, \environmentPlayer\}$ is an ownership function, assigning each state to either player $\systemPlayer$ or player $\environmentPlayer$.
This naturally gives rise to the sets of states $\StatesSystem$ and $\StatesEnvironment$, which are controlled by the respective player.

The definitions of (in)finite paths directly extend to stochastic games.
Policies are slightly modified, since each player can only make decisions in a part of the game.
Formally, we have two kinds of policies $\strategySystem : (\States \times \Actions)^* \times \StatesSystem \to \Distributions(\Actions)$ and $\strategyEnvironment : (\States \times \Actions)^* \times \StatesEnvironment \to \Distributions(\Actions)$, one for each player.
We denote the set of all policies of the respective players by $\StrategiesSystem$ and $\StrategiesEnvironment$.
Fixing the policy of a single player yields an MDP, denoted $\SG(\strategy_i)$; fixing both players' policies $\strategySystem$ and $\strategyEnvironment$ again yields an MC and measure over the set of runs, denoted $\Probability[\SG]<\strategySystem, \strategyEnvironment>$ [12].

§ PROBLEM STATEMENT

In this work, we are given a BMDP and want to control it such that the probability of an accepting run is maximized.
This raises two orthogonal questions:

Firstly, the semantics of the interval constraints have to be fixed.
We consider two different popular interpretations, called uncertain and antagonistic.
In the uncertain (or design-choice) model, an external environment fixes the transition probabilities once and for all, i.e. for a BMDP $\BMDP$ a particular consistent MDP $\MDP \in \BMDP$ is chosen.
In the antagonistic model, the external environment instead is allowed to change the transition probabilities at every step, taking into account the full path so far.
These interpretations have been shown to be yield the same optima for reachability in interval Markov chains [10].
In the following, we show that this also is the case for BMDP with Rabin objectives; hence we do not distinguish the semantics in our formal problem statement.

Secondly, it is not specified whether the aforementioned environment is cooperative or antagonistic.
We consider both of these two extreme cases.
In particular, we are interested in finding the maximal probability of acceptance while assuming that all transition probabilities are chosen (i) to our liking and (ii) as bad as possible.

Formally, given a BMDP $\BMDP$ we want to compute

* $\probupper(\BMDP) = \sup_{\strategy \in \Strategies} \sup_{\MDP \in \BMDP} \Probability[\MDP]<\strategy>[\infinitepath \accepted \RabinAcc]$, and

* $\problower(\BMDP) = \sup_{\strategy \in \Strategies} \inf_{\MDP \in \BMDP} \Probability[\MDP]<\strategy>[\infinitepath \accepted \RabinAcc]$.

Further, we are interested in the optimal policy and the best- / worst-case MDP consistent with the given BMDP, if it exists, i.e. the witnesses for the above values.

Case (<ref>) can be understood as a design challenge.
We are interested in building our system, i.e. finding an optimal assignment for all transitions, such that we maximize the probability of acceptance.
On the other hand, Case (<ref>) can be thought of as uncertainty about the real world or measurement imprecisions.
Here, we rather are interested in optimizing the worst case and want to find a safe strategy, able to reasonably cope with any concrete instantiation of the intervals.

Consider the situation depicted in <ref>.
We are interested in finding the upper and lower bounds for the BMDP given in <ref>.
The upper bound, $1.0$, is exhibited by the left MDP of <ref>.
There, we end up in $q_1$ with probability $1$ and, by always playing action $b$, get an accepting run with probability $1$.
The right MDP shows the lower bound of $0.5$, since we get stuck in state $q_2$ with probability $0.5$.
Observe that if action $d$ in state $q_2$ had a non-zero probability of moving to $q_0$, the resulting run would be accepting with probability $1$, since we would almost surely eventually reach $q_1$.

In the following, we re-interpret existing approaches, and present our unified approach for solving BMDP.

§ SOLUTION APPROACH

In order to explain our approach, we first shed some light on the simpler case of interval Markov chains (IMC), handled in [15], and provide a different perspective on their approach.

In [15], the authors present a specialized algorithm for dealing with IMCs.
In essence, they compute maximal sets of (non)accepting states and then obtain the final value by solving a reachability query for these states.
We now provide a different viewpoint on their algorithm which will help us solve the more general case of BMDPs.

The key observation is the following.
We can view the intervals in an IMC as a player (the external environment) picking the transition probabilities at every step.
This can be understood as an MDP, where in every state the player has an action for each distribution satisfying the interval constraints.
This MDP has uncountably many actions in general, as there are infinitely many possibilities to choose the probabilities.
However, all possible distributions can be constructed as a convex combination of finitely many special cases which are basic feasible solutions (BFS) of a linear program [9, 19] (also known as corner-point abstraction).
We can identify each of these special solutions and use them to construct a finite MDP.
This MDP is often called interval Markov decision process (IMDP); not to be confused with BMDP.
By model checking the IMDP, using established methods, we obtain the desired result for the IMC.

Indeed, the algorithm presented in <cit.> actually can be interpreted as a symbolic adaption of the standard model checking procedure for Rabin objectives on the MDP, namely an adapted MEC decomposition together with a reachability query <cit.>.
Similar to the methods presented in [19], their specialized algorithm cleverly avoids explicit computation of the exponentially large IMDP, achieving polynomial runtime.

Before we can extend these ideas to BMDP, we explain some details of the basic feasible solutions, since they are essential to our idea.

§.§ Basic feasible solutions

[Example IMC]
[auto,initial text=]
[state] at (0,0) (q0) $q_0$;
[state] at (1.75,1.25) (q1) $q_1$;
[state] at (1.75,0) (q2) $q_2$;
[state] at (1.75,-1.25) (q3) $q_3$;

(q0) edge[sloped, bend left, anchor=south] node[probtext] $[0.0, 0.9]$ (q1)
(q0) edge[sloped, anchor=south] node[probtext] $[0.1, 0.4]$ (q2)
(q0) edge[sloped, bend right, anchor=north] node[probtext] $[0.3, 0.7]$ (q3)

[Visualized constraints.]
[auto,initial text=]
axis lines=box,
ylabel=$p(q_2)$,y label style=anchor=north,rotate=-90,
zlabel=$p(q_3)$,z label style=rotate=-90
3 [no marks,densely dashed] coordinates (0.0,0.1,0.3) (0.9,0.1,0.3) (0.9,0.4,0.3) (0.0,0.4,0.3) (0.0,0.1,0.3);
3 [no marks,densely dashed] coordinates (0.0,0.1,0.7) (0.9,0.1,0.7) (0.9,0.4,0.7) (0.0,0.4,0.7) (0.0,0.1,0.7);

3 [no marks,densely dashed] coordinates (0.0,0.1,0.3) (0.0,0.1,0.7);
3 [no marks,densely dashed] coordinates (0.9,0.1,0.3) (0.9,0.1,0.7);
3 [no marks,densely dashed] coordinates (0.0,0.4,0.3) (0.0,0.4,0.7);
3 [no marks,densely dashed] coordinates (0.9,0.4,0.3) (0.9,0.4,0.7);

3 [fill=gray, opacity=0.1, fill opacity=0.4] coordinates (1.0,0.0,0.0) (0.0,1.0,0.0) (0.0,0.0,1.0);

3 [mark=diamond, fill=darkgray, draw=none, opacity=1.0, fill opacity=0.4] coordinates (0.0,0.3,0.7) (0.2,0.1,0.7) (0.6,0.1,0.3) (0.3,0.4,0.3) (0.0,0.4,0.6);

Visualization of the set of basic feasible solutions.
The left picture shows a state together with its transition constraints in an IMC, the right picture depicts a geometric representation of the inequalities induced by the interval constraints.
The light grey plane corresponds to the distribution constraints (<ref>), while the dashed box represents the interval constraints (<ref>).
Finally, the dark grey area shows the set of consistent distributions and the diamonds mark the basic feasible solutions.

Given an IMC $(\States, \initialstate, \bmdpTransitionsLower, \bmdpTransitionsUpper, \labelling)$ and a state $s \in \States$, we are interested in the set of all successor distributions $p \in \Distributions(\States)$ consistent with the constraints imposed by the IMC.
In particular, the following constraints have to be satisfied:

*  $\sum_{s' \in \States} p(s') = 1$, and

*  $\bmdpTransitionsLower(s, s') \leq p(s') \leq \bmdpTransitionsUpper(s, s')$ for all $s' \in \States$.

Geometrically, <ref> constrains the solution set to a plane, while <ref> bounds it in a box, as shown in <ref>.
Since each point in the solution corresponds to a valid transition distribution and vice versa, we identify solutions of the constraints with their corresponding distributions.
Observe that the resulting solution set (and the corresponding set of distributions) is convex and any element of this set can be obtained by a convex combination of the corner-points, which are the basic feasible solutions.

There is one dimension per successor state and thus at most exponentially many basic feasible solutions.
This set can be computed in exponential time using standard theory of linear programs or simple geometric computations.
Due to lack of space we refer the reader to, e.g., <cit.> for further detail.

§.§ Solving BMDP

When solving Rabin objectives on BMDPs, we observe one central problem:
The set of end components depends on the choice of intervals.
For example, consider the BMDP in <ref>.
This BMDP comprises only one MEC containing all three states.
However, depending on the choice of probabilities, edges may be removed from the underlying graph, as for example in the right MDP of <ref>.
This MDP contains two MECs, namely $(\{q_1\}, \{b\})$ as well as $(\{q_2\}, \{d\})$.

In [15], a similar problem was encountered, as in IMC the set of bottom strongly connected components can be modified by the choice of intervals.
The authors solved the problem implicitly by considering states where the Rabin objective is not satisfied as leaky, i.e. not part of any strongly connected component.

In contrast to that, our general solution relies on making the possible choices of the probabilities explicit.
We utilize the key observation that the non-determinism induced by intervals essentially corresponds to adding a player, who picks the probabilities for the intervals.
Thus, we reduce the BMDP to a stochastic game that can be solved by known model checking methods.
However, in the next section we introduce a more sophisticated approach inspired by the ideas of [15].

Intuitively, the reduction from BMDP to SG amounts to replacing every action in the BMDP with an additional state owned by the new player.
In this state, the new player can choose from the corresponding basic feasible solutions, allowing him to construct any consistent distribution over the successors.
An example of this construction is shown in <ref>, where the game constructed from the BMDP in <ref> is depicted.
This new player can play against the system (yielding $\problower$) or cooperate (yielding $\probupper$).

[auto,initial text=]
[maxstate,initial left] at (0,0) (q0) $q_0$;
[minstate] at (1.5,0) (q0a) $(q_0, a)$;
[actionnode] at (2.5,0) (q0a1) ;

[minstate] at (3,-1.5) (q1) $q_1$;
[minstate] at (1.5,-1.5) (q1b) $(q_1, b)$;
[minstate] at (5,0) (q1c) $(q_1, c)$;
[actionnode] at (4.25,0.8) (q1c1) ;
[actionnode] at (4.25,-0.8) (q1c2) ;

[maxstate] at (3,1.5) (q2) $q_2$;
[minstate] at (0.75,1.5) (q2d) $(q_2, d)$;
[actionnode] at (0.4,2) (q2d1) ;

(q0) edge[pos=0.4] node[actionnode,anchor=center]  (q0a)
(q1) edge[bend left] node[actionnode,anchor=center]  (q1b)
(q1) edge[bend right=40] node[actionnode,anchor=center]  (q1c)
(q2) edge node[actionnode,anchor=center]  (q2d)

(q0a) edge[bend left=10] node[actionnode,anchor=center]  (q1)
(q1b) edge[bend left] node[actionnode,anchor=center]  (q1)
(q2d) edge[bend left] node[actionnode,anchor=center]  (q0)

(q0a) edge (q0a1)
(q1c) edge (q1c1)
(q1c) edge (q1c2)
(q2d) edge (q2d1)

(q0a1) edge[in=90,out=0] node[probtext,sloped,anchor=north] $0.5$ (q1)
(q0a1) edge[in=-90,out=0] node[probtext,sloped,anchor=south] $0.5$ (q2)

(q1c1) edge[in=60,out=180,pos=0.2] node[probtext,sloped,anchor=south] $0.25$ (q1)
(q1c1) edge[in=-20,out=130] node[probtext,sloped,anchor=south] $0.75$ (q2)

(q1c2) edge[in=20,out=-130] node[probtext,sloped,anchor=south] $0.5$ (q1)
(q1c2) edge[in=-60,out=180,pos=0.2] node[probtext,sloped,anchor=south] $0.5$ (q2)

(q2d1) edge[in=100,out=135] node[probtext,sloped,anchor=south] $0.5$ (q0)
(q2d1) edge[in=100,out=135] node[probtext,sloped,anchor=south] $0.5$ (q2)

The stochastic game obtained from the BMDP in <ref> by the construction in the proof of Theorem 2.
States owned by the system are depicted by rectangles, while environment states have rounded corners.
For readability, we omit all action labels.
Furthermore, we omit action nodes for probability $1$ transitions.

For every BMDP $\BMDP$, there exists an SG $\SG(\BMDP)$ such that

* $\probupper(\BMDP) = \sup_{\strategySystem \in \StrategiesSystem} \sup_{\strategyEnvironment \in \StrategiesEnvironment} \Probability[\SG(\BMDP)]<\strategySystem,\strategyEnvironment>[\infinitepath \accepted \RabinAcc]$, and

* $\problower(\BMDP) = \sup_{\strategySystem \in \StrategiesSystem} \inf_{\strategyEnvironment \in \StrategiesEnvironment} \Probability[\SG(\BMDP)]<\strategySystem,\strategyEnvironment>[\infinitepath \accepted \RabinAcc]$

Let $\BMDP = (\States, \initialstate, \Actions, \stateactions, \bmdpTransitionsLower, \bmdpTransitionsUpper, \labelling)$ be a BMDP.
In contrast to IMC, where we found the basic feasible solutions for a state, in BMDP we have to consider state-action pairs.
Recall that we assumed that each action belongs to a single state.
Hence, each $a \in \Actions$ induces a set of basic feasible solutions, given by the constraints $\bmdpTransitionsLower(s, a)$ and $\bmdpTransitionsUpper(s, a)$, where $s$ is the unique state with $a \in \stateactions(s)$.
We denote this set by $\BFS(a)$, and it can be computed as described in <ref>.
Recall that any $p \in \BFS(a)$ corresponds to a distribution over states.

The SG $\SG(\BMDP) = (\States', \initialstate, \Actions', \stateactions', \sgTransitions, \RabinAcc, \ownerFunction)$ is constructed from $\BMDP$ as follows.

* $\States' = \States \union \{(s, a) \mid s \in \States \land a \in \stateactions(s)\}$,

* $\Actions' = \Actions \union \{(a, p) \mid a \in \Actions, p \in \BFS(a)\}$, and

* $\ownerFunction(s) = \systemPlayer$ if $s \in \States$ and $\environmentPlayer$ otherwise, i.e. all newly introduced states $(s, a)$ belong to the environment.

* For every old state $s \in \States$ we set

* $\stateactions'(s) = \stateactions(s)$ and

* $\sgTransitions(s, a, (s, a)) = 1$ (and 0 for all other states) for all actions $a \in \stateactions(s)$.

* For every new state $(s, a) \in \States' \setminus \States$ we set

* $\stateactions'((s, a)) = \{(a, p) \mid p \in \BFS(a)\}$ and

* $\sgTransitions((s, a), (a, p), s') = p(s')$ for all $p \in \BFS(a)$.

For any consistent MDP $\MDP \in \BMDP$, there exists a policy for the other player $\strategyEnvironment$ inducing the transition function of $\MDP$, i.e. for all $\strategySystem \in \StrategiesSystem$ we have $\Probability[\MDP]<\strategySystem>[\infinitepath \accepted \RabinAcc] = \Probability[\SG(\BMDP)]<\strategySystem, \strategyEnvironment>[\infinitepath \accepted \RabinAcc]$, and vice versa.
This can be proven completely analogously to the proof for IMC, see, e.g., <cit.>.
Intuitively, randomizing over the BFS exactly yields the set of valid distributions.

This immediately yields the desired equality.

Positional policies suffice to achieve optimal solutions in BMDP.
Consequently, the uncertain and antagonistic semantics are equivalent for the optima.

Positional policies are sufficient for Rabin objectives in SG [8], and thus by the reduction of <ref> also for BMDP.
Hence the best policy for choosing the intervals is positional both for maximization and minimization, and there is no benefit in switching.

This result relies on the fact that the objective $\RabinAcc$ is already part of the BMDP.
See Appendix <ref> for further discussion.

To solve $\omega$-regular objectives for SGs, we use the strategy improvement algorithm presented in [7] and the reachability algorithm for MDPs from [1], which yields both the maximum and minimum probability, as well as the optimal controller.
Given a BMDP $\BMDP$, our procedure works as follows:

* Lower bound:

* Use <cit.> to solve $\SG(\BMDP)$ with the given Rabin objective $\RabinAcc$.
This yields the optimal player 1 policy $\strategySystem$, which induces an MDP $\MDP_{\strategySystem}$.
Note that the actions of the system, the original non-determinism of the BMDP, are fixed in $\MDP_{\strategySystem}$, and the remaining non-determinism belongs to the environment player choosing the intervals.

* Compute the minimum reachability probability with the algorithm from <cit.>, to obtain the the value $\problower$ and the worst-case environment policy $\strategyEnvironment$ for $\MDP_{\strategySystem}$, and thus the worst-case instantiation of the intervals.

* Upper bound:

* Let $\MDP(\BMDP)$ be the MDP obtained by assigning all nodes in $\SG(\BMDP)$ to player $\systemPlayer$.

* Use standard model checking procedures to obtain the best policy $\strategy$ for $\MDP(\BMDP)$ and the value $\probupper$; the policy handles both the non-determinism of the system and the instantiation of the intervals.

This procedure correctly computes

* $\problower(\BMDP)$, the optimal policy $\strategySystem$ to achieve it and the worst-case MDP, and

* $\probupper(\BMDP)$, and $\strategy$, describing the best-case system controller as well as the best choice of intervals.

It terminates in time exponential in the size of the $\SG(\BMDP)$, which in turn is exponential in the size of $\BMDP$.

The correctness follows directly from <ref> and the correctness of the the used algorithms <cit.>, <cit.>.

The complexity is dominated by the computation of the game $\SG(\BMDP)$ and its solution process.
The SG is exponential in the size of the BMDP (see <ref>) and the solution algorithm takes time exponential in the size the game <cit.>.

We can immediately apply the presented methods to bounded-parameter stochastic games, i.e. stochastic games with transition probability intervals.
In particular, we do not need to introduce another player, as the states added by the construction in the proof of <ref> can be assigned to one of the existing players – player 1 in the uncertain and player 2 in the antagonistic setting.
Thus the system remains a stochastic game.

§.§ Improving computation of upper bounds

Note that for the computation of the upper bounds, we did not make use of the second player, but instead only introduced new states for the existing player, yielding an exponentially large MDP.
By adapting observations from [15], we can improve on this algorithm by directly analysing the MC and avoiding the explicit construction of the SG, yielding a polynomial time algorithm for computing the upper bound.

Intuitively, the improved procedure symbolically identifies for each Rabin pair in $(\RabinFin, \RabinInf) \in \RabinAcc$ the winning end components.
It does so by computing MECs while temporarily excluding states in $\RabinFin$.
After obtaining all states that are in a winning end-component for some pair, we compute the probability to reach any of these states.
The structure of this improved procedure is similar to <cit.>, and relies on methods to compute the MEC decomposition on a BMDP from [19] and the reachability algorithm from [32].[In [19] and [32], the authors refer to BMDP as IMDP.]

Given a BMDP $\BMDP$, our procedure works as follows:

* For each Rabin pair $(\RabinFin_i, \RabinInf_i) \in \RabinAcc$:

* Construct a modified copy $\BMDP_i$ of $\BMDP$ where all $(s, q)$ with $q \in \RabinFin_i$ absorbing, i.e. all outgoing transitions are replaced with a self-loop.

* Compute the MEC decomposition of the resulting BMDP using <cit.>.

* If a MEC $(T, A)$ has a non-empty intersection with $\RabinInf_i$, then it is winning and all states $T$ are added to the set of winning states $W$.

* Compute the maximal probability of reaching $W$, using the methods presented in, e.g., [32].

This procedure correctly computes $\probupper(\BMDP)$ and terminates in polynomial time.

By <cit.>, we get that the MEC computation of a BMDP $\BMDP$ through <cit.> is correct, i.e. the computed MECs correspond to the MECs of $\SG(\BMDP)$.
The MECs identified as winning in Step <ref> and <ref> thus indeed are winning MECs in $\MDP(\BMDP)$, where $\MDP(\BMDP)$ is as in Step <ref> of the procedure of <ref>.
Consequently, we exactly identify the set of potentially winning states.
Finally, the correctness of the algorithms used to compute the reachability in Step <ref> yields the overall correctness.

For the complexity, observe that each step requires at most polynomial time (<cit.> for Step <ref>, <cit.> for Step <ref>) and there are only linearly many Rabin pairs in $\RabinAcc$.

Note that in the setting of [15] a procedure for computing the upper bound is sufficient, as the lower bound can be computed as 1 minus the maximal probability to satisfy the negation of the specification.
However, this idea is not applicable in the BMDP setting due to the alternation of $\sup$ and $\inf$ in the definition of $\problower$.

Our algorithm can easily be extended to use generalized Rabin transition acceptance, allowing for efficient practical implementation.
See [6] for details.

§ CASE STUDY

[auto,initial text=,scale=0.9]
[state,initial left] at (0,0) (q0) $q_0$;
[state,fill=green] at (3,0) (q1) $q_1$;
[state] at (6,0) (q2) $q_2$;
[state,fill=red] at (0,-3) (q3) $q_3$;
[state] at (3,-3) (q4) $q_4$;
[state,fill=red] at (6,-3) (q5) $q_5$;

[actionnode] at (0,-1.5) (q0d) ;
[actionnode] at (0.75,-0.75) (q0r) ;

[actionnode] at (2,-1.5) (q1d) ;
[actionnode] at (1.5,0.4) (q1l) ;
[actionnode] at (4.5,0.4) (q1r) ;

[actionnode] at (6,-1.5) (q2d) ;
[actionnode] at (5.25,-0.75) (q2l) ;

[actionnode] at (0,-3.7) (q3s) ;

[actionnode] at (1.5,-3) (q4l) ;
[actionnode] at (4.5,-3) (q4r) ;
[actionnode] at (4,-1.5) (q4u) ;

[actionnode] at (6,-3.7) (q5s) ;

(q0) edge node[actiontext] $r_0$ (q0r)
(q0) edge node[actiontext,swap] $d_0$ (q0d)

(q1) edge[in=0,out=150] node[actiontext,swap] $l_1$ (q1l)
(q1) edge[in=90,out=-135] node[actiontext] $d_1$ (q1d)
(q1) edge[out=30,in=180] node[actiontext] $r_1$ (q1r)

(q2) edge node[actiontext,swap] $l_2$ (q2l)
(q2) edge node[actiontext] $d_2$ (q2d)

(q3) edge[out=-60,in=0] node[actiontext] $s_3$ (q3s)

(q4) edge node[actiontext] $l_4$ (q4l)
(q4) edge[in=-90,out=45] node[actiontext] $u_4$ (q4u)
(q4) edge node[actiontext,swap] $r_4$ (q4r)

(q5) edge[out=-60,in=0] node[actiontext] $s_5$ (q5s)

(q0r) edge[sloped,in=180,out=45] node[anchor=south,probtext] $[0.1,0.5]$ (q1)
(q0r) edge[sloped] node[anchor=north,probtext] $[0.3,0.6]$ (q4)
(q0r) edge[sloped,in=90,out=225,pos=0.4] node[anchor=north,probtext] $[0.3,0.6]$ (q3)

(q0d) edge[thick,dashed] node[probtext]  (q3)

(q1l) edge[out=180,in=30,thick,dashed] node[probtext]  (q0)

(q1r) edge[out=0,in=150,thick,dashed] node[probtext]  (q2)

(q1d) edge[out=-90,in=135,thick,dashed] node[probtext]  (q4)

(q2l) edge[sloped,in=0,out=135] node[anchor=south,probtext] $[0.1,0.5]$ (q1)
(q2l) edge[sloped] node[anchor=north,probtext] $[0.3,0.6]$ (q4)
(q2l) edge[sloped,in=90,out=315,pos=0.4] node[anchor=north,probtext] $[0.3,0.6]$ (q5)

(q2d) edge[thick,dashed] node[probtext]  (q5)

(q3s) edge[out=-180,in=-120,thick,dashed] node[probtext]  (q3)

(q4l) edge[thick,dashed] node[probtext]  (q3)

(q4u) edge[out=100,in=90,sloped,pos=0.6,looseness=1.5] node[anchor=south,probtext] $[0.4,1.0]$ (q4)
(q4u) edge[out=90,in=-45,sloped] node[anchor=south,probtext] $[0.0,0.6]$ (q1)

(q4r) edge[thick,dashed] node[probtext]  (q5)

(q5s) edge[out=-180,in=-120,thick,dashed] node[probtext]  (q5)

[anchor=west] at (-0.5,-4.25) $\RabinAcc_1 = \{ \rabinpair{ \colorchar{red} }{ \colorchar{green} } \}$;
[anchor=east] at (6.5,-4.25) $\RabinAcc_2 = \{ \rabinpair{ \emptyset }{ \colorchar{green} }, \rabinpair{ \colorchar{red}\colorchar{green} }{ \colorchar{white} } \}$;

[]Graphic representation of our extension of the case study from [15].
A robot navigates through a grid of six states according to the BMDP, using the actions up, down, left, and right, where enabled.
For readability, all $[1.0, 1.0]$ constraints are omitted and the corresponding edges are drawn dashed.
In our analysis, we consider two different acceptance conditions $\RabinAcc_1$ and $\RabinAcc_2$.

We extend the case study from [15], where an agent moves on a coloured grid of six states.
We added several actions in each state, modelling a robot which navigates the grid as depicted in <ref>.
It can choose between going down, up, left or right; it cannot leave the grid, e.g., in $q_0$ only down and right are available.
The robot is pulled towards the red states $q_3$ and $q_5$, e.g. when moving right from $q_0$ there is some chance to be pulled down onto $q_4$ or even $q_3$.
The strength of the pulling force and hence also the probability distribution over the successor states is unknown and hence modelled by uncertainty intervals.

As a first example, we calculate the probability to reach state $q_2$ starting from $q_0$.
From $q_1$ we can surely reach $q_2$ and from $q_3$ and $q_5$ there is no possibility of reaching $q_2$.
From $q_4$, it depends on the instantiation of the BMDP.
The probability to remain in $q_4$ may equal $1$, preventing the robot from reaching $q_2$ when it is in $q_4$.
On the other hand, we might have $\mdpTransitions(q_4, u_4, q_1) = 0.6$ and $q_1$ can almost surely be reached from $q_4$.
Consequently, $q_2$ can be reached from $q_4$ with probability $1$.
Finally, the best strategy in $q_0$ is to go right, as otherwise the robot is immediately stuck in $q_3$.
Together, this gives us a lower bound of $0.1$ and an upper bound of $0.7$.

Results for the BMDP in <ref>

$\problower$     $\probupper$

$\RabinAcc_1$     $0.0$     $0.7$

$\RabinAcc_2$     $0.4$     $0.7$

Now we consider the properties from [15], adjusted to our setting as depicted in <ref>.
The resulting probabilities are given in <ref> and explained below.

$\RabinAcc_1$ corresponds to The agent visits a green state infinitely often while visiting red states finitely often.
In the antagonistic interpretation, the probability of satisfying this property is zero, since there is no MEC containing $q_1$.
Intuitively, actions $r_0$, $d_1$ and $l_2$ all have a positive probability of moving to the bottom row, where we may be forced to remain forever.

For the upper bound, observe that by setting $\mdpTransitions(q_4, u_4, q_1) = 0.6$ we obtain the winning MEC $(\{q_1,q_4\}, \{d_1,u_4\})$, which can be reached with probability $0.7$.

$\RabinAcc_2$ corresponds to The agent visits a red state infinitely often only if it visits a green state infinitely often.
Observe that in this case both $q_4$ and $q_1$ are winning in any consistent MDP, as playing actions $d_1$ and $u_4$ always leads to a winning path.
In contrast to $\RabinAcc_1$, remaining in $q_4$ is winning by the second pair of $\RabinAcc_2$, since only white states are visited.
We thus get a lower and upper bound of $0.4$ and $0.7$, respectively, by computing the probability to reach $q_1$ or $q_4$.

§ CONCLUSION

We have presented a solution to the open problem of bounding the probabilities to satisfy an $\omega$-regular property on a bounded-parameter Markov systems.
A different perspective on previous approaches enabled us to solve the problem by analysis of $\omega$-regular stochastic games.

Future work includes applications of our approach to more general settings such as MDPIP, as well as a practical implementation.
For the latter, we plan to apply approaches based on learning and real-time dynamic programming, see e.g. [17].

[1]
Christel Baier and Joost-Pieter Katoen.
Principles of model checking.
MIT Press, 2008.

[2]
Anicet Bart, Benoît Delahaye, Didier Lime, Eric Monfroy, and Charlotte
Reachability in parametric interval markov chains using constraints.
In QEST, pages 173–189, 2017.

[3]
Michael Benedikt, Rastislav Lenhardt, and James Worrell.
LTL model checking of interval markov chains.
In TACAS, pages 32–46, 2013.

[4]
Olivier Buffet.
Reachability analysis for uncertain ssps.
In ICTAI, pages 515–522, 2005.

[5]
Souymodip Chakraborty and Joost-Pieter Katoen.
Model checking of open interval markov chains.
In ASMTA, pages 30–42, 2015.

[6]
Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretínský.
Automata with generalized rabin pairs for probabilistic model
checking and LTL synthesis.
In CAV, volume 8044 of LNCS, pages 559–575.
Springer, 2013.

[7]
Krishnendu Chatterjee and Thomas A. Henzinger.
Strategy improvement for stochastic rabin and streett games.
In CONCUR, volume 4137 of LNCS, pages 375–389.
Springer, 2006.

[8]
Krishnendu Chatterjee and Thomas A. Henzinger.
A survey of stochastic \(\omega\)-regular games.
J. Comput. Syst. Sci., 78(2):394–413, 2012.

[9]
Krishnendu Chatterjee, Koushik Sen, and Thomas A. Henzinger.
Model-checking omega-regular properties of interval markov chains.
In FOSSACS, pages 302–317, 2008.

[10]
Taolue Chen, Tingting Han, and Marta Z. Kwiatkowska.
On the complexity of model checking interval-valued discrete time
markov chains.
Inf. Process. Lett., 113(7):210–216, 2013.

[11]
Ventsislav Chonev.
Reachability in augmented interval markov chains.
CoRR, abs/1701.02996, 2017.

[12]
Anne Condon.
The complexity of stochastic games.
Inf. Comput., 96(2):203–224, 1992.

[13]
Costas Courcoubetis and Mihalis Yannakakis.
The complexity of probabilistic verification.
Journal of the ACM, 42(4):857–907, July 1995.

[14]
Benoît Delahaye, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, and
Andrzej Wasowski.
Decision problems for interval markov chains.
In Language and Automata Theory and Applications - 5th
International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011.
Proceedings, pages 274–285, 2011.

[15]
Maxence Dutreix and Samuel Coogan.
Satisfiability bounds for co-regular properties in interval-valued
markov chains.
In CDC, pages 1047–1052, 2018.

[16]
Javier Esparza, Jan Kretínský, and Salomon Sickert.
One theorem to rule them all: A unified translation of LTL into
\(\omega\)-automata.
In LICS, pages 384–393. ACM, 2018.

[17]
Fernando L. Fussuma, Karina Valdivia Delgado, and Leliane Nunes de Barros.
B$^2$rtdp: An efficient solution for bounded-parameter markov
decision process.
In BRACIS, pages 128–133, 2014.

[18]
Robert Givan, Sonia M. Leach, and Thomas L. Dean.
Bounded-parameter markov decision processes.
Artif. Intell., 122(1-2):71–109, 2000.

[19]
Serge Haddad and Benjamin Monmege.
Interval iteration algorithm for MDPs and IMDPs.
Theor. Comput. Sci., 735:111–131, 2018.

[20]
Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, and
Andrea Turrini.
Multi-objective robust strategy synthesis for interval markov
decision processes.
In QEST, pages 207–223, 2017.

[21]
Vahid Hashemi, Holger Hermanns, and Andrea Turrini.
Compositional reasoning for interval markov decision processes.
CoRR, abs/1607.08484, 2016.

[22]
Cyrille Jégourel, Jingyi Wang, and Jun Sun.
Importance sampling of interval markov chains.
In DSN, pages 303–313, 2018.

[23]
Bengt Jonsson and Kim Guldstrand Larsen.
Specification and refinement of probabilistic processes.
In LICS, pages 266–277, 1991.

[24]
Suresh Kalyanasundaram, Edwin KP Chong, and Ness B Shroff.
Markov decision processes with uncertain transition rates:
Sensitivity and robust control.
In CDC, volume 4, pages 3799–3804. IEEE, 2002.

[25]
M. Kloetzer and C. Belta.
A fully automated framework for control of linear systems from
temporal logic specifications.
IEEE Trans. Automat. Contr., 53(1):287–297, Feb 2008.

[26]
Igor Kozine and Lev V. Utkin.
Interval-valued finite markov chains.
Reliable Computing, 8(2):97–113, 2002.

[27]
Jan Kretínský, Tobias Meggendorfer, Salomon Sickert, and
Christopher Ziegler.
Rabinizer 4: From LTL to your favourite deterministic automaton.
In CAV (1), volume 10981 of LNCS, pages 567–577.
Springer, 2018.

[28]
VP Kuznetsov.
Interval methods for processing statistical characteristics.
In Proceedings of the 1995 International Workshop on
Applications of Interval Computations, El Paso, TX, 1995.

[29]
Morteza Lahijanian, Sean B. Andersson, and Calin Belta.
Formal verification and synthesis for discrete-time stochastic
IEEE Trans. Automat. Contr., 60(8):2031–2045, 2015.

[30]
Arnab Nilim and Laurent El Ghaoui.
Robust control of markov decision processes with uncertain transition
Operations Research, 53(5):780–798, 2005.

[31]
Amir Pnueli.
The temporal logic of programs.
In FOCS, pages 46–57. IEEE Computer Society, 1977.

[32]
Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, and
Sanjit A. Seshia.
Polynomial-time verification of PCTL properties of MDPs with
convex uncertainties.
In CAV, pages 527–542, 2013.

[33]
Martin L. Puterman.
Markov Decision Processes: Discrete Stochastic Dynamic
John Wiley & Sons, Inc., New York, NY, USA, 1st edition, 1994.

[34]
Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M. Murray,
Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia.
Model predictive control with signal temporal logic specifications.
In CDC, pages 81–87. IEEE, 2014.

[35]
Willy Arthur Silva Reis, Leliane Nunes de Barros, and Karina Valdivia Delgado.
Robust topological policy iteration for infinite horizon bounded
markov decision processes.
Int. J. Approx. Reasoning, 105:287–304, 2019.

[36]
Jay K. Satia and Roy E. Lave Jr.
Markovian decision processes with uncertain transition probabilities.
Operations Research, 21(3):728–740, 1973.

[37]
Koushik Sen, Mahesh Viswanathan, and Gul Agha.
Model-checking markov chains in the presence of uncertainties.
In TACAS, pages 394–410, 2006.

[38]
Ambuj Tewari and Peter L. Bartlett.
Bounded parameter markov decision processes with average reward
In COLT, pages 263–277, 2007.

[39]
J. G. THISTLE and W. M. WONHAM.
Control problems in a temporal logic framework.
International Journal of Control, 44(4):943–976, 1986.

[40]
Wolfgang Thomas.
Languages, automata, and logic.
In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of
Formal Languages, Volume 3: Beyond Words., pages 389–455. Springer, 1997.

[41]
Peter Walley.
Statistical reasoning with imprecise probabilities.

[42]
Peter Walley.
Measures of uncertainty in expert systems.
Artificial intelligence, 83(1):1–58, 1996.

[43]
Eric M. Wolff, Ufuk Topcu, and Richard M. Murray.
Robust control of uncertain markov decision processes with temporal
logic specifications.
In CDC, pages 3372–3379, 2012.

[44]
Tichakorn Wongpiromsarn, Ufuk Topcu, and Richard M. Murray.
Receding horizon control for temporal logic specifications.
In HSCC, pages 101–110. ACM, 2010.

[45]
Di Wu and Xenofon D. Koutsoukos.
Reachability analysis of uncertain systems using bounded-parameter
markov decision processes.
Artif. Intell., 172(8-9):945–954, 2008.

[46]
B. Yordanov, J. Tumova, I. Cerna, J. Barnat, and C. Belta.
Temporal logic control of discrete-time piecewise affine systems.
IEEE Transactions on Automatic Control, 57(6):1491–1504, June

§ APPENDIX – THE PRODUCT CONSTRUCTION

In this section, we briefly explain how linear objectives usually are specified and how they are model checked using the product construction.
First, we define the concept of $\omega$-regular languages and automata.
Fix a finite alphabet $\Alphabet$.
Elements of $\Alphabet^\omega$ are called words and sets of words $\Language \subseteq \Alphabet^\omega$ are called languages.
Such a language is $\omega$-regular if it can be recognized by an automaton.

§.§ Automata & regular languages

A deterministic Rabin automaton (DRA) is a tuple $\automaton = (\automatonStates, \automatonTransitions, \automatonInitialState, \RabinAcc)$, where
$\automatonStates$ is a finite set of states,

$\automatonTransitions : \automatonStates \times \Alphabet \to \automatonStates$ is a transition function[Recall that the alphabet $\Alphabet$ is already fixed.],
$\automatonInitialState \in \automatonStates$ is an initial state, and
$\RabinAcc \subseteq 2^\automatonStates \times 2^\automatonStates$ is the Rabin condition.
An element $(\RabinFin_i, \RabinInf_i) \in \RabinAcc$ is called Rabin pair.
We assume w.l.o.g. that $\RabinFin_i \intersection \RabinInf_i = \emptyset$.

Let $\automaton$ be a DRA and $w \in \Alphabet^\omega$ a word.
A word $w$ induces a run, i.e. a sequence of states $\automaton(w) = \automatonInitialState q_1 q_2 \cdots \in \automatonStates^\omega$, where $q_{i+1} = \automatonTransitions(q_i, w_i)$.
As with MDP, let $\Inf(w)$ denote the set of states occurring infinitely often on the run $\automaton(w)$.
A word is accepted by the automaton, denoted $w \accepted \automaton$, if there exists a Rabin pair $(\RabinFin_i, \RabinInf_i) \in \RabinAcc$ with $\RabinFin_i \intersection \Inf(w) = \emptyset$ and $\RabinInf_i \intersection \Inf(w) \neq \emptyset$.
Such a Rabin pair is called accepting for $w$.

[auto,initial text=]
[automatonstate,initial above] at (0,0) (s0) $s_0$;
[automatonstate] at (2,0) (s1) $s_1$;

(s0) edge[loop left] node $z$ (s0)
(s0) edge[bend left] node $x, y$ (s1)
(s1) edge[loop right] node $y$ (s1)
(s1) edge[bend left] node $x, z$ (s0)

[]Example DRA with acceptance $\RabinAcc = \{\rabinpair{s_0}{s_1}, \rabinpair{s_1}{s_0}\}$.

A language $\Language \subseteq \Alphabet^\omega$ is called $\omega$-regular if and only if there exists a DRA $\automaton$ recognizing $\Language$, i.e. some word $w \in \Alphabet^\omega$ is accepted by the automaton if and only if it is in $\Language$.
See <ref> for an example of a DRA recognizing the language eventually only $y$ or eventually only $z$.

A wide variety of specifications are $\omega$-regular.
For example, reachability and liveness constraints can easily be translated to an automaton.
Moreover, the whole of linear temporal logic is expressible through Rabin automata and efficient translations from LTL to Rabin automata exist [16].

§.§ Labelled MDPs & product

For the product construction, we modify the definition of MDPs by replacing the acceptance by a labelling function $\labelling : \States \to \Alphabet$, assigning to each state of the MDP a letter.
We are given such a labelled MDP and a Rabin automaton.
We construct the product by tracking both the evolution of the MDP and the automaton, where the automaton progresses based on the letter assigned to the current state.

Let $\MDP = (\States, \initialstate, \Actions, \stateactions, \mdpTransitions, \labelling)$ be a labelled MDP and $\automaton = (\automatonStates, \automatonTransitions, \automatonInitialState, \RabinAcc)$ a Rabin automaton.
The product $\MDP \otimes \automaton = (\States \times \automatonStates, (\initialstate, \automatonInitialState), \Actions, \stateactions', \mdpTransitions', \RabinAcc')$ is an MDP where
$\stateactions'((s, q)) := \stateactions(s)$,
$\mdpTransitions((s, q), a, (s', q')) := \mdpTransitions(s, a, s')$ if $q' = \automatonTransitions(q, \labelling(s))$ and $0$ otherwise, and
$\RabinAcc' = \{(\RabinFin_i \times \States, \RabinInf_i \times \States) \mid (\RabinFin_i, \RabinInf_i) \in \RabinAcc\}$.

We analogously define this product construction for BMDP.
Observe that the product is now of the form as we defined it in <ref>.
Applying our methods to this product yields a solution for the original system.

§.§ Caveat

[][Example DRA with acceptance $\RabinAcc = \{\rabinpair{q_2}{q_0, q_1}\}$]
[auto,initial text=]
[automatonstate,initial left] at (0,0) (q0) $q_0$;
[automatonstate] at (2,0) (q1) $q_1$;
[automatonstate] at (4,0) (q2) $q_2$;
[automatonstate] at (6,0) (q3) $q_3$;
[automatonstate] at (3,-1.5) (e) $q_4$;

(q0) edge node $x$ (q1)
(q1) edge node $y$ (q2)
(q2) edge node $x$ (q3)
(q3) edge[bend right,swap] node $z$ (q0)

(q0) edge[sloped,anchor=north] node $y, z$ (e)
(q1) edge[sloped,anchor=south] node $x, z$ (e)
(q2) edge[sloped,anchor=south] node $y, z$ (e)
(q3) edge[sloped,anchor=north] node $x, y$ (e)

(e) edge[loop left] node $x, y, z$ (e)

[Example IMC.]
[auto,initial text=]
[state,initial above] at (0,0) (s0) $s_0, x$;
[state] at (2,0) (sr) $s_2, z$;
[state] at (-2,0) (sl) $s_1, y$;

(s0) edge[bend left] node[probtext] $[0.0, 1.0]$ (sr)
(s0) edge[bend left] node[probtext] $[0.0, 1.0]$ (sl)
(sl) edge[bend left] node[probtext] $[1.0, 1.0]$ (s0)
(sr) edge[bend left] node[probtext] $[1.0, 1.0]$ (s0)

Uncertain/adversarial interval interpretations are not equal.

Since this construction modifies the state space, it is not obvious how optimal policies on the product relate to policies on the original MDP.
Indeed, while a memoryless policy may be optimal on the product, it might be the case that finite memory is needed to behave optimally in the given system.
Moreover, it is the case that for $\omega$-regular objectives, the optimal values for the uncertainty and the antagonistic interpretation are not equal already for IMCs.

Fix the alphabet $\Alphabet = \{x, y, z\}$ and consider the language $\Language = \{(xyxz)^\omega\}$, i.e. a language containing a single word $w$ which repeats the string $xyxz$ indefinitely.
This language is regular and is recognized by the automaton shown in <ref>.
Consider now the IMC in <ref>.
Clearly, the probability of satisfying the property is zero under the uncertainty interpretation – any MC consistent with the IMC eventually violates the structure of the property with probability $1$.
On the other hand, interpreted as an IMDP, the transitions can be chosen such that the required word is always produced.


#  There and back again:
Solar cycle effects in future measurements of low-energy atmospheric neutrinos

Kevin J. Kelly<EMAIL_ADDRESS>Theoretical Physics Department, CERN,
Esplande des Particules, 1211 Geneva 23, Switzerland  Department of Physics
and Astronomy, Mitchell Institute for Fundamental Physics and Astronomy, Texas
A&M University, College Station, TX 77843, USA  Pedro A. N. Machado
<EMAIL_ADDRESS>Theoretical Physics Department, Fermilab, P.O. Box 500,
Batavia, IL 60510, USA  Nityasa Mishra<EMAIL_ADDRESS>Department of
Physics and Astronomy, Mitchell Institute for Fundamental Physics and
Astronomy, Texas A&M University, College Station, TX 77843, USA  Louis E.
Strigari<EMAIL_ADDRESS>Department of Physics and Astronomy, Mitchell
Institute for Fundamental Physics and Astronomy, Texas A&M University, College
Station, TX 77843, USA  Yi Zhuang<EMAIL_ADDRESS>Department of Physics and
Astronomy, Mitchell Institute for Fundamental Physics and Astronomy, Texas A&M
University, College Station, TX 77843, USA

###### Abstract

We study the impact of time-dependent solar cycles in the atmospheric neutrino
rate at DUNE and Hyper-Kamiokande (HK), focusing in particular on the flux
below 1 GeV. Including the effect of neutrino oscillations for the upward-
going component that travels through the Earth, we find that across the solar
cycle the amplitude of time variation is about $\pm 5\%$ at DUNE, and $\pm
1\%$ at HK. At DUNE, the ratio of up/down-going events ranges from $0.45$ to
$0.85$, while at HK, it ranges from $0.75$ to $1.5$. Over the 11-year solar
cycle, we find that the estimated statistical significance for observing time
modulation of atmospheric neutrinos is $4.8\sigma$ for DUNE and $2.0\sigma$
for HK. Flux measurements at both DUNE and HK will be important for
understanding systematics in the low-energy atmospheric flux as well as for
understanding the effect of oscillations in low-energy atmospheric neutrinos.

††preprint: FERMILAB-PUB-23-143-T, CERN-TH-2023-056, MI-HEE-800

##  I Introduction

While one of the oldest sources of neutrinos studied in high energy physics,
atmospheric neutrinos continue to be an active area of research, significantly
contributing to the determination of oscillation parameters Super-
Kamiokande:1998kpq ; Super-Kamiokande:2010orq ; Super-Kamiokande:2005mbp ;
Super-Kamiokande:2015qek ; Super-Kamiokande:2017yvm ; IceCube:2017lak ; Super-
Kamiokande:2019gzr . Atmospheric neutrinos are produced when cosmic rays (CRs)
collide with the Earth’s atmosphere, resulting in the production of charged
mesons which, through a series of decays, ultimately leading to a large flux
of electron, muon, and even tau neutrinos. The neutrinos are produced ranging
from sub-MeV to greater than PeV energies, and have been studied by many
experiments Gaisser:2002jj .

The lowest energy component of the atmospheric neutrino flux arises from CR
with energies of $\lesssim 10$ GeV, see Fig. 1. At these energies, two
distinct physical mechanisms affect the CR flux at Earth. First, CRs diffuse
through the solar wind (Gleeson:1968zza, ), so there is an expected modulation
from the solar cycle Potgieter:2013pdj . This CR modulation due to solar
activity has been measured by PAMELA Marcelli:2020uqv  and BESS Abe:2015mga .
The Super-Kamiokande (SK) experiment searched for such a correlation in the
atmospheric neutrino flux over 20-year-long periods, but reported a detection
with a statistical significance of only 1.1$\sigma$ Super-Kamiokande:2015qek .
One of the challenges in measuring this effect is that it is largest at low
energies, particularly below the GeV scale, and it depends on the incoming
direction of the neutrinos. Reconstructing energy and direction of sub-GeV
atmospheric neutrinos is a challenge for large Cherenkov detectors since low
energy protons do not emit Cherenkov light.

A second mechanism that affects the low-energy atmospheric neutrino flux is
the rigidity (momentum/charge) cutoff which results from the geomagnetic
field. This rigidity cutoff is different for each location on Earth, so that
the low-energy CR spectrum is different for different locations on Earth. This
cut-off ultimately induces an asymmetry in the low-energy atmospheric flux
Lipari:2000du . This effect has also been studied by SK Super-
Kamiokande:2015qek , which identified an east-west asymmetry due to the
geomagnetic field.

Figure 1: Cosmic ray protons producing neutrinos $E_{\nu}>100$ MeV. For each
spectrum (latitudes indicated), the shaded band represents the differences
between solar min and solar max.

The next generation of neutrino experiments will provide improved sensitivity
to low-energy atmospheric neutrinos, allowing for better estimates of the
solar modulation and geomagnetic field effects. The Deep Underground Neutrino
Experiment (DUNE) DUNE:2020ypp , which uses liquid argon time projection
chamber technology, is expected to measure sub-GeV atmospheric neutrinos and
provide unparalleled reconstruction of both energy and direction of this
sample Kelly:2021jfs . The Hyper-Kamiokande (HK) experiment Hyper-
Kamiokande:2018ofw , a massive 200 kton water detector that is ten times
larger than SK, is expected to have a large statistical sample that is
sensitive to even percent-level time modulations of the atmospheric neutrino
flux. The Jiangmen Underground Neutrino Observatory (JUNO) JUNO:2021vlw , a 20
kton liquid scintillator experiment designed to measure reactor neutrinos, is
also expected to contribute to the observation of various other sources of
neutrinos, including the sun, the atmosphere, and (along with DUNE and HK) the
diffuse background of supernova neutrinos Moller:2018kpn . In addition to the
above dedicated neutrino experiments, a future large scale dark matter
detector will be somewhat sensitive to low energy atmospheric neutrinos
Aalbers:2022dzr .

In this paper, we examine the correlation between solar magnetic activity and
the atmospheric neutrino flux, and the prospects for measuring this
correlation at the aforementioned experiments. Despite being relatively well
understood in theory, this effect has yet to be observed in neutrino
experiments. We estimate the sensitivity of experiments to the correlation
between solar magnetic activity and atmospheric neutrino flux using
simulations of the atmospheric neutrino flux and detector responses in an
event-by-event basis. By examining how the nature of the signal changes at
different locations, we show that a measurement at both DUNE and HK is
necessary to best understand the systematic uncertainties in the flux.

##  II Low-Energy Atmospheric Neutrino Flux

To calculate the low-energy atmospheric neutrino flux spectrum from the
interactions of CRs, we follow the method of Ref. Zhuang:2021rsg . In Fig. 2,
we show the $\nu_{e}$ and $\nu_{\mu}$ fluxes at HK and DUNE for upgoing and
downgoing neutrinos at the extrema of the solar cycles. In the following, we
highlight relevant aspects of the calculation, and refer to Ref.
Zhuang:2021rsg  for further details on the simulations. We start from the
CORSIKA code Wentz:2003bp , which generates neutrinos from simulations of CR
interactions and the subsequent air showers. Within CORSIKA, we use the FLUKA
model to simulate low energy events, $<$ 80 GeV, and QGSJET 01C for higher
energy events. For the input CR spectrum, we use the updated measurements of
the CR spectrum on Earth at the different phases of the Solar cycle
Marcelli:2020uqv ; Abe:2015mga .

We consider the detection prospects of the low-energy atmospheric neutrino
flux at two future, large neutrino detectors that will be coming online with
particular strengths (and complementarity). DUNE DUNE:2020ypp  which is at a
latitude ${\sim}44^{\circ}$ N and has a goal of 40 kt liquid argon fiducial
mass, can detect charged-current electron-neutrino scattering down to
$\mathcal{O}$(tens) of MeV thanks to its liquid argon time-projection-chamber
technology, as well as charged-current muon-neutrino scattering above the
$\mu^{\pm}$ production threshold. Hyper-Kamiokande Hyper-Kamiokande:2018ofw ,
which is at latitude ${\sim}36^{\circ}$ N, offers a significantly larger
detector volume (of water), however due to Cerenkov thresholds of charged
particles, its low-energy capabilities are relatively weaker than that of
DUNE. Though our primary analysis will be presented for DUNE and HK, we also
compare to the prospects for JUNO JUNO:2021vlw , which is at latitude
${\sim}22^{\circ}$ N, and will be able to detect low-energy $\bar{\nu}_{e}$
events via inverse-beta-decay scattering in its liquid scintillator.

At any location on Earth, the neutrino flux is a sum of a downward-going
component, $0<\cos\theta_{z}<1$, and an upward-going component,
$-1<\cos\theta_{z}<0$, where $\theta_{z}$ is the zenith angle. The downgoing
flux may be estimated from interactions of neutrinos in the atmosphere above
the horizon. On the other hand, the upward flux requires information on the
rigidity cutoff at all positions for all directions below the horizon. For
this reason, estimating the upward-going flux presents a more substantial
computational challenge. We therefore explicitly divide our simulations up
into the downward and the upward flux components, and estimate the integrated
neutrino fluxes over all angles for both directions.

Figure 2: Electron-neutrino (left) and muon-neutrino (right) fluxes at the
Hyper-Kamiokande (top) and DUNE (bottom) detectors at the extrema of the solar
cycle: solar max. in blue and min. in orange. We divide the fluxes into the
down-going (dashed lines) and up-going (solid bands, driven by uncertainty in
neutrino oscillation parameters) components.

To simulate the upward-going flux for each location, we divide the Earth into
20 zenith and 20 azimuthal patches. These upward-going samples are divided by
different $\cos\theta_{z}$ and energy so that the effects of neutrino
oscillations, as described below, may be properly included – our end result is
the direction-integrated upward-going neutrino flux of each relevant neutrino
flavor, $\nu_{e}$, $\bar{\nu}_{e}$, $\nu_{\mu}$, and $\bar{\nu}_{\mu}$. To
check our differential fluxes as a function of zenith angle, for a fixed
zenith angle we integrate over azumith, and ensure that the flux smoothly
matches the fluxes from previous calculations at a zenith angle of
$\cos\theta_{z}=0.5$ Honda:2015fha  for neutrino energies $>1$ GeV.

Upward-going neutrinos additionally experience matter-induced oscillations as
they travel through the Earth. We calculate the oscillation probabilities for
$-1\leq\cos\theta_{z}\leq 1$ and $100$ MeV $\leq E_{\nu}\leq 1$ GeV, assuming
the PREM Earth Density Model Dziewonski:1981xy . Previously, it has been
demonstrated that measurements of these oscillations can provide additional,
complementary information on leptonic CP-violation, specifically at DUNE
Kelly:2019itm . We additionally allow the six oscillation parameters to vary
assuming current knowledge of their values111Specifically,
$\sin^{2}\theta_{12}$, $\sin^{2}\theta_{13}$, and $\Delta m_{21}^{2}$ are
drawn from their assumed-Gaussian distributions, and $\sin^{2}\theta_{23}$,
$\Delta m_{31}^{2}$, and $\delta_{\rm CP}$ are drawn with weights according to
the $\chi^{2}$ table (including Super-Kamiokande atmospheric data) provided
from Ref. nufit  to include proper parameter correlations. from Ref.
Esteban:2020cvm . Note that we focus on the current knowledge of oscillation
parameters because, while DUNE and HK will greatly improve these measurements
with beam neutrinos and JUNO with reactor ones, it will still be invaluable to
perform independent measurements with atmospheric neutrinos. We find that
varying $\sin^{2}\theta_{23}$ and $\delta_{\rm CP}$ according to present-day
uncertainty leads to the greatest variance in expected upward-going fluxes.

The time variation of the flux is manifest when examining the spectrum of CR
protons that produce low-energy, $>100$ MeV neutrinos at each detector
location. These spectra are shown in Figure 1. As is apparent, DUNE is more
sensitive to lower-energy CRs than any other detector, sampling CRs down to
the limit of our calculation of ${\sim}2$ GeV CR kinetic energy. For
comparison, the CR spectra at HK and at JUNO cut off at higher energies,
${\sim}6$ and ${\sim}9$ GeV, respectively. Because of this lower energy cut-
off, there is a larger variation in the CR proton flux in one solar cycle at
DUNE.

The corresponding low-energy neutrino fluxes are shown in Figure 2, for DUNE
and HK. Analogous fluxes for antineutrinos are presented in the appendix. The
first interesting point to note from Figure 2 is that the upward-going fluxes
at HK and DUNE are very similar. This is because the upgoing flux is
integrated over a wide range of angular directions, so that the rigidity
information in the CR spectrum is in essence averaged out. By similar
reasoning, the impact of oscillations is similar for the DUNE and HK fluxes
(the thickness of the colored bands indicate $\pm 1/2/3\sigma$ uncertainty of
the upward-going fluxes due to oscillation parameter uncertainty). The
situation is different, however, for the downgoing fluxes. In comparison to
the results from DUNE, the fluxes at HK are lower and have less variation when
comparing the Solar cycle maximum and minimum.

A second interesting feature to note from Figure 2 is the relationship between
the upward-to-downward going fluxes at each location. Given the nature of the
magnetic field nearer to the poles, the rigidity cut-off for CRs at DUNE’s
Homestake Mine location is lower than it is for detectors closer to the
equator such as Kamioka. This implies that the downgoing neutrino flux at
Homestake at low energy is larger than it is for HK, which results from the CR
spectrum show in Figure 1. However, for the upward going flux, the situation
changes. Since Kamioka is on the opposite hemisphere relative to the South
Atlantic Anomaly, which is a region defined by a low rigidity cutoff, at this
location the upward going flux is larger than the downgoing flux. On the other
hand, at the Homestake location, the downward going flux is larger, since on
average the upward flux arises from regions of higher rigidity. Since the
upward/downward-going ratio is different for each location, a flux measurement
at both locations is crucial for understanding the systematics that arise due
to the solar modulation and the geomagnetic field.

Figure 3: Event rates per year at HK (top) and DUNE (bottom) for $\mu^{\pm}$
(purple) and $e^{\pm}$ (green) event signatures. Up-going and down-going event
rates are added for simplicity.

##  III Measurement Capabilities

Figure 4: Ratio of up-going events to down-going ones in HK (left) and DUNE
(right) over the course of one solar cycle – the top (bottom) panels
demonstrate this ratio for $e^{\pm}$ ($\mu^{\pm}$) events. In each panel, the
dark/medium/light shaded regions are the $\pm 1/2/3\sigma$ allowed regions of
this prediction when we vary oscillation parameters consistent with current
measurements Esteban:2020cvm , and the thick, solid line is the median
expectation. The predicted solar-cycle dependence is highly correlated once a
given set of oscillation parameters is assumed to be true.

We now move on to estimating the prospects for measurement of the time
variation of the atmospheric neutrino flux at DUNE and HK.222We have also
determined these charged-current scattering rates for low-energy neutrinos at
JUNO and find that they are too small to be meaningfully measured to the same
level as at DUNE and HK, consistent with the findings of Ref. JUNO:2021vlw .
We use the NuWro Golan:2012rfa ; Golan:2012wx  Monte Carlo event generator to
determine charged-current-inclusive scattering cross sections of the different
neutrino flavors on the different detector targets at these low energies and
in turn, the expected event rate in a given time period. For simplicity, we
first consider the total $e^{\pm}$ and $\mu^{\pm}$ event rates (assuming no
particle mis-identification and no charge identification) during one complete
solar cycle at DUNE with a 40 kt fiducial detector volume and HK with a 217 kt
one. The expected event rates for $E_{\nu}<1$ GeV are displayed in Fig. 3 for
$e^{\pm}$ (green) and $\mu^{\pm}$ (purple), where we take the median expected
event rate subject to neutrino oscillation uncertainties and provide
statistical error bars. The fact that these rates are not constant with
respect to time is readily apparent – for a 40 kt detector, DUNE can, in
principle, detect this modulation in the $e^{\pm}$ and $\mu^{\pm}$ samples at
the ${\sim}4.8\sigma$ in one cycle. If DUNE only operates with two modules and
a fiducial volume of 20 kt, this reduces to ${\sim}3.4\sigma$. HK, in
contrast, will only have sensitivity to this modulation at the
${\sim}2.0\sigma$ level due to the smaller fractional modulation of its event
rates, apparent in the top half of Fig. 3. Further challenges exist,
especially for HK, in measuring and reconstructing low-energy $e^{\pm}$ events
due to Cherenkov threholds. Realistic reconstruction of low-energy events will
reduce HK’s sensitivity to the solar cycle.

In comparing the DUNE results presented here with those of Hyper-Kamiokande,
we see that the expected modulation at DUNE is relatively large (a ${\sim}$10%
effect), roughly twice that predicted in HK. However, the larger detection
volume of HK leads to event rates ${\sim}$3 times as large as those in DUNE.
Put together, this means that such modulations should be taken into account
carefully for both experiments when measuring atmospheric neutrinos,
especially as it pertains to oscillation analyses.

There is an additional important issue when performing any analysis of
atmospheric neutrino oscillations with these next-generation detectors that we
highlight: implementing time-dependent fluxes for both upward- and downward-
going neutrino components appropriately. Typically, the data are analyzed
integrated over the entire lifetime of the experiment; if this is done without
consideration of the flux modulation, a biased measurement of oscillation
parameters (notably $\sin^{2}\theta_{23}$ and/or $\delta_{\rm CP}$) may be
extracted from an analysis. Fig. 4 demonstrates this with respect to the ratio
of neutrino-scattering events from the up-going flux to the down-going flux
for $e^{\pm}$ (top) and $\mu^{\pm}$ (bottom). The thick line in each panel
presents the median-expected result when considering the possible values of
neutrino oscillation parameters given current data Esteban:2020cvm , whereas
the shaded regions demonstrate the $\pm 1/2/3\sigma$ range allowed. Especially
focusing on the DUNE panels (right), we see that the up/down ratio will vary
at the several-percent level over one solar cycle. However, a few-percent
change in the up/down event ratio is similarly produced by varying
$\sin^{2}\theta_{23}$ or $\delta_{\rm CP}$ within their current uncertainties.
This difference could result in an extracted atmospheric measurement at DUNE
that is inconsistent with that extracted from DUNE’s long-baseline $\nu_{e}$
appearance measurements, if these effects are not treated carefully. We note
that this is a challenging measurement to perform, given the required
direction reconstruction to separate up-going and down-going events
Kelly:2021jfs , and leave dedicated studies of this and other experimental
features to future work.

It is also important to note that the modulating flux ratios between HK and
DUNE shown in Fig. 4 are out of phase – this is because DUNE sees modulations
most significantly in its down-going neutrino fluxes (see Fig. 2), whereas HK
has nearly constant down-going neutrino fluxes and small variance in the up-
going ones. A combined analysis of DUNE and HK that reveals this out-of-phase
dependence would provide further support for understanding of the CR flux, the
varying rigidity cutoffs, and the modulation due to the solar cycle.

##  IV Discussion & Conclusions

We have demonstrated that the time-variation of low-energy atmospheric
neutrinos at next-generation experiments is a significant effect. This must be
carefully accounted for to yield accurate predictions for neutrino-oscillation
studies, and for them to be competitive with alternate methods of measuring
parameters, such as the CP-violating phase in the lepton sector. This effect
can be measured at DUNE and, to a lesser extent, HK, over the course of 11
years of data collection. The event rates at JUNO will be too small for
meaningful measurements of these effects.

Interestingly, the nature of the modulation is unique at both detectors. DUNE
sees a large modulation in its downward-going flux due to the low rigidity
cutoff at its high latitude, whereas the downward-going flux at HK is fairly
stable at a lower detector latitude. Both detectors, when viewing upward-going
neutrinos, effectively sample the same profile of latitudes and longitudes.
This, combined with the impact of neutrino oscillations in the upward-going
fluxes, results in fairly similar upward-going modulation for both detector
locations. These effects together can predict non-trivial event modulations
for both electron-like and muon-like events, for both upward- and downward-
going neutrinos. The ratio of upward-to-downward-going events is a key
indicator of these effects, and we have highlighted how the out-of-phase
variation of this quantity, as measured by DUNE and Hyper-Kamiokande, is a
clear indicator of the solar cycle modulation. Further, this up-to-down-going
ratio is important for the extraction of neutrino oscillation parameters and
so care is required when performing these upcoming analyses.

We have presented results focused on generator-level information of incoming
neutrinos at these two detector locations. On one hand, reconstructing the
incoming direction of incoming sub-GeV atmospheric neutrinos is a non-trivial
challenge. While LArTPCs may be able to achieve 20-30∘ directional
reconstruction Kelly:2019itm ; Kelly:2021jfs , water Cherenkov detectors have
much worse directional capabilities due to the fact that low energy protons do
not emit Cherenkov light. Determining the feasibility of realistic
measurements of these modulations and up-to-down ratios, as well as more in-
depth statistical measures of these time-variations, is therefore left for
future work.

Nevertheless, measurements of neutrino oscillations will improve between now
and these experiments’ data collections. These measurements will further
inform our understanding of neutrino oscillations, and we have demonstrated
the importance of understanding these modulations when using atmospheric
neutrinos for oscillation measurements. Combined measurements of DUNE and
Hyper-Kamiokande should meaningfully identify such solar-cycle effects and
help for a better understanding of these low-energy cosmic ray fluxes as well.

###### Acknowledgements.

L.S., N.M., and Y.Z. are supported by the DOE Grant No. DE-SC0010813. Fermilab
is managed by the Fermi Research Alliance, LLC (FRA), acting under Contract
No. DE-AC02-07CH11359.

## References

  * (1) Super-Kamiokande collaboration, “Evidence for oscillation of atmospheric neutrinos”, _Phys. Rev. Lett._ 81 (1998) 1562 [hep-ex/9807003].
  * (2) Super-Kamiokande collaboration, “Atmospheric neutrino oscillation analysis with sub-leading effects in Super-Kamiokande I, II, and III”, _Phys. Rev. D_ 81 (2010) 092004 [1002.3471].
  * (3) Super-Kamiokande collaboration, “A Measurement of atmospheric neutrino oscillation parameters by SUPER-KAMIOKANDE I”, _Phys. Rev. D_ 71 (2005) 112005 [hep-ex/0501064].
  * (4) Super-Kamiokande collaboration, “Measurements of the atmospheric neutrino flux by Super-Kamiokande: energy spectra, geomagnetic effects, and solar modulation”, _Phys. Rev. D_ 94 (2016) 052001 [1510.08127].
  * (5) Super-Kamiokande collaboration, “Atmospheric neutrino oscillation analysis with external constraints in Super-Kamiokande I-IV”, _Phys. Rev. D_ 97 (2018) 072001 [1710.09126].
  * (6) IceCube collaboration, “Measurement of Atmospheric Neutrino Oscillations at 6–56 GeV with IceCube DeepCore”, _Phys. Rev. Lett._ 120 (2018) 071801 [1707.07081].
  * (7) Super-Kamiokande collaboration, “Atmospheric Neutrino Oscillation Analysis with Improved Event Reconstruction in Super-Kamiokande IV”, _PTEP_ 2019 (2019) 053F01 [1901.03230].
  * (8) T. K. Gaisser and M. Honda, “Flux of atmospheric neutrinos”, _Ann. Rev. Nucl. Part. Sci._ 52 (2002) 153 [hep-ph/0203272].
  * (9) L. J. Gleeson and W. I. Axford, “Solar Modulation of Galactic Cosmic Rays”, _Astrophys. J._ 154 (1968) 1011.
  * (10) M. Potgieter, “Solar Modulation of Cosmic Rays”, _Living Rev. Solar Phys._ 10 (2013) 3 [1306.4421].
  * (11) N. Marcelli et al., “Time dependence of the flux of helium nuclei in cosmic rays measured by the PAMELA experiment between July 2006 and December 2009”, 2005.08524.
  * (12) K. Abe et al., “Measurements of cosmic-ray proton and helium spectra from the BESS-Polar long-duration balloon flights over Antarctica”, _Astrophys. J._ 822 (2016) 65 [1506.01267].
  * (13) P. Lipari, “The East west effect for atmospheric neutrinos”, _Astropart. Phys._ 14 (2000) 171 [hep-ph/0003013].
  * (14) DUNE collaboration, “Deep Underground Neutrino Experiment (DUNE), Far Detector Technical Design Report, Volume II: DUNE Physics”, 2002.03005.
  * (15) K. J. Kelly, P. A. N. Machado, I. Martinez-Soler and Y. F. Perez-Gonzalez, “DUNE atmospheric neutrinos: Earth tomography”, _JHEP_ 05 (2022) 187 [2110.00003].
  * (16) Hyper-Kamiokande collaboration, “Hyper-Kamiokande Design Report”, 1805.04163.
  * (17) JUNO collaboration, “JUNO physics and detector”, _Prog. Part. Nucl. Phys._ 123 (2022) 103927 [2104.02565].
  * (18) K. Møller, A. M. Suliga, I. Tamborra and P. B. Denton, “Measuring the supernova unknowns at the next-generation neutrino telescopes through the diffuse neutrino background”, _JCAP_ 05 (2018) 066 [1804.03157].
  * (19) J. Aalbers et al., “A next-generation liquid xenon observatory for dark matter and neutrino physics”, _J. Phys. G_ 50 (2023) 013001 [2203.02309].
  * (20) Y. Zhuang, L. E. Strigari and R. F. Lang, “Time variation of the atmospheric neutrino flux at dark matter detectors”, _Phys. Rev. D_ 105 (2022) 043001 [2110.14723].
  * (21) J. Wentz, I. M. Brancus, A. Bercuci, D. Heck, J. Oehlschlager, H. Rebel et al., “Simulation of atmospheric muon and neutrino fluxes with CORSIKA”, _Phys. Rev. D_ 67 (2003) 073020 [hep-ph/0301199].
  * (22) M. Honda, M. Sajjad Athar, T. Kajita, K. Kasahara and S. Midorikawa, “Atmospheric neutrino flux calculation using the NRLMSISE-00 atmospheric model”, _Phys. Rev. D_ 92 (2015) 023004 [1502.03916].
  * (23) A. M. Dziewonski and D. L. Anderson, “Preliminary reference earth model”, _Phys. Earth Planet. Interiors_ 25 (1981) 297.
  * (24) K. J. Kelly, P. A. Machado, I. Martinez Soler, S. J. Parke and Y. F. Perez Gonzalez, “Sub-GeV Atmospheric Neutrinos and CP-Violation in DUNE”, _Phys. Rev. Lett._ 123 (2019) 081801 [1904.02751].
  * (25) I. Esteban, M. Gonzalez-Garcia, M. Maltoni, T. Schwetz and A. Zhou, “NuFit 5.2 (2022) nu-fit.”
  * (26) I. Esteban, M. C. Gonzalez-Garcia, M. Maltoni, T. Schwetz and A. Zhou, “The fate of hints: updated global analysis of three-flavor neutrino oscillations”, _JHEP_ 09 (2020) 178 [2007.14792].
  * (27) T. Golan, J. T. Sobczyk and J. Zmuda, “NuWro: the Wroclaw Monte Carlo Generator of Neutrino Interactions”, _Nucl. Phys. B Proc. Suppl._ 229-232 (2012) 499.
  * (28) T. Golan, C. Juszczak and J. T. Sobczyk, “Final State Interactions Effects in Neutrino-Nucleus Interactions”, _Phys. Rev. C_ 86 (2012) 015505 [1202.4197].

##  Appendix A Upward- and downward-going antineutrino fluxes

For completeness, in Fig. 5, we show the $\overline{\nu}_{e}$ and
$\overline{\nu}_{\mu}$ fluxes at HK and DUNE for upgoing and downgoing
neutrinos at the extrema of the solar cycles.

Figure 5: Electron-antineutrino (left) and muon-antineutrino (right) fluxes at
the Hyper-Kamiokande (top) and DUNE (bottom) detectors at the extrema of the
solar cycle: solar max. in blue and min. in orange. We divide the fluxes into
the down-going (dashed lines) and up-going (solid bands, driven by uncertainty
in neutrino oscillation parameters) components. See text for more detail.