11institutetext: Johannes Kepler University, Linz, Austria
11email<EMAIL_ADDRESS>22institutetext: Heinrich Heine University,
Düsseldorf, Germany
22email<EMAIL_ADDRESS>
# Trace Refinement in B and Event-B††thanks: This research presented in this
paper has been conducted within the IVOIRE project, which is funded by
“Deutsche Forschungsgemeinschaft” (DFG) and the Austrian Science Fund (FWF)
grant # I 4744-N. The work of Austrian authors has been partly funded by the
LIT Secure and Correct Systems Lab sponsored by the province of Upper Austria.

Sebastian Stock  11 Atif Mashkoor  11 Michael Leuschel  22 Alexander Egyed  11

###### Abstract

Traces are used to show whether a model complies with the intended behavior. A
modeler can use trace checking to ensure the preservation of the model
behavior during the refinement process. In this paper, we present a trace
refinement technique and tool called BERT that allows designers to ensure the
behavioral integrity of high-level traces at the concrete level. The proposed
technique is evaluated within the context of the B and Event-B methods on
industrial-strength case studies from the automotive domain.

###### Keywords:

B method Event-B Animation Traces Refinement

##  1 Introduction

In a correct-by-construction model development process, refinement takes
center stage. The idea is to incrementally enrich a model in detail
(horizontal or vertical refinement) while preserving the correctness of
already introduced functionalities and properties. This correctness assurance
process requires both verification and validation. While proof obligations
(POs) [1] can ensure that the model is verifiable, validation obligations
(VOs) [26] can be used to assess the validity of the model.

A trace can ascertain two conditions: 1) a specific end-state is reachable
after executing steps in a specific order, and 2) a specific order of
transitions is feasible. When creating a trace for a model, the designer may
be interested in keeping the specific trace throughout the refinement chain as
evidence that particular behavior is preserved. However, the time invested in
creating the trace may be lost during the refinement process. Furthermore, the
trace may no longer be replayable due to a change in the operations or the
addition of new operations. One could argue that the designer could postpone
validation until the model is concrete or recreate the trace on the refined
machine. However, the first approach is against the spirit of early validation
in the modeling process, while the latter case entails additional work and
complexity.

In this paper, we present a technique and tool called BERT (B and Event-B
Trace Refinement Technique) showing how traces on abstract models can be
refined automatically to replay on later stages of the refinement chain. With
this technique and tool, we aim to make traces transferable between an
abstract and refining machine in the context of B [1], and Event-B [2]. The
ability to transfer traces increases the worth of traces in multiple aspects.
For one, we can assure ourselves of the presence of abstract behavior in the
refinement, which helps us validate the specification. Additionally, we
encourage tracing and the exploration of the model via animation in general.
With BERT, designers can automatically transfer the findings of their
experiments to the next stage of development, i.e., the next refinement step.
This is an aspect of early validation, which is desirable when writing formal
models. However, we aim not to establish a refinement relationship but to
transform a trace from an abstract machine $M_{A}$ to a concrete machine
$M_{C}$. So trace refinement in our context means not establishing a
refinement relationship via traces but refinement of a trace. Trace refinement
enables comfortable early validation of models via trace checking. We choose B
and Event-B as candidate formal methods in this endeavor. The proposed
technique is implemented as an add-on for the animator and model checker ProB
[19]. The proposed technique is validated using industrial-strength case
studies from the automotive domain.

The rest of the paper is structured as follows. Section 2 introduces formal
methods B and Event-B and the tool-set ProB. Section 3 discusses the
relationship between refinement checking and trace refinement and formalizes
the technique of this paper. Section 4 introduces the techniques used for
trace refinement. In Section 5 BERT is evaluated on two mid-size Event-B case
studies. In Section 6 the observations regarding algorithm and case studies
are presented. Section 7 compares the presented technique with the related
work. Finally, Section 8 concludes the paper.

##  2 Formal methods B and Event-B

The B modeling language, and its successor Event-B, shown in Figure 1(a), are
formal methods based on set theory and first-order predicate logic. Although
the methods differ in various ways, as explained by Leuschel [17] and Mashkoor
et al. [25], both promote the correct-by-construction development paradigm.
Designers can describe a machine that behaves like a state automaton with both
languages. In B, so-called operations are used to make transitions between
states, while in Event-B, the transitions are made via events. Both events and
operations manipulate the state of the machine111In the following, events and
operations will be used as interchangeable words.. The events have guards
consisting of predicates checked against the machine’s state. Depending on
whether a guard is met, the transition is enabled. With the events, we can
manipulate variables written in the variables section of the machine. For a
machine, we can also define invariants that constrain the state space and are
also used to define variables.

###  2.1 Refinement

In B and Event-B, refinement is a way to enrich the model by adding new
variables or events or by replacing existing variables with more complex
constructs. The key to refinement is that the concrete model preserves
abstract behavior. Refinement enhances the abilities of a model without
violating its properties.

In classical B, refinement of operations happens in a strict 1:1 relation.
Practically this means that every operation from the abstract machine is
refined in the concrete one only once, and no new operations are introduced.
Furthermore, the name of the operation and the number and name of its
parameters cannot change in the concrete machine $M_{C}$ once defined in the
abstract machine $M_{A}$.

In Event-B, refinement is more liberal. For example, it is allowed to rename
events, and it is allowed to introduce new events in $M_{C}$ that refine the
invisible skip event from $M_{A}$. Furthermore, unlike B, in Event-B, multiple
events in $M_{C}$ can refine one abstract event from $M_{A}$, and the
parameters can also be changed. To check for the consistency of an Event-B
refinement, one can use proofs showing a refinement does not violate the
abstract model. These proofs are supported by, for example, the Rodin platform
[3].

Figure 1(a) shows an abstract model of a traffic light taken from the Rodin
handbook [10]. We see two variables, one for pedestrians and one for cars,
stating whether they can pass. We can manipulate these variables with events.
Additionally, the invariant @inv3 ensures that cars and people cannot pass at
the same time.

Figure 1(b) shows the refinement of Figure 1(a). Here, two main features are
implemented. First, we replace the Boolean variables with actual colors
introduced in Figure 1(c) and couple the abstract and concrete states with
@inv7 and @inv8, thus ensuring that the safety invariant established in Figure
1(a) is also present in Figure 1(b). Furthermore, we have two colors for
pedestrians and four for a car traffic light. The fact that these four
phases222We model them in the way how German traffic lights operate. have a
specific order is accounted for in set_cars_colors where we have four
consecutive phases for the lights. namely: green $\rightarrow$ yellow
$\rightarrow$ red $\rightarrow$ red,yellow $\rightarrow$ green. Second, we
introduce a new behavior in the form of the activateSystem event that refines
skip. This event symbolizes the start of the system and is fired once.

In Event-B, stuttering events are allowed. Stuttering describes the phenomenon
when one abstract transition/state is replaced with multiple concrete ones.
From the perspective of the abstract model, the concrete one has the same
behavior. From the concrete model perspective, one may have to do multiple
steps in the concrete state-space to mirror one abstract step. The abstract
handling of the traffic light contains two consecutive phases for cars TRUE
$\rightarrow$ FALSE and the concrete version contains four consecutive color
phases, as mentioned earlier. Abstract and concrete states are coupled via the
witness @new_value, such that the light is green whenever the Boolean variable
would be TRUE and vice versa, thus mapping one abstract state to multiple
concrete ones.

(a) Abstract machine with binary light status

(b) Refined machine with colors

(c) Context for colors

(d) Example of trace refinement result visualization outputted by BERT

Figure 1: Traffic light refinement example

###  2.2 ProB

ProB [6] is a model checker and animator for formal methods, including B and
Event-B. ProB allows for sophisticated manipulation and reasoning about models
of different formal languages with its extensions and libraries, making it a
suitable tool for trace refinement. BERT is implemented as an add-on to ProB
and utilizes its infrastructure, e.g., Java APIs of the kernel, to execute the
necessary tasks.

##  3 Trace refinement concept

Back and Wright [5] showed how to establish a refinement relationship by
showing that the behavior of the concrete machine simulates the abstract
machine. We are not establishing a refinement relationship here but
transforming a trace from $M_{A}$ to $M_{C}$. The target of trace refinement
is to find a trace in $M_{C}$ that contains the behavior of the trace from
$M_{A}$. This is achieved step-wise by transforming the abstract trace’s
transitions and adapting them for the concrete machine. However, as Back and
Wright’s approach works well for transforming a concrete trace back to an
abstract one, one cannot simply conclude the other way around. This is because
not every abstract trace has a concrete counterpart. Similarly, only because
an abstract trace can be refined for a concrete machine, those machines are
not necessarily in a correct refinement relationship. However, the concrete
machine mimics the behavior of the abstract machine encoded in the form of a
trace.

###  3.1 Trace refinement in B

For B, the concept of trace refinement is implemented in the form of
refinement checking to ensure that an abstract machine contains all concrete
traces [7, 9, 18]. We define a trace $T$ as an ordered list of transitions
$t_{1},\ldots,t_{n}$, which describe the operation’s name, the parameters
used, and the state reached. For a B machine, it is refined to $T^{\prime}$
iff every transition $t$, consisting of a state and an operation, from the
abstract trace has 1) a distinguishable counterpart in the corresponding
concrete trace, 2) transitions and states have the same order, and 3) the
length of the abstract trace and the concrete trace is equal. These attributes
are directly derived from the notion of refinement of B refinement and the
findings of Leuschel and Butler [18] regarding refinement checking via traces.

###  3.2 Trace refinement in Event-B

Trace refinement in Event-B is commonly established via proofs. In terms of
our trace refinement algorithm, it is more challenging than the B version. Let
us consider a small example trace for Figure 1(a). INITIALISATION
$\rightarrow$ set_cars(TRUE) $\rightarrow$ set_cars(FALSE) represents the
abstract model allowing the cars to go and stops them afterwards. Now we want
to refine the trace and adapt it to Figure 1(b). Consider Figure 1(d) as a
reference to a successful refinement333The graphical output shown in Figure
1(d) is the result of BERT’s automatic visualization. As ProBs internal
representation is used, some names, for example $initalize\\_machine$, are
held in the ProB style.. Figure 1(d) shows two traces, both to be read
horizontally. Each rectangle represents a trace transition, with the upper
part being the operation and the body representing the changed values. The
different transitions are connected via the red lines. The connection between
the abstract and concrete transitions is marked with strokes with a square
head on both ends, e.g., the concrete initialization contains a more
sophisticated set of variables than the abstract one. Two placeholders skip
and stuttering were inserted in the places where the concrete trace diverges
from the abstract - those two transitions were not part of the abstract trace.
The event activateSystem that refines skip has become a necessity in order to
progress further in the trace. Same goes for set_cars_colors, which is a
stuttering action. Note the values of the machine here. While it was possible
to directly switch from TRUE to FALSE in the abstract version, a stuttering
action is needed as FALSE is mapped to red and red,yellow in the concrete
version.

For a successful trace refinement, we borrow some of the attributes from
section 3.1: 1) pairs of abstract and concrete states are distinguishable, and
2) order persevering. However, with 3), the trace might get lengthier as new
observable behaviors might become necessary to mirror the abstract behavior in
the concrete model. Though acceptable, being unavoidable, the addition of new
behaviors is not preferable.

A significant challenge for the trace refinement algorithm is stuttering, skip
refinements, and their ability to introduce divergence [8]. Divergence means
that the model neither runs in a deadlock nor terminates but evolves in a way
not observable from an abstract standpoint. For refinement in Event-B, this
can be the case as skip and refines keywords add behaviors not observable from
an abstract viewpoint. We cannot be sure whether these behaviors terminate or
deadlock at some point. Event-B offers a solution for this by annotating
events as convergent associated with a proof that the event will occur only
finite times often. Further challenges are that multiple events can refine a
single one, thus forcing us to investigate all concrete events, and that
renaming can occur.

To sum up: Trace refinement in Event-B, like in B, ensures that the abstract
behavior is preserved in the concrete trace in the same order. However, there
can be additional, new behaviors only observable in the concrete machine at
any point in the concrete trace. If the related events are not annotated as
convergent at some point, these concrete events can occur infinitely often. If
the convergence is unproven, we can run into a situation where we often
discover new concrete states that do not present in the abstract model, thus
running into an endless loop without any abort condition.

##  4 BERT

BERT444BERT is available as part of ProB2, see
https://www3.hhu.de/stups/downloads/prob2/snapshot/ is a technique and tool
for trace refinement. It needs $M_{A}$, $M_{C}$, and the trace to be refined.
BERT uses the ProB libraries to prepare the machines on the implementation
level. The actual refinement process is done with the help of the ProB
animator. The solution can be stored in the trace format used by the
animator555A demo is provided at
https://doi.org/10.6084/m9.figshare.16909006.v2. It can be replayed on the
concrete machine without additional measures. If there is no solution, an
error message is displayed, and the last attempt is given as a trace. The
visual representation provided by BERT is shown in Figure 1(d).

###  4.1 Trace refinement for B

The existence of data refinement makes it necessary to observe abstract and
concrete state space simultaneously when doing trace refinement as a designer
can replace abstract variables with concrete ones. The consequence is that the
abstract variables are no longer visible in the concrete machine. This could
leave us unsure which transition to take when doing trace refinement, as each
transition in the trace is formulated as a predicate over state variables and
enabled operations. Missing information could lead to ambiguity. The problem
is that machines are independent components. Therefore, we combine the state
spaces of $M_{A}$ and $M_{C}$ to eliminate the data refinement problem. One
way to achieve this is by merging abstract syntax trees (ASTs) and creating an
intermediate machine. After a successful combination of state spaces, we can
proceed with trace refinement.

Let $M(R,V,I,Op)$ be a simplified machine. Each of the four elements
represents one of the ASTs node types.

  * •

$R$ is the set of references to other machines, represented as an identifier
list

  * •

$V$ is the set of variables, represented as an identifier list

  * •

$I$ is the invariant, a conjunction of predicates

  * •

$Op$ is the set of operations. An operation has the form $op(N,In,Ou,B)$

    * –

$N$ represents the name of the operation

    * –

$In$ represents input variables of the operation

    * –

$Ou$ represents output variables of the operation

    * –

$B$ represents the body of the operation

Let $M_{A}(R_{A},V_{A},I_{A},Op_{A})$ be the abstract and
$M_{C}(R_{C},V_{C},I_{C},Op_{C})$ be the concrete machine. An interleaved
machine $M_{I}=M_{A}||M_{C}$ has the form $M_{I}(R_{A}\cup R_{C},I_{A}\land
I_{C},V_{A}\cup V_{C},Op_{A}||Op_{B})$ and the operations are interleaved by
$Op_{A}||Op_{B}=\\{op(N,In,Ou,B_{1}||B_{2})|op(N,In,Ou,B_{1})\in Op_{A}\land
op(N,In,Ou,B_{2})\in Op_{C}\\}$. In the case of the operation bodies, $||$ is
the parallel substitution. As parameters cannot be changed, they stay
untouched. In B machines with multiple, overlapping references, merging
$R_{A}$ and $R_{C}$ can be challenging. This is because of the possibility
that $R_{A}$ and $R_{C}$ could contain conflicting statements which would need
to be resolved by renaming large parts of the AST to avoid conflicts.
Currently, these cases are not treated in this work and should be considered
as out of scope.

Algorithm 1 shows the process of the actual trace refinement. For reasoning,
we borrow the $start\overset{op}{\underset{M_{C}}{\rightarrow}}s$ notation
from the work of Leuschel et al. [18] to describe the process of creating a
transition. This notation expresses multiple things. First, a transition goes
from a state $start$ to a state $s$. Furthermore, the transition uses the
operation $op$. Finally, the transition is executed on the machine $M_{C}$.
Internally, the transition is written as a predicate consisting of abstract
variables, operation parameters, and the operation name. If an operation with
the name exists that fulfills the predicates, the operation is seen as a valid
transition.

Algorithm 1 aims to implement the condition for successful trace refinement we
set up in Section 3.1: an order-preserving and length preserving image from an
abstract transition to the concrete counterpart. In Algorithm 1, we show how B
traces are refined. We take a transition, find its counterpart, and append the
found concrete transition to our solution in each step. This happens in line
12 of Algorithm 1. As multiple solutions per transition are possible, we have
to carry all those solutions with us, which result in the fact that we store
all concrete traces that are candidates for being a solution in currentTraces.
Due to the way we copy resultTraces into currentTraces, we dismiss those
traces from further calculations that are no more qualified candidates. The
way we use the coupled state spaces, the
$start\overset{op}{\underset{M_{C}}{\rightarrow}}s$ relation and reduce the
trace in each step, we ensure that Algorithm 1 produces the correct result.

Algorithm 1 Algorithm of BERT for B

1:$M_{C}$ that has access to $M_{A}$, Trace T made out of a list of
transitions $t_{1},\ldots,t_{n}$ with t = (op,s)

2:$resultTraces\leftarrow$ FindPath($\langle\langle(\\_,root)\rangle\rangle$,
T, $M_{C}$)

3:if resultTraces = $\langle\rangle$ then

4: println(_”Trace could not be translated”_)

5:else

6: selectAnySolution(resultTraces) $\triangleright$ Hand selection of the
result

7:end if

8:function FindPath(currentTraces, T, $M_{C}$)

9: for (op, s) $\in$ T do

10: resultTraces $\leftarrow\langle\rangle$

11: for trace $\in$ currentTraces do

12: (_, currentState) $\leftarrow$ last(trace)

13: trans
$\leftarrow\\{(op,s^{\prime})|currentState\overset{op}{\underset{M_{C}}{\rightarrow}}s^{\prime}\land
s\sqsubseteq s^{\prime}\\}$ $\triangleright$ Next reachable states

14: for tran $\in$ trans do $\triangleright$ Collect all solutions

15: resultTraces $\leftarrow$ append(resultTraces, append(trace, tran))

16: end for

17: end for

18: currentTraces $\leftarrow resultTraces$

19: end for

20: return currentTraces

21:end function

###  4.2 Trace refinement for Event-B

Merging state spaces for Event-B is analogous to B, as shown in section 4.1,
with minor changes in how parameters and 1:n relations between concrete events
are handled.

The trace refinement algorithm for Event-B is shown in Algorithm 2. Besides
static information about alternatives and skip refinement, it includes a list
of trace data structures, which itself is a triple and consists of the current
concrete trace, the abstract transitions left, and the already visited nodes
of the state space. We loop until we either have no further state to traverse
and return unsuccessful or find a trace that refines all abstract steps and
has found a solution. Inside the loop, we consider each trace structure, which
is currently maintained as a possible solution for all valid successors. In
line 13 of Algorithm 2, one can recognize the formulation already used in
Algorithm 1 where a direct equivalent to an abstract transition exists. In
this case, the abstract trace is reduced in size in line 16 of Algorithm 2,
and the solution for this step is added to the set of solutions. In line 18 of
Algorithm 2, we create all solutions for this step, erasing all stored states
as we made progress in reducing the task size. New is the calculation for skip
and stuttering in line 20. We remove every transition we have already seen
from the found solutions to avoid being livelocked as we made no progress in
reducing the task size. In line 23, we then construct the set of solution
candidates. All solution candidates are then sent to the next iteration. As
Algorithm 2 terminates when it reaches the first set of solutions, we can be
sure that we find a minimal solution without added behavior if there is any.

Algorithm 2 Algorithm of BERT for Event-B

1:$M_{C}$ that has access to $M_{A}$, Trace T made out of a list of
transitions $t_{1},\ldots,t_{n}$ with t = (op,s), a map alt mapping abstract
to concrete operations, the list of transitions refining skip

2:$resultTrace\leftarrow$ FindPath($\langle
trace(\langle(\\_,root)\rangle,T,seenTrans)\rangle,M_{C},alt,skip$)

3:if resultTraces = $\langle\rangle$ then

4: println(_”Trace could not be translated”_)

5:else

6: return selectAnySolution(resultTraces)

7:end if

8:function FindPath(currentTraces, $M_{C}$, alt, skip)

9: while $\lvert currentTraces\rvert\neq 0\land\nexists trace\in
currentTraces\centerdot\lvert trace(1)\rvert=0$ do

10: resultTraces $\leftarrow\langle\rangle$

11: for entry $\in$ currentTraces do

12: (op, s) $\leftarrow$ first(entry(1))

13: (_, cS) $\leftarrow$ last(entry(0))

14: t $\leftarrow\\{(op^{\prime},s^{\prime})|op^{\prime}\in alt(op)\land
cS\overset{op^{\prime}}{\underset{M_{C}}{\rightarrow}}s^{\prime}\ \land
s\sqsubseteq s^{\prime}\\}$

15: for tran $\in$ t do

16: T $\leftarrow$ entry(1)

17: newT $\leftarrow$ drop(T,0) $\triangleright$ Reduce the task size

18: newTrace $\leftarrow$ append(entry(0), tran)

19: resultTraces $\leftarrow$ append(resultTraces, trace(newTrace, newT,
$\langle\rangle$)

20: end for

21: t $\leftarrow\\{(op^{\prime},s^{\prime})|(op^{\prime}\in$ skip $\lor
op^{\prime}\in alt(tOp))\land
cS\overset{op}{\underset{M_{C}}{\rightarrow}}s^{\prime}\land
s^{\prime}\sqsubseteq cS\\}$

22: t $\leftarrow$ t $\cap$ entry(2) $\triangleright$ Remove all solutions
leading into livelock

23: for tran $\in$ t do

24: seenTrans $\leftarrow$ tran $\cup$ entry(2) $\triangleright$ Add seen
transitions

25: newTrace $\leftarrow$ append(entry(0), tran)

26: mewEntry $\leftarrow$ trace(newTrace, entry(1), seenTrans)

27: resultTraces $\leftarrow$ append(resultTraces, newEntry)

28: end for

29: end for

30: currentTraces $\leftarrow$ resultTraces

31: end while

32: return $\\{trace|trace\in currentTraces\land\lvert trace(1)\rvert=0\\}$

33:end function

###  4.3 Practical limitations and optimizations

Practically the state space explosion problem can hinder both algorithms from
finding a solution if the machine running the algorithm runs out of memory. In
the case of Event-B, introduced divergence can result in an endless loop.
However, it is up to the designer to show the convergence of the events.

The designer may limit the search depth or the number of investigated branches
to mitigate the state space problem. In our implementation and the resulting
testing, we had good experiences with this. A further modification to the
proposed algorithms was a mixed breadth/depth-first search resulting in
quicker results in our test cases for the price that, in rare cases, not the
shortest solution was found. Further optimization was comparing candidate sub-
traces for their equality, resulting in pruning traces that occurred multiple
times.

##  5 Case studies

In this section, we experiment to validate the proposed technique on two
industrial-strength case studies, both implementing models of an automotive
system [16]. For brevity, we demonstrate only the Event-B implementation as
shown in Algorithm 2 on case studies as Event-B refinements pose a more
significant challenge than B as far as trace refinement is concerned. In the
first case study, we work out the quality aspect of trace refinement. In the
second case study, we address the performance aspect.

###  5.1 Pitman arm controller

#### Case study description.

The first case study is the pitman arm controller model [20]. The authors
modeled a pitman arm that controls car lights and the user’s interaction with
it. The model consists of three machines forming a refinement chain of:

$BlinkLamps\rightarrow PitmanController\rightarrow PitmanControllerTime$

BlinkLights models the light environment of a car and its behavior. It allows
controlling lights. Furthermore, one can set a blinking timer emulating the
actual number of blinks of the lights. In the model itself, the amount is set
via parameters of the SET_REMAININGBlinks and its refinements. -1 means
forever, 3 means three-time, and so on. The third feature is the tip blinking
or comfort blinking of modern cars, which is also modeled. The
PitmanController extends the BlinkLights and adds an actual car environment
building on top of the lamps. The position of the Pitman arm and car’s key
state is modeled. In PitmanControllerTime the abstract time counting is
replaced with a concrete one. Normally the tip blinking of a car has a
specified time interval, usually three to five times. PitmanControllerTime
models this behavior. For the experiment we will create a trace on BlinkLamps
and refine it step-wise to PitmanControllerTime. We will present all three
traces and evaluate what the refinement did to the trace and which knowledge
one can extract from this.

#### Results.

In Figure 2 one can see the abstract trace and its refinements. The abstract
trace in Figure 2(a) captures the idea of first using the tip blinker, but the
user then decides to make the blinking permanent after one blink. Again, after
one blink, the user turns off the blinker entirely.

In Figure 2(b) one can see the adaptation. The most important change is that
it is now necessary to turn on the engine, for the lamps to blink. A new
transition at position 4 is introduced for this. Renaming introduced with the
refinement is considered, and the events have been changed accordingly, for
example, SET_REMAININGBlinks is now called TIME_Tip_Blinking,
SET_RightBlinkersOn is now called ENV_Pitman_TipBlinkingRight_Blink, and
SET_AllBlinkersOff is now called ENV_Pitman_Reset_to_Neutral_Noblink.

For the third refinement, the introduction of time had a minor effect on the
existing behavior. This is mirrored in the resulting trace adaptation. In
Figure 2(c) we see no change compared to Figure 2(b) besides additional
parameters for the events, for example, on position 3.

We gathered multiple insights into the effectiveness of trace refinement from
our experiments. 1) The engine needs to be turned on for the lights to blink,
which can be checked against the specification to learn if it is intentional
behavior. 2) The newly introduced event in PitmanControllerTime does not
interfere with existing behavior. Once again, one can check if this is
intentional. 3) From the perspective of animation, there is an event
SET_RemainingBlinks that can have parameters 1,2,3 as input. We observed that
2 always leads to a failing adaptation process. When checking for the reason,
it was found that the state in which the remaining blinks are equal to 2 is no
longer reachable. Therefore, all behaviors relying on this are no longer
possible. Designers might want to check whether this is an intentional
behavior with the stakeholders.

(a) Original trace on BlinkLamps

(b) Refined trace on PitmanController

(c) Refined trace on PitmanControllerTime

Figure 2: Trace before and after the first and second step of trace
refinement.

###  5.2 Automotive adaptive exterior light system

#### Case study description.

The second case study is more complex than the first one and is about the
specification of the adaptive exterior light system of an automobile [22]. The
case study focuses on the lights, their behavior, reaction to the user, and
environmental changes. As a result, the refinement chain is more prolonged,
reaching from M0 as the most abstract machine to M5 as the most concrete
machine.

  * •

M0 introduces a simple event with the name headLightSet with the ability to
set a specific light of the car to a specific level.

  * •

M1 introduces the interfaces allowing the user to interact with the car.

  * •

M2 introduces details to the direction indicators, the hazard lights, and the
emergency brake light.

  * •

M3 introduces details for the low beam lights.

  * •

M4 introduces details for the cornering lights.

  * •

M5 introduces details for the high beam lights.

The introduction order of the features in M2 up to M5 was arbitrary. This is
related to the problem of expressing topological orders in the strict Event-B
refinement hierarchy even tho there are attempts, such as by Mashkoor et al.
[24]. We provide an overview of the exact metrics of all refinement steps in
table 1. Like the previous case study, the first refinement step sees a
massive increase of events as several new features are introduced to model the
user interface. The table shows that we have a continuous, stark growth of
variables in each step, on average twelve, which heavily increased the state
space in each step. The fact of the possible inputs further blows up the
state-space for each event. As events had large sets of parameters, each step
had a large set of possible parameter values. The resulting increase of the
state space caused problems as generating all possible inputs for an event
became very memory intensive. Thus, there was a need for cutting away
solutions to not run out of memory. For this, the internal standard of ProB
was used that provides the first five correct solutions to a predicate if not
further modified. For the experiment, we create a longer trace (30 steps) and
find an adaptation for each machine. As mentioned earlier, this quantitative
experiment shows how well BERT deals with larger state spaces.

Table 1: Refinement chain statistics Machine | M0 | M1 | M2 | M3 | M4 | M5
---|---|---|---|---|---|---
Introduced Variables | 1 | 15 | 9 | 12 | 12 | 12
Overall Variables | 1 | 16 | 25 | 37 | 49 | 61
Introduced Events (via skip) | 1 | 1 | 0 | 0 | 0 | 3
Refined Events | N/A | 10 | 3 | 5 | 0 | 0
Extended Events | N/A | 1 | 11 | 14 | 20 | 20
Overall Events | 1 | 12 | 14 | 19 | 20 | 23

#### Results.

With the introduced restrictions, a trace could be successfully adapted. The
results are shown in Table 2. For our experiment, we measure four categories:
1) the input trace to the algorithm, 2) the time needed for adaptation, 3) the
number of transitions that need to be added for a successful adaptation, and
4) the amount of solutions found for the input trace.

The trace was not refined for M1 as it was created on this machine, thus N/A.
We can see that the number of transitions stays constant while the calculation
time increases up to M4. The reason here seems to be the number of possible
solutions and the increasing number of variables later leading to state space
explosion. The decline in time for M5 can be explained because there were not
many solutions to be explored. No transitions were added, which was expected
as the refinement steps focused on adding new behaviors, so the abstract
behavior was preserved.

Overall we conclude the experiment a success. We anticipated problems with
larger state spaces when designing the algorithm back in Section 4.3.
Nevertheless, we managed to refine a trace even under more challenging
conditions.

Table 2: Trace refinement statistics for the trace refined with BERT Machine | M1 | M2 | M3 | M4 | M5
---|---|---|---|---|---
Trace Input Size | N/A | 96 | 96 | 96 | 96
Adaptation Time (ms) | N/A | 1663 | 2289 | 8268 | 1938
Added Transitions | 96 | 0 | 0 | 0 | 0
Individual solutions | N/A | 3 | 4 | 10 | 2

###  5.3 Threat to validity

The application of Algorithm 2 to case studies poses an internal threat. We
used the readily available implementations. While the first case study was
created to be animated, the second was not, meaning that creating traces was
far more difficult for the second case study. We created meaningful traces for
the first case study, and the results had meanings we could reason. The second
case study was not created with animation in mind. Hence the traces created to
test were not always meaningful. In the first case study, we observed quality
features of the behavior of trace refinement, while in the second one, we
could only observe quantitative behaviors.

##  6 Lessons learned

  * •

Trace early. Following this long-standing advice can indeed save from making
poor design choices. Trace refinement can then help to design elegant
refinement steps.

  * •

Keep the refinement step simple and small, i.e., introduce one feature per
refinement as also suggested by Mashkoor et al. [23]. This will simplify the
refinement process and help understand the reasons for a failing trace
refinement.

  * •

Do not create unnecessary choice points. Checking choice points created by
newly introduced events and non-deterministic choices can increase calculation
time significantly. This was discovered when searching for a valid
configuration that holds throughout the refinement chain. Whenever there was
no first best choice but many second-best choices, the path branched heavily,
leading to long-running times. This case can be handled by keeping the number
of choice points introduced in each refinement step small.

Overall, BERT helped clarify whether a specific behavior in $M_{A}$ is still
valid in $M_{C}$. This seems particularly interesting from the designer’s
perspective as it can validate the assumption that refinement ruled out a
particular behavior. In addition, the high level of details that a trace
provides can help a designer understand why a specific behavior is not
feasible in the refinement, thus identifying modeling flaws.

Especially interesting when using trace refinement is what can be learned from
a failing adaptation. There are two reasons for a failing adaptation. Either
there is no adaptation or the adaptation is not achievable within the set
memory limits. If we expect a successful adaptation, a manual inspection of
the resulting trace of the failed adaptation can uncover design flaws. It can
hint at questionable design from the animation perspective, as shown in the
second case study, where technical limitations made it hard to find solutions.
One might want to rethink the model to keep it easily animatable and
traceable. Also, with manual inspection of failing results, cases were
encountered where events were not sound and forgot to reset a specific
variable leading to a failing adaptation.

##  7 Related work

We compare our technique to the related work’s existing trace and scenario
refinement techniques. We want to stress the difference between traces and
scenarios. Even though the term ’scenarios’ is heavily overused, we can
extract a baseline of scenarios being high-level representations of intended
behavior. With high-level, we mean only selected pre-selected variables and
transitions of interest are observed. Traces, on the other hand, are more low
level. As traces need to be precise, they contain all available information
about states and transitions.

#### Trace refinement.

One important inspiration for this paper is how refinement is defined and
established in state-of-the-art CSP [15] algorithms [12]. In CSP, one
specification can refine another in multiple ways, i.e., trace- and failure
refinement. The refinement relationship is established by showing that both
specifications are equivalent regarding the traces they share or do not share.
The notion of ’hiding’ transitions was especially interesting for our
technique. In Event-B, we encountered a similar situation when stuttering
refinement occurred. Whenever a transition or variables only occur in the
concrete specification, we ’hide’ them to treat the situation like a case of
B-trace refinement to check whether the trace is still valid in the concrete
refinement.

#### Scenario refinement.

Arcaini and Riccobene [4] describe how to refine ASM scenarios, which are used
as acceptance tests. Using their proposed tool, scenarios are translated into
an LTL formula. Then $M_{C}$ is loaded into the tool-related model checker,
the LTL formula is negated, and the model checker will try to find a counter-
example. This counter-example can be re-translated into a scenario. The
authors define two mapping procedures from scenario to LTL formulas, one that
is strict and will produce 1:1 traces and one that can produce 1:n traces. The
latter will add new behaviors. Besides the obvious difference that the
proposed technique deals with ASMs, the authors seem not to encounter
divergences as part of the concrete model. The ASM technique completely rely
on its existing framework using an existing scenario language and the LTL
model checker. In contrast, in our technqiue, we can perform calculations only
based on a state-space representation, and we have chosen the one provided by
ProB. Therefore, we provide a common technique for trace refinement and a
tool. The advantage of our technique is that whenever low level properties are
of interest we are able to refine them.

Scenarios for Event-B were introduced, e.g., by Fischer and Dghyam [11] where
Cucumber [29] is used as a description language. However, compared to our
work, the refinement abilities described in the paper are minimal. The created
tests are not further refined but statically generated for each model version.
Another technique to Event-B scenarios, which catered for refinement, was
proposed by Malik et al. [21] where for Event-B models, scenarios were encoded
in CSP and then refined. However, this technique suffers from the need to
encode scenarios in CSP, which loses exact information about states as CSP
only supports reasoning about transitions. Furthermore, the problems tackled
by our work are only partially tackled in this work. The idea of scenario
refinement was then advanced by Snook et al. [27] where it is investigated how
scenarios can be refined or applied to more abstract machines. The authors
also suggested a tool [28] for scenario generation for Rodin that is currently
not able to refine those scenarios.

#### Dual animation.

Our technique focuses on going from an abstract to a concrete level while the
technique of Hallerstede et al. [13, 14] proposes the opposite. In their
technique, a concrete machine is linked to its predecessor, thus giving
insight into how the abstraction behaves when the concrete model does
something. This helps to explore the actual behavior of an abstract and
concrete machine and the changes due to refinement. However, checking the
preservation of behavior is a cumbersome, manual task and not a real option as
too many details need to be considered. With our technique, this task is
automatically done by the provided tool.

##  8 Conclusion and future work

This paper introduces BERT – a technique and a tool to refine traces that are
explicit paths through state space. With this tool, it is possible to refine
traces of abstract B and Event-B machines for their respective refinement.
This transfer helps designers to ensure the presence of an abstract behavior
in the concrete specification. We successfully conducted experiments on two
case studies to showcase the validity of the proposed technique. While BERT
produced the expected results, the case studies helped find its role as a
support tool for designers. With its help, one can comprehend if and why a
specific behavior is still allowed in a refined model. The benefit for the
designer is the fine-grained details a trace provides that allow exact
reproduction of the defined behavior.

We are currently tackling refinements for Event-B and using the usage of the
REFINES keyword for B. In the future, we want to tackle B’s alternative ways
of enriching a machine’s behavior, for example, INCLUDES or EXTENDS. This will
leverage the burden of animating and refining B machines, making trace
refinement through animation more convenient.

## References

  * [1] Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge university press (2005)
  * [2] Abrial, J.R.: Modeling in Event-B: system and software engineering. Cambridge University Press (2010)
  * [3] Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. International journal on software tools for technology transfer 12(6), 447–466 (2010)
  * [4] Arcaini, P., Riccobene, E.: Automatic Refinement of ASM Abstract Test Cases. In: 2019 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). pp. 1–10 (2019)
  * [5] Back, R., von Wright, J.: Trace refinement of action systems. In: International conference on concurrency theory. pp. 367–384. Springer (1994)
  * [6] Bendisposto, J., Geleßus, D., Jansing, Y., Leuschel, M., Pütz, A., Vu, F., Werth, M.: ProB 2-UI: A java-based user interface for ProB. In: International Conference on Formal Methods for Industrial Critical Systems. pp. 193–201. Springer (2021)
  * [7] Butler, M.: An approach to the design of distributed systems with B AMN. In: International Conference of Z Users. pp. 221–241. Springer (1997)
  * [8] Derrick, J., Boiten, E.: Refinement: Semantics, Languages and Applications. Springer (2018)
  * [9] Dunne, S., Conroy, S.: Process refinement in B. In: International Conference of B and Z Users. pp. 45–64. Springer (2005)
  * [10] Rodin User’s Handbook. https://www3.hhu.de/stups/handbook/rodin/current/html/, accessed:
  * [11] Fischer, T., Dghyam, D.: Formal Model Validation Through Acceptance Tests. In: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. pp. 159–169. Springer International Publishing (2019)
  * [12] Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3–a modern refinement checker for CSP. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 187–201. Springer (2014)
  * [13] Hallerstede, S., Leuschel, M., Plagge, D.: Refinement-Animation for Event-B — Towards a Method of Validation. In: Abstract State Machines, Alloy, B and Z. pp. 287–301. Springer Berlin Heidelberg (2010)
  * [14] Hallerstede, S., Leuschel, M., Plagge, D.: Validation of formal models by refinement animation. Science of Computer Programming 78(3), 272–292 (2013)
  * [15] Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21(8), 666–677 (1978)
  * [16] Houdek, F., Raschke, A.: Adaptive exterior light and speed control system. In: International Conference on Rigorous State-Based Methods. pp. 281–301. Springer (2020)
  * [17] Leuschel, M.: Spot the Difference: A Detailed Comparison Between B and Event-B. In: Logic, Computation and Rigorous Methods, pp. 147–172. Springer (2021)
  * [18] Leuschel, M., Butler, M.: Automatic Refinement Checking for B. In: Formal Methods and Software Engineering. pp. 345–359. Springer Berlin Heidelberg (2005)
  * [19] Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. International Journal on Software Tools for Technology Transfer 10(2), 185–203 (2008)
  * [20] Leuschel, M., Mutz, M., Werth, M.: Modelling and Validating an Automotive System in Classical B and Event-B. In: Rigorous State-Based Methods. pp. 335–350. Springer International Publishing (2020)
  * [21] Malik, Q.A., Lilius, J., Laibinis, L.: Model-based testing using scenarios and Event-B refinements. In: Methods, Models and Tools for Fault Tolerance, pp. 177–195. Springer (2009)
  * [22] Mammar, A., Frappier, M., Laleau, R.: An Event-B Model of an Automotive Adaptive Exterior Light System. In: Rigorous State-Based Methods. pp. 351–366. Springer International Publishing (2020)
  * [23] Mashkoor, A., Jacquot, J.P.: Guidelines for Formal Domain Modeling in Event-B. In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering. pp. 138–145 (2011)
  * [24] Mashkoor, A., Jacquot, J.: Utilizing Event-B for domain engineering: a critical analysis. Requir. Eng. 16(3), 191–207 (2011)
  * [25] Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exp. 48(12), 2350–2379 (2018)
  * [26] Mashkoor, A., Leuschel, M., Egyed, A.: Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER). pp. 1–5 (2021)
  * [27] Snook, C., Hoang, T.S., Dghaym, D., Fathabadi, A.S., Butler, M.: Domain-specific scenarios for refinement-based methods. Journal of Systems Architecture 112, 101833 (2021)
  * [28] Snook, C., Hoang, T.S., Fathabadi, A.S., Dghaym, D., Butler, M.: Scenario Checker: An Event-B tool forvalidating abstract models. Rodin Workshop (2021)
  * [29] Wynne, M., Hellesoy, A., Tooke, S.: The cucumber book: behaviour-driven development for testers and developers. Pragmatic Bookshelf (2017)


for some coefficients $a_{i},b_{i}$. Then, if $w,z$ satisfy the system (7.19),
we conclude that

$\textstyle-\sum_{i}\lambda_{i}a_{i}\varphi_{i}+\mu_{1}\sum_{i}b_{i}\varphi_{i}=\sum_{i}\langle
f_{1},\varphi_{i}\rangle\varphi_{i}$

and similarly

$\textstyle-\sum_{i}\lambda_{i}b_{i}\varphi_{i}+\mu_{1}\sum_{i}a_{i}\varphi_{i}=\sum_{i}\langle
f_{2},\varphi_{i}\rangle\varphi_{i}.$

Therefore, by the first equation for any $i$ we need

$\textstyle b_{i}=\frac{1}{\mu_{1}}\langle
f_{1},\varphi_{i}\rangle+\frac{\lambda_{i}}{\mu_{1}}a_{i}$

and putting this information into the second equation

$\textstyle-\frac{\lambda_{i}}{\mu_{1}}\langle
f_{1},\varphi_{i}\rangle+\frac{-\lambda_{i}^{2}}{\mu_{1}}a_{i}+\mu_{1}a_{i}=\langle
f_{2},\varphi_{i}\rangle$

which implies

$\textstyle a_{i}=\frac{1}{\mu_{1}^{2}-\lambda_{i}^{2}}\,\\{\,\mu_{1}\,\langle
f_{2},\varphi_{i}\rangle+\lambda_{i}\,\langle f_{1},\varphi_{i}\rangle\,\\}$

since $\mu_{1}\neq\lambda_{i}$. This proves that (7.19) has a (unique)
solution if $g_{1},g_{2}\in C_{c}^{\infty}(\Omega)$. The general case follows
by approximation arguments, by recalling that $C_{c}^{\infty}(\Omega)$ is
dense in $L^{\varrho}(\Omega)$.

The fact that the solution is unique can be proved considering the problem

$\beta\Delta w+\mu_{1}z=0,\quad\beta\Delta z+\mu_{1}w=0\;\textrm{ in
}\;\Omega,\quad w\,=\,z=0\;\textrm{ on }\;\partial\Omega,$

and recalling that
$\lambda_{1}(\beta\Delta,\beta\Delta)<\mu_{1}<\lambda_{2}(\beta\Delta,\beta\Delta)$.
∎

###### Conclusion of the proof of Theorem 1.11-(ii).

Taking, as before
$R:=1+C(1+\max\\{\|f_{1}\|_{\varrho},\|f_{2}\|_{\varrho}\\})$, we have by
homotopy invariance of the degree that
$\deg(\mathcal{B}_{0},B_{R}^{E}(0),0)=\pm 1.$ Therefore there exists $(u,v)\in
B_{R}^{E}(0)$ such that $\mathcal{A}_{0}(u,v)=(u,v)$, and this gives us the
desired existence result. Notice that $0\not\in\mathcal{B}_{s}(\partial
B_{R}^{E}(0))$ due to the a priori estimates we get in Lemma 7.13. ∎

##  8 The signed Dirichlet problem

In this section we draw some attention to the Dirichlet problem (1.4), or
equivalently to (2.7), see Section 2.4, in the case the functions
$f_{1},f_{2}$ have the “good” sign.

When $pq=1$ we have seen that the Dirichlet problem (5.5) is solvable for any
$\lambda<m_{1}$, with $m_{1}$ as in (2.6), independently of sign on
$f_{1},f_{2}$. Now we turn to the case $\lambda\in(m_{1},M_{1})$.

Moreover, a variation of such argument applies to show that the Dirichlet
problem is uniquely solvable among positive viscosity solutions in the
sublinear regime $pq<1$. We start with the latter, by proving Theorem 1.17.

###### Proof of Theorem 1.17.

We borrow some ideas from [33, Section 5] and [32, Theorem 4.1], based on a
Krasnoselskii [29] type argument.

Step 1) Existence: Let us consider the eigenvalue problem obtained in Theorem
1.3 for the operators $(F_{1})_{*}$ and $(F_{2})_{*}$, i.e. we take the strong
solution pair $\varphi,\psi\in W^{2,p}_{\mathrm{loc}}(\Omega)$ of

$\displaystyle\left\\{\begin{array}[]{rclcc}(F_{1})_{*}[\varphi]+\lambda_{1}^{+}\tau_{1}(x)\psi^{1/p}=0&\mbox{in}&\;\Omega\\\
(F_{2})_{*}[\psi]+\lambda_{1}^{+}\tau_{2}(x)\varphi^{p}=0&\mbox{in}&\;\Omega\\\
\varphi\,,\;\,\psi&>&0&\mbox{in}&\;\Omega\\\
\varphi\;\,=\,\;\psi&=&0&\mbox{on}&\;\partial\Omega.\end{array}\right.$ (8.5)

Notice that the operators $(F_{i})_{*}$ are homogeneous if $F_{i}$ are
homogenous, namely satisfy (H2). Moreover,
$\lambda_{1}^{+}(((F_{i})_{*})^{*})=\lambda_{1}^{-}(((F_{i})_{*})_{*})=\lambda_{1}^{-}((F_{i})_{*})=\lambda_{1}^{+}(F_{i}^{*})>0$,
hence also (H3) is true. Finally, $(F_{i})_{*}$ satisfy (H4) as they are
concave operators with $(F_{i})_{*}(\cdot,0,0,0)=0$, see Lemma 3.5. For the
sake of convenience we now look at the Dirichlet problem

$\displaystyle\left\\{\begin{array}[]{rclcc}F_{1}[u]+\tau_{1}(x)|v|^{q-1}v&=&f_{1}(x)&\mbox{in}&\;\Omega,\\\
F_{2}[v]+\tau_{2}(x)|u|^{p-1}u&=&f_{2}(x)&\mbox{in}&\;\Omega,\\\
u\,\;=\,\;v&=&0&\mbox{on}&\;\partial\Omega.\end{array}\right.$ (8.9)

Observe that (1.4) and (8.9) are equivalent up to scaling, since $pq<1$, see
Section 2.4.

We first construct a subsolution pair
$(u_{0},v_{0})=(\epsilon\varphi,\;\epsilon^{k}\psi)$ to (8.9), say for
$f_{i}\in L^{\varrho}(\Omega)$ with $f_{i}\leq 0$ a.e. in $\Omega$. We use
(8.5) and pick up some positive constants $\varepsilon,k$ to be chosen. For
this, we write in the a.e. sense,

$\displaystyle-
F_{1}[u_{0}]\leq-(F_{1})_{*}[\varepsilon\varphi]=\lambda_{1}^{+}\epsilon\tau_{1}\psi^{1/p}=\lambda_{1}^{+}\tau_{1}(\epsilon^{p}\psi)^{1/p}\leq\tau_{1}v_{0}^{q}-f_{1}(x),$
(8.10)

and

$\displaystyle-
F_{2}[v_{0}]\leq-(F_{2})_{*}[\varepsilon^{k}\psi]=\lambda_{1}^{+}\epsilon^{k}\tau_{2}\varphi^{p}=\lambda_{1}^{+}\tau_{2}(\epsilon^{k/p}\varphi)^{p}\leq\tau_{2}u_{0}^{p}-f_{2}(x).$
(8.11)

The choice of $\epsilon$ is made in order to have
$\lambda_{1}^{+}\epsilon^{1-kq}\leq\|\psi\|_{\infty}^{(pq-1)/p}$ in (8.10),
for some $1-kq>0$. In addition, for (8.11) we require
$\lambda_{1}^{+}\epsilon^{k-p}\leq 1$, with $k>p$. Then, by diminishing
$\epsilon$ if necessary, it is enough to choose $k\in(p,{1}/{q})$.

Next, for each $n\geq 0$ we define recursively $(u_{n+1},v_{n+1})$ as the
unique strong solution of

$-F_{1}[u_{n+1}]=\tau_{1}(x)v_{n}^{q}-f_{1}(x)\,,\;\;-F_{2}[v_{n+1}]=\tau_{2}(x)u_{n}^{q}-f_{2}(x)\;\textrm{
in }\Omega\,,\quad u_{n+1}=v_{n+1}=0\;\,\textrm{ on }\partial\Omega.$

Note that by (H3) and ABP-mP for scalar equations (Theorem 3.4, since
$\lambda_{1}^{-}(F_{i}^{*})\geq\lambda_{1}^{+}(F_{i}^{*})>0$) one has
$u_{n+1}$, $v_{n+1}\geq 0$ in $\Omega$, for all $n\geq 0$.

Now we infer that the sequences $(u_{n})$ and $(v_{n})$ are monotone
nondecreasing. This is accomplished via a monotone iterations technique.
Indeed,

$F_{1}^{*}[u_{n}-u_{n+1}]\geq-
F_{1}[u_{n+1}]+F_{1}[u_{n}]=\tau_{1}(x)(v_{n}^{q}-v_{n-1}^{q}),\quad
F_{2}^{*}[v_{n}-v_{n+1}]\geq\tau_{2}(x)(v_{n}^{p}-v_{n-1}^{p}),$

for all $n\geq 1$. For $n=0$ one has

$F_{1}^{*}[u_{0}-u_{1}]\geq-
F_{1}[u_{1}]+F_{1}[u_{0}]\geq\tau_{1}(x)(v_{0}^{q}-v_{0}^{q})=0,\quad
F_{2}^{*}[v_{0}-v_{1}]\geq\tau_{2}(x)(u_{0}^{p}-u_{0}^{p})=0.$

This implies $u_{1}\geq u_{0}$ and $v_{1}\geq v_{0}$ in $\Omega$, by (H3) and
ABP-MP for scalar equations (Theorem 3.4), as desired.

Next we claim that $(u_{n},\;v_{n})$ is bounded in $L^{\infty}\times
L^{\infty}$. To see this we use the blow up method. Suppose
$\alpha_{n}=\|u_{n}\|_{\infty}\to\infty$ in order to get a contradiction. We
know that $(\alpha_{n})$ is a nondecreasing sequence. Hence we define the
rescaled pair

$u_{n}=\alpha_{n}U_{n}$ and $v_{n}=\alpha_{n}^{Q}V_{n}$ , where
$Q=\frac{p+1}{q+1}$.

Properties of $F_{1}^{*}$, $F_{2}^{*}$ and (H1) for $F_{1}$, $F_{2}$ give us

$-F_{1}^{*}[U_{n+1}]\leq-\frac{F_{1}[u_{n+1}]}{\alpha_{n+1}}=\frac{\tau_{1}(x)v_{n}^{q}}{\alpha_{n+1}}-\frac{f_{1}(x)}{\alpha_{n+1}}\leq\tau_{1}(x)\alpha_{n}^{\frac{pq-1}{q+1}}V_{n}^{q}-f_{1}^{n}(x),$

and analogously,

$-F_{2}^{*}[V_{n+1}]\leq-\frac{F_{2}[v_{n+1}]}{\alpha_{n+1}^{Q}}=\frac{\tau_{2}(x)u_{n}^{p}}{\alpha_{n+1}^{Q}}-\frac{f_{2}(x)}{\alpha_{n+1}^{Q}}\leq\tau_{2}(x)\alpha_{n}^{\frac{pq-1}{q+1}}U_{n}^{p}-f_{2}^{n}(x),$

where $f_{1}^{n}(x)={f_{1}(x)}\alpha_{n+1}^{-1}$ and
$f_{2}^{n}(x)={f_{2}(x)}{\alpha_{n+1}^{-Q}}$ for all $n\geq 1$. Since the last
RHS converges to zero in $L^{\varrho}$, then by (H3) and ABP-MP we obtain that
$V_{n+1}\to 0$. So, again ABP-MP for the first equation yields $U_{n+2}\to 0$,
which derives a contradiction.

Therefore, since the sequences $u_{n}^{q}$ and $v_{n}^{p}$ are uniformly
bounded from above and from below, by $C^{\alpha}$ regularity estimates
$u_{n},v_{n}\in C^{\alpha}(\overline{\Omega})$ with
$\|u_{n}\|_{C^{\alpha}(\overline{\Omega})},\|v_{n}\|_{C^{\alpha}(\overline{\Omega})}\leq
C$. Thus compact inclusion and a standard stability argument of viscosity
solutions lead to solution pair $u,v$ of (1.10). Here $u,v>0$ in $\Omega$ by
the uniformly bound from below via $u_{0},v_{0}$.

Step 2) Uniqueness:

Let $(u_{1},v_{1})$ and $(u_{2},v_{2})$ be two positive pairs of viscosity
solutions to (1.10). Since $f_{i}\leq 0$ we can use Hopf lemma to conclude
${\partial_{\nu}u_{i}}<0$ and ${\partial}_{\nu}v_{i}<0$ on $\partial\Omega$,
$i=1,2$, where $\nu$ is the exterior unit normal. Thus we may define (the
nonempty set)

$S=\\{s>0\,:\;u_{1}>s^{\frac{p+1}{p}}u_{2}\,,\;v_{1}>s^{\frac{q+1}{q}}v_{2}\textrm{\,
in }\Omega\,\\}$, $s_{*}=\sup S$.

Here $s_{*}<+\infty$ since $u_{2}$ and $v_{2}$ are positive. So, up to
exchanging the roles of $(u_{1},v_{1})$ and $(u_{2},v_{2})$ if necessary, say
that $s_{*}\leq 1$. Let us look at the nonnegative functions $w,z$ given by

$w:=u_{1}-s_{*}^{\frac{p+1}{p}}u_{2}$ and
$z:=v_{1}-s_{*}^{\frac{q+1}{q}}\,v_{2}$ in $\Omega$,

which satisfy in $\Omega$, in the viscosity sense,

$\displaystyle-(F_{1})_{*}[w]$ $\displaystyle\geq-
F_{1}[u_{1}]+s_{*}^{\frac{p+1}{p}}F_{1}[u_{2}]=\tau_{1}(x)v_{1}^{q}-f_{1}(x)-\tau_{1}(x)s_{*}^{\frac{p+1}{p}}v_{2}^{q}+s_{*}^{\frac{p+1}{p}}f_{1}(x)$
$\displaystyle\geq\tau_{1}(x)\,v_{1}^{q}\,(1-s_{*}^{\frac{1-pq}{p}})-f_{1}(x)\,(1-s_{*}^{\frac{1-pq}{p}})\geq
0,$

and similarly $-(F_{2})_{*}[z]\,\geq 0.$ Whence SMP for scalar equations and
the strongly coupling of the Lane-Emden type system imply either $w,z>0$ or
$w,z\equiv 0$ in $\Omega$.

Suppose on the contrary that $w,z>0$ in $\Omega$. Now we may repeat the
preceding argument with the pair $(u_{2},v_{2})$ replaced by $(w,z)$ in order
to conclude the existence of some small $\varepsilon>0$ such that
$u_{1}>(s_{*}+\varepsilon)u_{2}$ in $\Omega$. But this contradicts the
definition of $s_{*}$ as the supremum of $S$.

Therefore $w,z\equiv 0$ in $\Omega$. To finish we infer that $s^{*}=1$;
otherwise the strict inequalities above and SMP would be in force to produce
the positivity of $w$ and $z$. So one concludes $u_{1}\equiv u_{2}$ and
$v_{1}\equiv v_{2}$ in $\Omega$, as desired. ∎

Next we return to the regime $pq=1$.

###### Proof of Theorem 1.8 (ii), (iii).

We prove $(ii)$; the case $(iii)$ is similar. Since we have $pq=1$, and
$f_{i}\equiv 0$ is an eigenvalue problem which we have already studied, is
enough to consider either $f_{1}\not\equiv 0$ or $f_{2}\not\equiv 0$.
Therefore, we are going to obtain positive solutions, by SMP and strong
coupling of the system. In particular, the uniqueness can be carried out as in
Step 2 of the proof of Theorem 1.17. Let us show the existence assertion in
$(ii)$.

Step 1) Continuous and compactly supported $f_{i}$, with uniformly positive
weights.

Say $\tau_{i}\geq a_{i}>0$ a.e. in $\Omega$, and $f_{i}\geq-b_{i}$ in
$K_{i}=\mathrm{supp}(f_{i})\subset\subset\Omega$, for some $b_{i}>0$, $i=1,2$.
In this case we choose a large constant $A>0$ such that

$b_{1}\leq Aa_{1}(\lambda^{+}_{1}-\lambda)(\psi^{+}_{1})^{q}$ a.e. in $K_{1}$,
$b_{2}\leq A^{p}a_{2}(\lambda^{+}_{1}-\lambda)(\varphi^{+}_{1})^{p}$ a.e. in
$K_{2}$.

Then the pairs $u^{*}=A\varphi^{+}_{1}$, $v^{*}=A^{1/q}\,\psi^{+}_{1}$ and
$u_{*}\equiv 0$, $v_{*}\equiv 0$ satisfy

$\displaystyle F_{1}[u_{*}]+\lambda\tau_{1}(x)|v_{*}|^{q-1}v_{*}\geq
f_{1}(x)\geq F_{1}[u^{*}]+\lambda\tau_{1}(x)|v^{*}|^{q-1}v^{*}\;\;$
$\displaystyle\textrm{ a.e.\ in\, $\Omega$},$ $\displaystyle
F_{2}[v_{*}]+\lambda\tau_{2}(x)|u_{*}|^{p-1}u_{*}\geq f_{2}(x)\geq
F_{2}[v^{*}]+\lambda\tau_{2}(x)|u^{*}|^{p-1}u^{*}\;\;$ $\displaystyle\textrm{
a.e.\ in\, $\Omega$},$

with $u^{*}=u_{*}=0$ and $v^{*}=v_{*}=0$ on $\partial\Omega$. Thus we apply
the same monotone iterations technique as in Step 1 in the proof of Theorem
1.17, from the supersolution case instead of the subsolution one. This time is
even a bit simpler since the supersolution already gives us a uniform bound
from above on the uniform norm of the iterated solutions produced by the
method.

Step 2) General nonnegative $f_{i}\in L^{\varrho}(\Omega)$, but still
uniformly positive weights.

We take sequences $(f_{1}^{k}),(f_{2}^{k})\in L^{\varrho}(\Omega)$ of
continuous nonpositive functions with compact support in $\Omega$ such that
$f_{1}^{k}\to f_{1}$, $f_{2}^{k}\to f_{2}$ in $L^{\varrho}(\Omega)$. By Step
1, let $u_{k},v_{k}\geq 0$ solving

$\displaystyle F_{1}[u_{k}]+\lambda\tau_{1}(x)v_{k}^{q}=f_{1}^{k}(x),\quad
F_{2}[v_{k}]+\lambda\tau_{2}(x)u_{k}^{p}=f_{2}^{k}(x)\quad\textrm{ in
}\,\Omega,$

with $u_{k}=v_{k}=0$ on $\partial\Omega$. We infer that

$\|u_{k}\|_{L^{\infty}(\Omega)},\;\|v_{k}\|_{L^{\infty}(\Omega)}\leq C\textrm{
\; for all $k$.}$ (8.12)

Otherwise, assume for instance that
$\theta_{k}=\|u_{k}\|_{L^{\infty}(\Omega)}\to\infty$ as $k\to\infty$, and set
$u_{k}=\theta_{k}U_{k}$ and $v_{k}=\theta_{k}^{p}\,V_{k}$. Notice that the
pair $(U_{k},V_{k})$ satisfies the equation

$\displaystyle\textstyle
F_{1}[U_{k}]+\lambda\tau_{1}(x)V_{k}^{q}=\frac{f_{1}^{k}(x)}{\theta_{k}},\quad
F_{2}[V_{k}]+\lambda\tau_{2}(x)U_{k}^{p}=\frac{f_{2}^{k}(x)}{\theta_{k}^{p}}\quad\textrm{
in }\,\Omega,$

and $\|U_{k}\|_{\infty}=1$ for all $k$. Hence $\|V_{k}\|_{\infty}\leq C$ by
Theorem 3.4 for scalar equations. Thus, by $C^{1,\alpha}$ estimates one gets
that
$\|U_{k}\|_{C^{1,\alpha}(\overline{\Omega})},\|V_{k}\|_{C^{1,\alpha}(\overline{\Omega})}\leq
C$. Extracting a subsequence if necessary we may assume $U_{k}\to U$ and
$V_{k}\to V$ in $C^{1}(\overline{\Omega})$. Passing to limits, through
stability of viscosity solutions we end up with $U,V\geq 0$ in $\Omega$
satisfying

$\displaystyle\textstyle F_{1}[U]+\lambda\tau_{1}(x)V^{q}=0,\quad
F_{2}[V]+\lambda\tau_{2}(x)U^{p}=0\quad\textrm{ in }\,\Omega,$

with $U,V=0$ on $\partial\Omega$ and $\|U\|_{\infty}=1$. Since $F_{1}[U]\leq
0$, by SMP for scalar equations we have $U>0$ in $\Omega$. Whence
$F_{2}[V]=-\lambda\tau_{2}(x)U^{p}\lneqq 0$, from which also $V>0$ in
$\Omega$. By Corollary 4.3 one derives $U=t\phi_{1}^{+}$ and $V=t^{q}\psi^{q}$
in $\Omega$, which contradicts the fact that $U,V$ satisfy

$\displaystyle\textstyle F_{1}[U]+\lambda_{1}^{+}\tau_{1}(x)V^{q}\gneqq
0,\qquad F_{2}[V]+\lambda_{1}^{+}\tau_{2}(x)U^{p}\gneqq 0\;\;\textrm{ in
}\,\Omega,$

since $\lambda<\lambda_{1}^{+}$. If instead
$\left\|v_{k}\right\|_{\infty}\to\infty$ as $k\to\infty$ the argument is
analogous, by taking $\theta_{k}=\left\|v_{k}\right\|_{\infty}^{q}$. Therefore
one proves (8.12). Thus, again by $C^{1,\alpha}$ estimates, compact inclusion,
and stability of viscosity solutions one finds a nonnegative limit solution
pair $u,v\in C^{1,\alpha}(\overline{\Omega})$ of (1.4).

Step 3) General weights $\tau_{1},\tau_{2}\in L^{\varrho}_{+}(\Omega)$ and
general nonpositive $f\in L^{\varrho}(\Omega)$.

This case is very similar to the preceding step, by arguing via uniform bounds
and stability arguments. It is enough to pick up sequences of uniformly
positive weights $\tau^{k}_{1},\tau^{k}_{2}$ such that
$\tau_{1}^{k}\to\tau_{1}$ and $\tau_{2}^{k}\to\tau_{2}$ in
$L^{\varrho}(\Omega)$. By Step 2, we then take $u_{k},v_{k}\geq 0$ solving

$\displaystyle F_{1}[u_{k}]+\lambda\tau_{1}^{k}(x)v_{k}^{q}=f_{1}(x),\quad
F_{2}[v_{k}]+\lambda\tau_{2}^{k}(x)u_{k}^{p}=f_{2}(x)\quad\textrm{ in
}\,\Omega,$

with $u_{k}=v_{k}=0$ on $\partial\Omega$. Again one produces (8.12) by arguing
exactly as in Step 2. Thus, $C^{1,\alpha}$ estimates, compact inclusion, and
stability of viscosity solutions conclude the proof. ∎

##  9 An application: Isaac’s operators

In this section we prove that Isaac’s operators in the form (1.18) are
examples for which all our results are new even in the scalar case. In order
to do so, it is enough to prove that they satisfy (H4). We recall that the
$W^{2,\varrho}$ regularity results in [37] were extended in [49, Theorem 5.2]
to the context of unbounded coefficients and superlinear gradient growth, but
only for convex or concave operators. It is known that the same proof there
works if the corresponding pure second order operator $F(x,0,0,X)$ enjoys
$C^{1,1}$ regularity estimates, see [50, Remark 4.4] for instance.

The pure Isaac’s operator associated to (1.18) is again in the form (1.18)
with $\gamma_{s,t},\vartheta_{s,t}\equiv 0$ for all $s,t$. It is worth
mentioning that $C^{1,1}$ regularity estimates do not hold in general for
these operators, see [35]. On the other hand, in [31] the authors weakened the
$C^{1,1}$ hypothesis to a $W^{2,p}$ one. More recently in [38], regularity is
proved for Isaac’s operators with bounded drifts. Here we extend the preceding
results to unbounded weights. This is of independent interest in view of
applications [22, 23] to more general models driven by unbounded data.

As in [38], we assume that there exists $\bar{A}_{t}$ satisfying:

$\displaystyle|A_{s,t}(x)-\bar{A}_{t}(x)|\leq\epsilon_{1}\quad\textrm{
uniformly in }\,x,s,t$ (9.1)

where $\epsilon_{1}$ is the number of condition $A_{2}$ in [38], with
$\bar{A}_{t}\in C(\overline{\Omega})$ unifomly in $t\in\mathbb{N}$. In this
case the corresponding homogeneous Belmann operators generated by
$\bar{A}_{t}$ have $W^{2,q}$ regularity estimates for $q>\varrho>n$, see [14].

######  Proposition 9.1 ($W^{2,\varrho}$ regularity estimates for Isaac’s
operators).

Let $\Omega\subset{\mathbb{R}^{N}}$ be a bounded $C^{1,1}$ domain, $f\in
L^{\varrho}(\Omega)$, $\varrho>N$, and assume (9.1). Then any viscosity
solution $u\in C(\Omega)$ of

$I[u]=f(x)$ in $\Omega$, where
$I[u]=\inf_{s\in\mathbb{R}}\sup_{t\in\mathbb{R}}L_{s,t}$ or
$I[u]=\sup_{s\in\mathbb{R}}\inf_{t\in\mathbb{R}}L_{s,t}$

where $L_{s,t}$ satisfies (1.19), belongs to
$W^{2,\varrho}_{\mathrm{loc}}(\Omega)$ and satisfies the estimate

$\displaystyle\|u\|_{W^{2,\varrho}(\Omega^{\prime})}\leq
C\,\\{\|u\|_{L^{\infty}(\Omega)}+\|f\|_{L^{p}(\Omega)}\\},\;\;\textrm{ for all
}\Omega^{\prime}\subset\subset\Omega,$

where $C$ depends only on $N,\varrho,\alpha,\beta$,
$\|\gamma\|_{L^{\varrho}(\Omega)}$, $\|\vartheta\|_{L^{\varrho}(\Omega)}$,
$\Omega^{\prime}$, $\mathrm{dist}(\Omega^{\prime},\partial\Omega)$, and
$\mathrm{diam}(\Omega)$.

If in addition $u=\psi$ on $\partial\Omega$, for some $\psi\in
W^{2,\varrho}(\Omega)$, then $u\in W^{2,\varrho}(\Omega)$ and

$\displaystyle\|u\|_{W^{2,\varrho}(\Omega)}\leq
C\,\\{\|u\|_{L^{\infty}(\Omega)}+\|f\|_{L^{p}(\Omega)}+\|\psi\|_{W^{2,\varrho}(\Omega)}\\},$

where $C$ depends only on $N,\varrho,\alpha,\beta$,
$\|\gamma\|_{L^{\varrho}(\Omega)}$, $\|\vartheta\|_{L^{\varrho}(\Omega)}$,
$\partial\Omega$, and $\mathrm{diam}(\Omega)$.

###### Proof.

To fix the ideas we consider the first expression for $I$; the second case is
identical. Let $\gamma_{k},\vartheta_{k}\in L^{\infty}_{+}(\Omega)$, $f_{k}\in
C(\Omega)$, be such that $f_{k}\rightarrow f$, $\gamma_{k}\rightarrow\gamma$
and $\vartheta_{k}\rightarrow\vartheta$ in $L^{\varrho}(\Omega)$, with
$\gamma_{k}\leq\gamma$, $\vartheta_{k}\leq\vartheta$, and $|f_{k}|\leq|f|$. Up
to a subsequence, one can choose $\ell_{k}=\ell-\varepsilon_{k}>0$ for some
$\varepsilon_{k}\in(0,\ell)$, $\varepsilon_{k}\to 0$, such that

$\ell_{k}<\lambda_{1}^{+}(\mathcal{L}^{+}_{k}(\vartheta_{k}),\Omega)$, where
$\mathcal{L}_{k}^{+}[w]=\mathcal{M}^{+}(D^{2}w)+\gamma_{k}(x)|Dw|$

and $\ell$ as in (1.19). Note that $u\in
C^{1,\alpha_{0}}_{\mathrm{loc}}(\Omega)$ by Proposition 2.8. Let $u_{k}\in
C^{1,\alpha_{1}}(\overline{B}_{\varrho})$ be a viscosity solution of

$\displaystyle I_{k}[u_{k}]=f_{k}(x)\;\textrm{ in }B_{\rho},\quad
u_{k}=u\;\textrm{ on }\partial B_{\rho},$ (9.2)

given by Proposition 3.8, where $B_{\rho}$ is centered at $x_{0}\in\Omega$,
and

$I_{k}[w]:=\inf_{s\in\mathbb{R}}\sup_{t\in\mathbb{R}}L_{s,t}$, where
$L_{s,t}[w]=\mathrm{tr}(A_{s,t}(x)D^{2}w)+\gamma_{s,t}(x)|Dw|+\ell_{k}\vartheta_{s,t}(x)w$,

with $A_{s,t}$ as in (1.19), but now $|\gamma_{s,t}|\leq\gamma_{k}$ and
$|\vartheta_{s,t}|\leq\vartheta_{k}$ for all $s,t\in\mathbb{R}$.

Note that [48, Corollary 1.6] implies that $u_{k}$ is a viscosity solution of

$\inf_{s\in\mathbb{R}}\sup_{t\in\mathbb{R}}\mathrm{tr}(A_{s,t}(x)D^{2}u_{k})=g_{k}(x)$,
where $|g_{k}(x)|\leq|f|+\gamma(x)|Du_{k}|+\vartheta(x)|u_{k}|\in
L^{\varrho}(B_{\rho})$.

By [38, Theorem 1.1] one has $u_{k}\in
W^{2,\varrho}_{\mathrm{loc}}(B_{\rho})$, see also [1]. Now by the second part
of Proposition 3.8, we know that $u_{k}$ is the unique viscosity solution of
(9.2).

By the generalized Nagumo’s lemma in [37, Lemma 4.4] one gets

$\displaystyle\|u_{k}\|_{W^{2,\varrho}(B_{r})}\leq
C_{k}\,\\{\|u_{k}\|_{L^{\infty}(B_{\rho})}+\|f\|_{L^{\varrho}(B_{\rho})}\\},\;\textrm{
for all }r<\rho,$ (9.3)

where $C_{k}$ remains bounded, since $\gamma_{k}$ and $\vartheta_{k}$ are
bounded in $L^{\varrho}(B_{\rho})$. Moreover, since

$\ell_{k}<\lambda_{1}^{+}(\mathcal{L}_{k}^{+}(\vartheta_{k}),\Omega)\leq\lambda_{1}^{+}(\mathcal{L}_{k}^{+}(\vartheta_{k}),B_{\rho})\leq\lambda_{1}^{-}(\mathcal{L}_{k}^{+}(\vartheta_{k}),B_{\rho})$,

then one may apply ABP-MP and ABP-mP in Theorem 3.4 to obtain
$\|u_{k}\|_{L^{\infty}(B_{\rho})}\leq\|u\|_{L^{\infty}(\partial
B_{\rho})}+C\,\|f\|_{L^{\varrho}(B_{\rho})}$; again the constant does not
depend on $k$. This and (9.3) yield $\|u_{k}\|_{W^{2,\varrho}(B_{r})}\leq C$.
Hence there exists $v\in C^{1}(\overline{B}_{r})$ such that $u_{k}\rightarrow
v$ in $C^{1}(\overline{B}_{r})$, for all $r<\rho$. Note that
$\|u_{k}\|_{C^{1}(\overline{B}_{\rho})}\leq C$ by global $C^{1,\alpha_{1}}$
estimates in Proposition 2.8. Thus, Proposition 2.5 implies that $v$ is a
viscosity solution of

$\displaystyle I[v]=f(x)\;\textrm{ in }B_{\rho}\,,\quad v=u\;\textrm{ on
}\partial B_{\rho},$ (9.4)

Now, since $W^{2,\varrho}(B_{r})$ is reflexive, there exists $\tilde{v}\in
W^{2,\varrho}(B_{r})$ such that $u_{k}$ converges weakly to $\tilde{v}$. By
uniqueness of the limit, $\tilde{v}=v$ a.e. in $B_{r}$, and so $v\in
W^{2,\varrho}(B_{r})$, for all $r<\rho$.

Now, since $u$ is already a viscosity solution of (9.4), by using again the
uniqueness assertion in Proposition 3.8 one gets that $u\in
W^{2,\varrho}_{\mathrm{loc}}(B_{\rho})$. Since the ball $B_{\rho}$ is
arbitrary, and in each ball the solution is unique, a covering argument
produces $u\in W^{2,\varrho}_{\mathrm{loc}}(\Omega)$.

In the case of global regularity the argument is simpler, by taking $\Omega$
instead of $B_{\rho}$ in (9.2). ∎

Acknowledgments. We would like to thank Prof. A. Świȩch for his valuable
comments regarding our results on Isaac’s operators, and Prof. I. Biridelli
for kindly bringing reference [9] to our attention.

This project started during a visit of the first and second authors to the
University of Lisbon. They appreciate the invitation, hospitality, and support
provided by the Faculty of Sciences and FCT/Portugal.

## References

  * [1] P. D. Andrade, G. C. Rampasso, and M. S. Santos.  Geometric regularity theory for a time-dependent Isaacs equation.  arXiv preprint arXiv:2004.13806, 2020.
  * [2] A. Arapostathis, A. Biswas, and S. Saha.  Strict monotonicity of principal eigenvalues of elliptic operators in $\mathbb{R}^{d}$ and risk-sensitive control.  J. Math. Pures Appl. (9), 124:169–219, 2019.
  * [3] D. Arcoya and J. L. Gámez.  Bifurcation theory and related problems: anti-maximum principle and resonance.  Comm. Partial Differential Equations, 26(9-10):1879–1911, 2001\.
  * [4] S. N. Armstrong.  Principal eigenvalues and an anti-maximum principle for homogeneous fully nonlinear elliptic equations.  J. Differential Equations, 246(7):2958–2987, 2009.
  * [5] C. Bandle and W. Reichel.  Solutions of quasilinear second-order elliptic boundary value problems via degree theory.  In Stationary partial differential equations. Vol. I, Handb. Differ. Equ., pages 1–70. North-Holland, Amsterdam, 2004.
  * [6] H. Berestycki and L. Nirenberg.  On the method of moving planes and the sliding method.  Bol. Soc. Brasil. Mat. (N.S.), 22(1):1–37, 1991.
  * [7] H. Berestycki, L. Nirenberg, and S. R. S. Varadhan.  The principal eigenvalue and maximum principle for second-order elliptic operators in general domains.  Communications on Pure and Applied Mathematics, 47(1):47–92, 1994\.
  * [8] I. Birindelli.  Hopf’s lemma and anti-maximum principle in general domains.  J. Differential Equations, 119(2):450–472, 1995.
  * [9] I. Birindelli, E. Mitidieri, and G. Sweers.  Existence of the principal eigenvalue for cooperative elliptic systems in a general domain.  Differ. Uravn., 35(3):325–333, 429, 1999.
  * [10] D. Bonheure, J. Földes, E. Moreira dos Santos, A. Saldaña, and H. Tavares.  Paths to uniqueness of critical points and applications to partial differential equations.  Trans. Amer. Math. Soc., 370(10):7081–7127, 2018.
  * [11] D. Bonheure and E. Moreira dos Santos.  Representation theorems for Sobolev spaces on intervals and multiplicity results for nonlinear ODEs.  J. Differential Equations, 249(12):3148–3173, 2010.
  * [12] J. Busca, M. J. Esteban, and A. Quaas.  Nonlinear eigenvalues and bifurcation problems for Pucci’s operators.  Ann. Inst. H. Poincaré Anal. Non Linéaire, 22(2):187–206, 2005.
  * [13] L. Caffarelli, M. G. Crandall, M. Kocan, and A. Swiech.  On viscosity solutions of fully nonlinear equations with measurable ingredients.  Comm. Pure Appl. Math., 49(4):365–397, 1996.
  * [14] L. A. Caffarelli and X. Cabré.  Fully nonlinear elliptic equations, volume 43 of American Mathematical Society Colloquium Publications.  American Mathematical Society, Providence, RI, 1995.
  * [15] A. Carioli and R. Musina.  The homogeneous Hénon-Lane-Emden system.  NoDEA Nonlinear Differential Equations Appl., 22(5):1445–1459, 2015\.
  * [16] P. Clément and L. A. Peletier.  An anti-maximum principle for second-order elliptic operators.  J. Differential Equations, 34(2):218–229, 1979.
  * [17] A. Córdoba.  The Kakeya maximal function and the spherical summation multipliers.  Amer. J. Math., 99(1):1–22, 1977.
  * [18] A. Córdoba.  The multiplier problem for the polygon.  Ann. of Math. (2), 105(3):581–588, 1977.
  * [19] F. Da Lio and B. Sirakov.  Symmetry results for viscosity solutions of fully nonlinear uniformly elliptic equations.  J. Eur. Math. Soc. (JEMS), 9(2):317–330, 2007.
  * [20] R. Dalmasso.  Existence and uniqueness of positive solutions of semilinear elliptic systems.  Nonlinear Anal. Ser. A: Theory Methods, 39(5):559–568, 2000.
  * [21] D. G. de Figueiredo.  Positive solutions of semilinear elliptic problems.  In Differential equations (Sao Paulo, 1981), volume 957 of Lecture Notes in Math., pages 34–87. Springer, Berlin-New York, 1982.
  * [22] P. Felmer, A. Quaas, and B. Sirakov.  Landesman-Lazer type results for second order Hamilton-Jacobi-Bellman equations.  J. Funct. Anal., 258(12):4154–4182, 2010.
  * [23] P. Felmer, A. Quaas, and B. Sirakov.  Resonance phenomena for second-order stochastic control equations.  SIAM J. Math. Anal., 42(3):997–1024, 2010.
  * [24] H. Ishii and Y. Yoshimura.  Demi-eigenvalues for uniformly elliptic Isaacs operators.  preprint, 2005.
  * [25] S. Koike and A. Świȩch.  Weak Harnack inequality for fully nonlinear uniformly elliptic PDE with unbounded ingredients.  J. Math. Soc. Japan, 61(3):723–755, 2009.
  * [26] S. Koike and A. Świȩch.  Maximum principle for fully nonlinear equations via the iterated comparison function method.  Mathematische Annalen, 339(2):461–484, 2007.
  * [27] S. Koike and A. Świȩch.  Maximum principle for fully nonlinear equations via the iterated comparison function method.  Mathematische Annalen, 339(2):461–484, 2007.
  * [28] S. G. Krantz.  A panorama of harmonic analysis, volume 27 of Carus Mathematical Monographs.  Mathematical Association of America, Washington, DC, 1999.
  * [29] M. A. Krasnoselskii.  Positive solutions of operator equations.  Translated from the Russian by Richard E. Flaherty; edited by Leo F. Boron. P. Noordhoff Ltd. Groningen, 1964.
  * [30] E. J. F. Leite and M. Montenegro.  Maximum and comparison principles to Lane-Emden systems.  Journal of the London Mathematical Society, 101(1):23–42, 2020\.
  * [31] D. Li and K. Zhang.  $W^{2,p}$ interior estimates of fully nonlinear elliptic equations.  Bull. Lond. Math. Soc., 47(2):301–314, 2015.
  * [32] M. Montenegro.  The construction of principal spectral curves for Lane-Emden systems and applications.  Ann. Scuola Norm. Sup. Pisa Cl. Sci. (4), 29(1):193–229, 2000.
  * [33] E. Moreira dos Santos.  On the existence of positive solutions for a nonhomogeneous elliptic system.  Port. Math., 66(3):347–371, 2009.
  * [34] E. Moreira dos Santos, G. Nornberg, and N. Soave.  On unique continuation principles for some elliptic systems.  Ann. Inst. H. Poincaré Anal. Non Linéaire, 38(5):1667–1680, 2021.
  * [35] N. Nadirashvili and S. Vlăduţ.  Singular solutions of Hessian fully nonlinear elliptic equations.  Adv. Math., 228(3):1718–1741, 2011.
  * [36] G. Nornberg.  Methods of the regularity theory in the study of partial differential equations with natural growth in the gradient.  PhD thesis, PUC-Rio, 2018.
  * [37] G. Nornberg.  $C^{1,\alpha}$ regularity for fully nonlinear elliptic equations with superlinear growth in the gradient.  J. Math. Pures Appl. (9), 128:297–329, 2019.
  * [38] E. A. Pimentel.  Regularity theory for the Isaacs equation through approximation methods.  Ann. Inst. H. Poincaré Anal. Non Linéaire, 36(1):53–74, 2019.
  * [39] E. A. Pimentel and E. V. Teixeira.  Sharp Hessian integrability estimates for nonlinear elliptic equations: an asymptotic approach.  J. Math. Pures Appl. (9), 106(4):744–767, 2016.
  * [40] P. Poláčik, P. Quittner, and P. Souplet.  Singularity and decay estimates in superlinear problems via Liouville-type theorems. I. Elliptic equations and systems.  Duke Math. J., 139(3):555–579, 2007.
  * [41] A. Quaas.  Existence of a positive solution to a “semilinear” equation involving Pucci’s operator in a convex domain.  Differential Integral Equations, 17(5-6):481–494, 2004.
  * [42] A. Quaas and B. Sirakov.  Principal eigenvalues and the Dirichlet problem for fully nonlinear elliptic operators.  Adv. Math., 218(1):105–135, 2008.
  * [43] A. Quaas and B. Sirakov.  Solvability of monotone systems of fully nonlinear elliptic PDE’s.  C. R. Math. Acad. Sci. Paris, 346(11-12):641–644, 2008.
  * [44] B. Sirakov.  Solvability of uniformly elliptic fully nonlinear PDE.  Archive for Rational Mechanics and Analysis, 195(2):579–607, 2010\.
  * [45] B. Sirakov.  Boundary Harnack estimates and quantitative strong maximum principles for uniformly elliptic PDE.  Int. Math. Res. Not. IMRN, (24):7457–7482, 2018.
  * [46] B. Sirakov and P. Souplet.  The Vázquez maximum principle and the Landis conjecture for elliptic PDE with unbounded coefficients.  Adv. Math., 387:Paper No. 107838, 27, 2021.
  * [47] P. Souplet.  The proof of the Lane-Emden conjecture in four space dimensions.  Adv. Math., 221(5):1409–1427, 2009.
  * [48] A. Świȩch.  ${W}^{1,p}$-interior estimates for solutions of fully nonlinear, uniformly elliptic equations.  Advances in Differential Equations, 2(6):1005–1027, 1997.
  * [49] A. Świȩch.  Pointwise properties of ${L}^{p}$-viscosity solutions of uniformly elliptic equations with quadratically growing gradient terms.  Disc. Cont. Dyn. Systems-A, 40(5):2945–2962, 2020.
  * [50] N. Winter.  $W^{2,p}$ and $W^{1,p}$-estimates at the boundary for solutions of fully nonlinear, uniformly elliptic equations.  Z. Anal. Anwend., 28(2):129–164, 2009.