Cyril Grunspan

Ricardo Pérez-Marco

The mathematics of Bitcoin

1 Introduction to Bitcoin.

Bitcoin is a new decentralized payment network that started operating in January 2009. This new technology was created by a pseudonymous author, or group of authors, called Satoshi Nakamoto in an article that was publically released [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF] in the cypherpunk mailing list. The cypherpunks are anarchists and cryptographers that who have been concerned with personal privacy in the Internet since the 90's. This article follows on a general presentation of Bitcoin by the second author [START_REF] Pérez-Marco | Bitcoin and decentralized trust protocols[END_REF]. We refer to this previous article for general background. Here we focuss on mathematics being a feature of the security and effectiveness of Bitcoin protocol.

Roughly speaking the Bitcoin's protocol is a mathematical algorithm on a network which manages transaction data and builds majority consensus among the participants. Thus, if a majority of the participants are honest, then we get an honest automatic consensus. Its main feature is decentralization, which means that no organization or central structure is in charge. The nodes of the network are voluntary participants that enjoy equal rights and obligations. The network is open and anyone can participate. Once launched the network is resilient and unstopable. It has been functioning permanently without significant interruption since january 2009.

The code and development are open. The same code has been reused and modified to create hundreds of other cryptocurrencies based on the same principles. The security of the network relies on strong cryptography (several orders of magnitude stronger than the cryptography used in classical financial services). For example, classical hash functions (SHA256, RIPEMD-160) and elliptic curve digital signatures algorithm (ECDSA) are employed. The cryptography used is very standard and well known, so we will dwell on the mathematics of these cryptographic tools, but interesting cryptographical research is motivated by the special features of other cryptocurrencies.

Nodes and mining.

The Bitcoin network is composed by nodes, that correspond to the Bitcoin program running on different machines, that communicate with their neighbourds. Properly formatted Bitcoin transactions flood the network, and are checked, broadcasted and validated continuously by the nodes which follow a precise set of rules. There is no way to force the nodes to follow these rules. Incentives are created so that any divergence from the rules is economically penalised, thus creating a virtuous cycle. In this way, the network is a complex Dynamical System and it is far from obvious that it is stable. The stability of this system is a very interesting and fundamental mathematical problem. In its study we will encounter special functions, martingale theory, Markov chains, Dyck words, etc.

Nodes in the network broadcast transactions and can participate in their validation. The process of validating transac- tions is also called "mining" because it is related to the production of new bitcoins. The intuition behind Bitcoin is that of a sort of "electronic gold" and the rate of production of bitcoins is implemented in the protocol rules. On average every 10 minutes a block of transactions is validated and new bitcoins are minted in a special transaction without bitcoin input, called the coinbase transaction. At the beginning 50 B were created in each block, and about every 4 years (more precisely, every 210 000 blocks), the production is divided by 2. This event is called a "halving". So far, we had two halvings, and the production is currently set at 12.5 B per 10 minutes, or 1 800 B per day. The next halving will occur on May 2020. This geometric decrease of the production limits the total amount of bitcoins to 21 millions. Currently, about 18 millions have already been created. Each block containing the validated transactions can contain about 3 to 4 thousand transactions and has a size of about 1 Mb. These blocks are linked together cryptographically, and the set of all these blocks forms the "blockchain" that contains the full history of Bitcoin transactions. This data is stored efficiently, and the current blockchain is only about 260.000 Mb. The cryptographical link between blocks is provided by the mining/validation procedure that is based on a hash function and a "Proof-of-Work". It costs computation power to validate a block and this is what ensures that the data cannot be tampered or corrupted. In order to modify a single bit of a block, we must redo all computations that has been used to build all the subsequent blocks until the last current one. Currently the computation power needed to change only the last few blocks of the more than 600 thousands composing the blockchain is beyond the capabilities of any state or company.

The mining/validation procedure is a sort of decentralized lottery. A miner (this is a node engaging in validating transactions) packs together a block of floating not yet validated transactions, and builds a header of this block that contains a hash of the previous block header. The hash algorithm used is SHA-256 (iterated twice) that outputs 256 bits. Mathematically, a hash function is a deterministic one way function:

It is easy to compute, but practically impossible to find preimages, or collisions (two files giving the same output). Also it enjoys pseudo-random properties, that is, if we change a bit of the input, the bits of the output behave as uncorrelated random variables taking the values 0 and 1 with equal probabilities. The mining procedure consists of finding a hash that is below a pre-fixed threshold, which is called the difficulty. The difficulty is updated every two weeks (or more precisely every 2016 blocks) so that the rate of validation remains at 1 block per 10 minutes. The pseudo-random properties of the hash function ensure that the only way to find this hash is to probe many hashes by changing a parameter in the header (the nonce). The first miner to find a solution makes the block public, and the network adopts the block as the last block in the blockchain.

It can happen that two blocks are simultaneously validated in different parts of the network. Then a competition follows between the two candidates, and the first one to have a mined block on top of it wins. The other one is discarded and is called an orphan block. The blockchain with the larger amount of work (which is in general the longer one) is adopted by the nodes.

When a transaction is included in the last block of the blockchain, we say that it has one confirmation. Any extra block mined on top of this one gives another confirmation to the transaction and engraves it further inside the blockchain.

This apparently complicated procedure is necessary to ensure that neither the network nor the blockchain cannot be corrupted. Any participant must commit some computer power in order to participate in the decision of validation. The main obstacle for the invention of a decentralised currency was to prevent double spend without a central accounting authority. Hence, the first mathematical problem than Nakamoto considers in his founding article [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF] is to estimate the probability of a double spend. In the following we consider this and other stability problems, and prove mathematically the (almost general) stability of the mining rules.

2 The mining model.

We consider a miner with a fraction 0 < p ≤ 1 of the total hashrate. His profit comes from the block rewards of his validated blocks. It is important to know the probability of success when mining a block. The average number of blocks per unit of time that he succeeds mining is proportional to his hashrate p. The whole network takes on average τ 0 = 10 min to validate a block, hence our miner takes on average t 0 = τ 0 p . We consider the random variable T giving the time between blocks mined by our miner. The pseudo-random properties of the hash function shows that mining is a Markov process, that is, memoryless. It is then an elementary exercise to show from this property that T follows an exponential distribution,

f τ (t) = αe -αt
where α = 1/t 0 = 1/E[T]. If the miner starts mining at t = 0, and if we denote T 1 the time needed to mine a first block, then T 2 , . . . , T n the inter-block mining times of successive blocks, then the Markov property shows that the random variables T 1 , T 2 , . . . , T n are independent and are all identically distributed following the same exponential law. Therefore, the time needed to discover n blocks is

S n = T 1 + T 2 + . . . + T n .
The random variable S n follows the n-convolution of the exponential distribution and, as is well known, this gives a Gamma distribution with parameters (n, α),

f S n (t) = α n (n -1)! t n-1 e -αt
with cumulative distribution

F S n (t) = t 0 f S n (u)du = 1 -e -αt n-1 k=0 (αt) k k! .
From this we conclude that if N(t) is the process counting the number of blocks validated at time t > 0, N(t) = max{n ≥ 0; S n < t}, then we have

P[N(t) = n] = F S n (t) -F S n+1 (t) = (αt) n n! e -αt ,
and N(t) follows a Poisson law with mean value αt. This result is classical, and the mathematics of Bitcoin mining, as well as other crypto-currencies with validation based on proof of work, are Poisson distributions.

3 The double spend problem.

The first crucial mathematical problem that deserves attention in the Bitcoin protocol is the possibility of realisation of a double spend. This was the major obstacle to overcome for the invention of decentralized cryptocurrencies, thus it is not surprising that Nakamoto addresses this problem in Section 11 of his founding article [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF]. He considers the situation where a malicious miner makes a payment, then in secret tries to validate a second conflicting transaction in a new block , from the same address, but to a new address that he controls, which allows him to recover the funds. For this, once the first transaction has been validated in a block in the official blockchain and the vendor delivered the goods (the vendor will not deliver unless some confirmations are visible), the only possibility consists in rewriting the blockchain from that block. This is feasible if he controls a majority of the hashrate, that is, if his relative hashrate q satisfies q > 1/2, because then he is able to mine faster than the rest of the network, and he can rewrite the last end of the blockchain as he desires. This is the reason why a decentralised mining is necessary so that no one controls more than half of the mining power. But even when 0 < q < 1/2 he can try to attempt a double spend, and will succeed with a nonzero probability. The first mathematical problem consists of computing the probability that the malicious miner succeeds in rewriting the last n ≥ 1 blocks. We assume that the remaining relative hashrate, p = 1q, consists of honest miners following the protocol rules.

This problem is similar to the classical gambler's ruin problem. Nakamoto observes that the probaility to catch-up n blocks is

q n = q p n (Nakamoto)
The modelization of mining shows that the processes N(t) and N (t) counting the number of mined blocks at time t by the honest and malicious miners, respectively, are independent Poisson processes with respective parameters α et α satisfying

p = α α + α , q = α α + α .
The random variable X n = N (S n ) of the number of blocks mined by the attacker when the honest miners have mined their n-th block follows a negative binomial variable with parameters (n, p) ([3]), thus, for an integer k ≥ 1 we have

P[X n = k] = p k q k k + n -1 k .
Nakamoto, in section 11 of [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF], approximates abusively X n = N (S n ) by N (t n ) where

t n = E[S n ] = nE[T] = nτ 0 p
This means that he considers the classical approximation of a negative binomial variable by a Poisson variable. Rosenfeld observes in [START_REF] Rosenfeld | Analysis of hashrate-based double spending[END_REF] that the negative binomial variable seems to be a better approximation. We proved in [START_REF] Grunspan | Double spend races[END_REF] that this was indeed the case and we could find the exact formula for the double spend probability after z confirmations (z is the classical notation used by Nakamoto for the number of confirmations).

Theorem 1 ([3], 2017). After z confirmations, the probability of success of a double spend by attackers with a relative hashrate of 0 < q < 1/2 is

P(z) = I 4pq (z, 1/2)
where I x (a, b) is the incomplete regularized beta function

I x (a, b) = Γ(a + b) Γ(a)Γ(b) x 0 t a-1 (1 -t) b-1 dt .
Bitcoin security depends on this probability computation. It is not just a theoretical result. It allows the estimation of the risk of a transaction to be reversed and the number of confirmations required to consider it definitive. For example, if q = 0.1, after 6 confirmations, the probability of a double spend is smaller than 1% (for complete tables see [START_REF] Grunspan | Satoshi risk tables[END_REF]).

In his founding article, Nakamoto tries to compute this probability from his approximate argument and runs a numerical simulation. He convinced himself that the probability converges exponentially to 0 when the number of confirmations z goes to infinite (as he states "we can see the probability drop off exponentially with z"). The numerical simulation is not a proof, but we can read this statement repeated over and over, but never proved before 2017. With the previous exact formula, using classical methods (Watson Lemma), we can prove the following Corollary: Corollary 1. Let s = 4pq < 1. When z → +∞ the probability P(z) decays exponentially, and, more precisely, One can obtain higher order asymptotics in the classical way, or by using equivalent combinatorical methods as in [START_REF] Giogladis | A combinatorial-probabilistic analysis of bitcoin attacks[END_REF] We can be more precise by looking at the time it takes to the honest network to mine z blocks. A longer duration than the average τ 1 = zτ 0 leaves extra time for the attacker to build his replacement blockchain, and with this conditional knowledge the probability changes. If we define κ = τ 1 zτ 0 , we can compute this probability P(z, κ) and we can also obtain an exact formula using the regularized incomplete Gamma function

P(z) ∼ s z √ π(1 -s)z .
Q(s, x) = Γ(s, x) Γ(x) where Γ(s, x) = +∞ x t s-1 e -t dt
is the incomplete Gamma function.

Theorem 2. We have

P(z, κ) = 1 -Q(z, κ z q/p) + q p z e κ z p-q p Q(z, κ z) ,
Figure 2 shows the graphs of κ → P(z, κ) for different values of z.

Mining profitability.

After the study of the security of the protocol, the next important problem is its stability. For a decentralized protocol it is fundamental that the interests of the individuals are properly aligned with the protocol rules. In particular, the maximal gain of miners should be achieved when following the protocol rules. This is far from obvious, and we know from the study of unstable Dynamical Systems that this is hard to achieve. It is somewhat surprising that this has been empirically verified since Bitcoin's inception.

For example, it is by no means obvious that is in the best interest of a miner to publish immediately a block that he has validated. He can keep it secret and secretly push his advantage, but then he runs the risk that another miner publishes a validated block and the public blockchain adopts it thus loosing his reward. This type of scenario has been discussed since 2012 in bitcointalk forum, created by Nakamoto in 2010.

To answer this question, we first need to develop a proper profitability model. As in any business, mining profitability is accounted by the "Profit and Loss" per unit of time. The profits of a miner come from the block rewards that include the coinbase reward in new bitcoins created, and the transaction fees of the transactions in the block. The profitability at instant t > 0 is given by

PL(t) = R(t) -C(t) t
where R(t) and C(t) represent, respectively, the rewards and the cost of the mining operation up to time t. If we don't consider transaction fees we have

R(t) = N(t) b
where b > 0 is the coinbase reward. If we include transaction fees, the last equation remains true taking the average reward using the classical Wald Theorem.

The random variable C(t) representing the cost of mining operations is far more complex to determine since it depends on external factors (as electricity costs, mining hardware costs, geographic location, currency exchange rate, etc). But, fortunately, we don't need it in the comparison the profitability of different mining strategies as we explain next.

The mining activity is a repetitive and the miners returns to the same initial state after some time, for instant, start mining a fresh block. A mining strategy is composed by cycles where the miner invariably returns to the initial state. It is a "game with repetition" similar to those employed by profit gamblers in casino games (when they can spot a weakness that makes the game profitable). For example, an honest miner starts a cycle each time the network, he or someone else, has validated a new block.

We denote by τ the duration of the cycle, and we are interested in integrable strategies for which E[τ] < +∞ (this means that the cycles almost surely end up in finite time). Then it is easy to check, using the law of large numbers and Wald Theorem, that the long term profitability is given a.s. by the limit

PL ∞ = lim t→+∞ R(t) -C(t) t = E[R] -E[C] E[τ]
As observed before the second cost term is hard to compute, but the revenue term, that we call revenue ratio, is in general computable

Γ = E[R] E[τ]
For example, for an honest miner we have E[R] = p.0 + q.b = qb and E[τ] = τ 0 , and therefore

Γ H = qb τ 0
We have the fundamental Theorem on comparison of mining strategies with the same cost ratio. This is the case when both strategies use the full mining power at all time.

Theorem 3 ([7], 2018). We consider two mining strategies ξ and η with the same cost by unit of time. Then ξ is more profitable than η if and only if

Γ η ≤ Γ ξ 5 Protocol stability.
We can now mathematically study the protocol stability. The following remarkable result (remarkable because it is hard to imagine how Nakamoto could have foreseen it) validates the proper adjustment of the protocol: Theorem 4 ([7], 2018). In absence of difficulty adjustment, the optimal mining strategy is to publish immediately all mined blocks as soon as they are discovered.

We remind that the difficulty of mining adjusts in about every two weeks, so at the same time we spot a weakness of the protocol that we discuss below.

This Theorem holds true for any hashrate of the miner and without any assumption of the type of miners present in the network. It changes nothing that eventually there are some dishonest miners in the network.

The proof is simple and is a good example of the power of martingale techniques. For a constant difficulty, the average speed of block discovery remains constant and the counting process N(t) is a Poisson process with intensity α = p τ 0 where p is the relative hashrate of the miner. The cycle duration τ is a stopping time and the revenue per cycle equals to R = N (τ). Its mean value is then obtained using Doob's stopping time to the martingale N(t) -αt. Finally we get Γ ≤ Γ H .

But the Bitcoin protocol does have a difficulty adjustment algorithm that is necessary, in particular during the development phase. Theorem 4 shows that this is the only vector of attack. This difficulty adjustment provides a steady monetary creation and ensures that the interblock validation time stays at around 10 minutes. A minimum delay is necessary to allow a good synchronization of all network nodes. If the hashrate accelerates without a difficulty adjustment, then the nodes will desynchronise, and many competing blockchains will appear leaving a chaotic state.

6 Profitability of rogue strategies.

In view of Theorems 3 and 4, and in order to decide if a mining strategy is more profitable than the honest strategy, we only need to compute the revenue ratio Γ with the difficulty adjustment integrated. Selfish mining (SM strategy 1) is an example of rogue strategy. Instead of publishing a new block, the miner keeps the block secret and tries to build a longer blockchain increasing its advantage. When he makes it public, he will orphan the last mined honest blocks and will reap the rewards. To be precise, the attack cycles are defined as follows: the miner starts mining a new block on top of the official blockchain. If an honest miner finds a block first, then the cycle ends and he starts over. Otherwise, when he is the first to find a block, he keeps mining on top of it and keeping it secret. If before he mines a second block the honest network mines one public block, then he publishes his block immediately, thus trying to get a maximum proportion 0 < γ < 1 of honest miners adopting his block. The propagation is not instantaneous and the efficiency depends on the new parameter γ which represents his good connectivity to the network. A competition follows, and if the next block is mined on top of the honest block, then the selfish miner looses the rewards of this block and the attack cycle ends. If he, or his allied honest miners, mine the next block, then they publish it and the attack cycle ends again. If the attacker succeeds in mining two consecutive secret blocks at the beginning, then he continues working on his secret blockchain until he has only one block of advantage with respect to the public blockchain. In that case, he doesn't run any risk of being joined by the public blockchain and publishes all his secret blockchain, thus reaping all the rewards and ending the attack cycle again. In few words, the rogue miner spends most of his time replacing honest blocks by those that he mined in advance and kept secret. The mean duration E[τ] of the attack cycle is obtained as a variation of the following result about Poisson processes.

Proposition 5 (Poisson races). Let N and N be two independent Poisson processes with respective parameters α and α , with α < α and N(0) = N (0) = 0. Then, the stopping time

σ = inf{t > 0; N(t) = N (t) + 1}
is almost surely finite, and we have

E[σ] = 1 α -α , E[N (σ)] = α α -α , E[N(σ)] = α α -α .
The proof is a simple application of Doob's Stopping Time Theorem. Here, N and N are the counting processes of blocks mined by the honest miners and the attacker. To finish, we must compute the intensities α and α . At the beginning we have α = α 0 = p τ 0 and α = α 0 = q τ 0 where p is the apparent hashrate of the honest miners and q the one of the attacker. But the existence of a selfish miner perturbs the network and slows down the production of blocks. Instead of having one block for each period τ 0 , the progression of the official blockchain is of

E[N(τ) ∨ N (τ)] blocks during E[τ].
After validation of 2016 official blocks, this triggers a difficulty adjustment that can be important. The new difficulty is obtained from the old one by multiplication by a factor δ < 1 given by

δ = E[N(τ) ∨ N (τ)] τ 0 E[τ]
After the difficulty adjustment, the new mining parameters are α = α 1 = α 0 δ and α = α 1 = α 0 δ . The stopping time τ and the parameter δ can be computed using the relation |N(τ) -N (τ)| = 1. This can be used to compute the revenue ratio of the strategy [START_REF] Grunspan | On the profitability of selfish mining[END_REF]. This analysis can also checked by mining simulators.

An alternative procedure consists in modelling the network by a Markov chain where the different states correspond to different degree of progress of the selfish miner. Each transition corresponds to a revenue increase π and π for the honest and selfish miner. By another application of the Law of Large Numbers we prove that the long term apparent hashrate of the strategy, defined as the proportion of mined blocks by the selfish miner compared to the total number of blocks, is given by the formula

q = E[π ] E[π] + E[π ]
The expectation is taken relative to the stationnary probability that exists because the Markov chain is transitive and recurrent. Indeed, the Markov chain is essentially a random walk on N partially reflexive on 0. The computation of this stationnary probability proves the following Theorem: Theorem 6 ([8], 2014). The apparent hashrate of the selfish miner is

q = ((1 + pq)(p -q) + pq)q -(1 -γ)p 2 q(p -q) p 2 q + p -q
The results from [START_REF] Grunspan | On the profitability of selfish mining[END_REF] and [START_REF] Eyal | Majority is not enough: Bitcoin mining is vulnerable[END_REF] obtained by these different methods, are compatible. The revenue ratio Γ 1 and the apparent hashrate q are related by the following equation

Γ 1 = q b τ 0
But the first analysis is finer since it does explain the change of profitability regime after the difficulty adjustment. In particular, it allows to compute the duration before running into profitability for the attacker. The selfish miner starts by losing money, then after the difficulty adjustment that favors him, starts making profits. For example, with q = 0.1 and γ = 0.9, he needs to wait 10 weeks in order to be profitable. This partly explains why such an attack has never been observed in the Bitcoin network. Theorem 3 gives an explicit semi-algebraic condition on the parameters, namely q > q, that determines the values of the parameters q and γ for which the selfish mining strategy is more profitable than honest mining.

Theorem 4 shows that the achilles' heel of the protocole is the difficulty adjustment formula. This formula is supposed to contain the information about the total hashrate, but in reality it ignores the orphan blocks. The authors proposed a solution that incorporates this count, and this solves the stability problem of the protocol [START_REF] Grunspan | On the profitability of selfish mining[END_REF].

There are other possible block-withholding strategies that are variations of the above strategy [START_REF] Nayak | Stubborn mining: Generalizing selfish mining and combining with an eclipse attack[END_REF]. These are more agressive strategies. In the initial situation where the attacker succeeds to be two blocks ahead, instead of publishing the whole secret chain when he is only one block ahead, he can wait to be caught-up to release his blocks and then starts a final competition between the two competing chains. The attack cycle ends when the outcome is decided. This is the "Lead Stubborn Mining" (LSM, strategy 2). In this strategy it is important that the miner regularly publishes his secret blocks with the same height of the official blockchain, to attract part of the honest miners in order to take out hashrate from the pool of honest miners. Also in this way, even if he looses the final competition he will succeed in incorporating some of his blocks in the official blockchain and reap the corresponding rewards.

Another even more agressive variation consists in waiting not to be caught up but to be behind one block. This is the "Equal Fork Stubborn Mining Strategy" (EFSM, strategy 3). Here again, it is important to publish secret blocks regularly. Finally, the authors have considered another more agressive variation where the stubborn miner follows EFSM but then doesn't stop when he is one block behind. He keeps on mining until his delay becomes greater than a threshold A or until he successfully comes from behind, catches-up and finally takes the advantage over the official blockchain.

This strategy seems desperate, because the official blockchain progress is faster, on average. But in case of catching-up the selfish miner wins the jackpot of all the blocks he replaces. This is the "A-Trailing Mining" strategy (A-TM, strategy 4). The authors of [START_REF] Nayak | Stubborn mining: Generalizing selfish mining and combining with an eclipse attack[END_REF] conduct a numerical study of profitability by running a Montecarlo simulation and compare the profitability of the different strategies for different parameter values (q, γ). But we can find closed form formulas for the revenue ratio of all these strategies using the precedent martingale approach.

Theorem 7. ( [START_REF] Grunspan | On the profitability of selfish mining[END_REF][START_REF] Grunspan | On the profitability of stubborn mining[END_REF][START_REF] Grunspan | On the profitability of trailing mining[END_REF][START_REF] Grunspan | Bitcoin selfish mining and Dyck words[END_REF]) We have

Γ 1 Γ H = (1 + pq)(p -q) + pq -(1 -γ)p 2 (p -q) p 2 q + p -q Γ 2 Γ H = p + pq -q 2 p + pq -q - p(p -q) f (γ, p, q) p + pq -q Γ 3 Γ H = 1 p - p -q pq f (γ, p, q) Γ 4 Γ H = 1 + (1-γ)p(p-q) (p+pq-q 2 )[A+1] [A -1] + 1 p P A (λ) [A+1] λ 2 - 2 √ 1-4(1-γ)pq+p-q p+pq-q p+pq-q 2 + (1-γ)pq p+pq-q 2 (A + λ) 1 [A+1] -1 A+λ with f (γ, p, q) = 1 -γ γ • 1 - 1 2q (1 -1 -4(1 -γ)pq) and λ = q/p, [n] = 1-λ n 1-λ pour n ∈ N, P A (λ) = 1-Aλ A-1 +Aλ A+1 -λ 2A
(1-λ) 3 We can plot the parameter regions where each startegy is the best one (Figure 3). The Catalan numbers appear naturally in the computations.

C n = 1 2n + 1 2n n = (2n)! n!(n + 1)! .
For this reason their generating function appears in the formulas

C(x) = +∞ n=0 C n x n = 1 - √ 1 -4x 2x
We observe that 1 -4pq = pq and C(pq) = 1/p, and this justifies the definition of new probability distributions that arise in the proofs.

P[X = n] = pq 2 C n-1 (pq) n-1 .
7 Dyck words.

We can recover this results by a direct combinatorical approach representing each attack cycle by a Dyck word.

Definition 9. A Dyck word is a word built from the two letter alphabet {S , H} which contains as many S letters as H letters, and such that any prefix word contains more or equal S letters than H letters. We denote D the set of Dyck words, and for n ≥ 0, D n the subset of Dyck worlds of length 2n.

The relation to Catalan numbers is classical: the cardinal of D n is C n . We can encode attack cycles by a chronologic succession of block discoveries (disregarding if the blocks are made public or not). For a selfish block we use the letter S (for "selfish") and for the honest blocks the letter H (for "honest").

The link between the selfish mining strategy and Dyck words is given by the following proposition: Proposition 10. The attack cycles of the SM strategy are H, SHH, SHS, and SSwH where w ∈ D.

At the end of the cycle, we can summarise and count the total number of official blocks, say L, and how many of these blocks were mined by the attacker, say Z. Then, for strategy 1 (SM), the random variable L-1 follows a Catalan distribution of the third type, and except for some particular cases (when L < 3), we always have L = Z. The apparent hashrate q is then given by the formula:

q = E[Z] E[L]
We can then directly recover Theorem 6 by this simpler combinatorical procedure [START_REF] Grunspan | Bitcoin selfish mining and Dyck words[END_REF]. The other rogue strategies can be studied in a similar way. The Catalan distribution of the first type arises in the study of the strategy EFSM (strategy 3), and the one of the second type for the strategy LSM (strategy 2). We can then recover all the results given by the Markov chain analysis. Unfortunately we cannot recover the more finer results obtained by martingales techniques. This sort analysis applies to other Proof-of-Work cryptocurrencies, and to Ethereum that has a more complex reward system and a different difficulty adjustment formula [START_REF] Grunspan | Selfish mining in Ethereum[END_REF].

8 Nakamoto double spend revisited.

We come back to the fundamental double spend problem from Nakamoto Bitcoin paper discussed in section 3. In that section, we computed the probability of success of a double spend. But now, with the profitability model knowledge from section 4, we can study its profitability and get better estimates on the number of confirmations that are safe to consider a paiement definitive. The double spend strategy as presented in [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF] is unsound because there is a non-zero probability of failure and in that case, if we keep mining in the hope of catching-up from far behind the official blockchain, we have a positive probability of total ruin. Also the strategy is not integrable since the expected duration of the attack is infinite. Thus, we must obviously put a threshold to the unfavorable situation where we are lagging far behind the official blockchain.

We assume that the number of confirmations requested by the recipient of the transaction is z and we assume that we are never behind A ≥ z blocks of the official blockchain. This defines an integrable strategy, The A-Nakamoto double spend strategy. Putting aside technical details about premining, the probability of success of this strategy is a modification of the probability from Theorem 1 Theorem 11 ([14], 2019). After z confirmations, the probability of success of an A-Nakamoto double spend is P A (z) = P(z) -λ A 1 -λ A where P(z) is the probability from Theorem 1 and λ = q/p.

If v is the amount to double spend, then we can compute the revenue ratio

Γ A = E[R]/E[τ].
Theorem 12 ([14], 2019). With the previous notations, the expected revenue and the expected duration of the A-Nakamoto double spend strategy is

E[R A ]/b = qz 2p
I 4pq (z, 1/2) -Aλ A p(1 -λ) 3 [A] 2 I (p-q) 2 (1/2, z)

+ 2 -λ + λ A+1 (1 -λ) 2 [A]
p z-1 q z B(z, z)

+ P A (z) v b + 1 E[T A ]/τ 0 = z 2p I 4pq (z, 1/2) + A p(1 -λ) 2 [A]
I (p-q) 2 (1/2, z) -p z-1 q z p(1 -λ) B(z, z) + 1 q with the notation [n] = 1-λ n 1-λ for an integer n ≥ 0, and B is the classical Beta function. In principle a powerful miner does not have an interest in participating in a large double spend, since doing so will undermine the foundations of his business. For a small miner with relative hashrate 0 < q << 1 we can estimate the minimal amount of a double spend to be profitable. For this we only need to use the inequality from Theorem 3, Γ A ≥ Γ H = qb/τ 0 , and take the asymptotics q → 0 (with A and z being fixed, but the final result turns out to be independent of A).

Corollary 13. When q → 0 the minimal amount v for an Nakamoto double spend with z ≥ 1 confirmations is

v ≥ q -z 2 2z-1 z b = v 0 .
For example, in practice, with a 10% hashrate, q = 0.01, and only one confirmation, z = 1, we need to double spend more than v 0 /b = 50 coinbases. With the actual coinbase reward of b = 12.5 B bitcoins and the actual prize over 8.300 euros, this represents more than 5 millions euros.

Hence for all practical purposes and normal amount transactions, only one confirmation is enough to consider the transaction definitive.

Conclusions. Bitcoin provides a good example of the universality of Mathematical applications and its potential to impact our society. With the glimpse we have given, we hope to have convinced our colleagues that the Bitcoin protocol also motivates some exciting Mathematics.

Figure 1 :

 1 Figure 1: The Bitcoin logo.

Figure 2 :

 2 Figure 2: Probabilities P(z, κ) for q = 0.1 and distinct values of z.

Figure 3 :

 3 Figure 3: Comparison of HM, SM, LSM, EFSM and A-TSM.

Definition 8 .

 8 A discrete random variable X taking integer values follows a Catalan distribution of the first type if we have, for n ≥ 0, P[X = n] = C n p(pq) n . It follows a Catalan distribution of the second type if P[X = 0] = p and for n ≥ 1, P[X = n] = C n-1 (pq) n . It follows a Catalan distribution of the third type if P[X = 0] = p, P[X = 1] = pq + pq 2 and for n ≥ 2,

Figure 4 :

 4 Figure 4: Graph of Γ A , for z = 2, v = b and A = 3, 5, 10.


Pedro Cabalar

Jorge Fandinno

Torsten Schaub
email: torsten@cs.uni-potsdam.de

Sebastian Schellhorn

Lower Bound Founded Logic of Here-and-There

A distinguishing feature of Answer Set Programming is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There, whose equilibrium models correspond to stable models. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. This idea was generalized by Aziz to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In this paper, we present a logical reconstruction of Aziz' idea in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables along with its equilibrium models and elaborate upon its formal properties. Finally, we compare our approach with related ones and sketch future work.

Motivation

A distinguishing feature of Answer Set Programming (ASP; [START_REF] Baral | Knowledge Representation, Reasoning and Declarative Problem Solving[END_REF]) is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There (HT; [START_REF] Heyting | Die formalen Regeln der intuitionistischen Logik[END_REF]), whose equilibrium models correspond to stable models [START_REF] Pearce | Equilibrium logic[END_REF]. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. Thus, in analogy to [START_REF] Leone | Disjunctive stable models: unfounded sets, fixpoint semantics, and computation[END_REF][START_REF] Van Gelder | The well-founded semantics for general logic programs[END_REF] foundedness in ASP can be understood by minimizing values of Boolean variables. This idea was generalized in [START_REF] Aziz | Answer set programming: founded bounds and model counting[END_REF] to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In fact, ASP follows the rationality principle, which says that we shall only believe in things, we are forced to [START_REF] Gelfond | Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach[END_REF]. While this principle amounts to foundedness in the propositional case, there are at least two views of statements such as x ≥ 42. First, we may accept any value greater or equal than 42 for x. Second, we may only consider value 42 for x, unless there is a reason for a greater value. Arguably, the latter corresponds to the idea of foundedness in ASP.

The ASP literature contains several approaches dealing with atoms containing variables over non-Boolean domains [7,8,[START_REF] Janhunen | Clingo goes linear constraints over reals and integers[END_REF] but these approaches do not comply with foundedness in our sense. For instance, approaches to Constraint ASP (CASP) like [7] only allow for atoms with variables over non-Boolean domains in the body of a rule. Thus, these atoms and the values of non-Boolean variables cannot be founded in terms of ASP.

Approaches like [8,[START_REF] Janhunen | Clingo goes linear constraints over reals and integers[END_REF] focus on foundedness on an atom level and allow for almost any kind of atoms in heads and bodies. They match the view of the rationality principle that accepts any value satisfying a statement like x ≥ 42. This permits assignments over non-Boolean domains to be founded but the variables are not necessarily assigned to the smallest value that can be justified. The following examples point out the difference of the two views of the rationality principle. Moreover, we show that taking any value satisfying a statement as a rational choice together with separate minimization will not yield foundedness in terms of ASP. Consider the rules

x ≥ 0 y ≥ 0 x ≥ 42 ← y < 42 (1)
The approach presented in [8] produces the following result. The first two rules alone would generate any arbitrary pair of positive values for x and y, but the last rule further restricts x ≥ 42 when the choice for y satisfies y < 42. It is clear that this last rule causes the range of x to depend on the value of y.

Unfortunately, this dependence disappears if we try to minimize variable values a posteriori by imposing a Pareto minimality criterion on the solutions. If we do so, we get a first minimal solution with y → 0 and x → 42 which somehow captures the expected intuition: we first decide the minimal value of y (which does not depend on x) assigning 0 to y and then apply the third rule to conclude x ≥ 42 obtaining the minimal value 42 for x. However, among the solutions of (1), we also get those in which we chose y ≥ 42, so the third rule is not applicable and x ≥ 0. Therefore, we get a second Pareto-minimal solution with y → 42 and x → 0 that seems counter intuitive: as y does not depend on x there seems to be no reason to assign a minimal value other than 0 to y. To show that separate minimization on solutions does not always yield all (and possibly more) solutions as expected by foundedness, consider the rules

x ≥ 1 x ≥ 42 ← ¬(x ≤ 1) (2)
In this case, depending on whether we assume ¬(x ≤ 1) or not, we may get two founded solutions. By assuming x ≤ 1, the second rule is disabled and the first rule x ≥ 1 determines the founded minimal value 1 for x, still compatible with the assumption x ≤ 1. If, on the contrary, we assume ¬(x ≤ 1), then the second rule imposes x ≥ 42 determining the minimal value 42 for x that, again, confirms the assumption ¬(x ≤ 1). In other words, we expect two founded solutions with x → 1 and x → 42, respectively. In contrast, if we first apply [8] and then a Pareto minimization, we lose the solution with x → 42. This is because when assuming x ≤ 1, we get x ≥ 1 as before, and the only compatible solution assigns 1 to x, whereas if we assume ¬(x ≤ 1), we obtain infinitely many values x ≥ 42 compatible with the assumption. The solutions are then x → 1 plus the infinite sequence x → 42, x → 43 and so on. Thus, the unique Pareto minimal solution assigns 1 to x.

On the other hand, Aziz' original approach to foundedness [START_REF] Aziz | Answer set programming: founded bounds and model counting[END_REF] has some counter intuitive behavior. In this approach, p ← ¬p alone yields a solution with p, unlike in traditional ASP. In view of this, we present in the following a logical reconstruction of Aziz' idea of foundedness in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables (HT LB for short) along with its equilibrium models. 1 We elaborate upon the formal properties of HT LB like persistence, negation and strong equivalence. 2 Furthermore, we point out the relation of HT LB to HT, and show that our approach can alternatively be captured via a Ferraris-style definition of stable models [START_REF] Ferraris | Answer sets for propositional theories[END_REF] adapted to our setting. Finally, we compare our approach with related work and point out the benefits of HT LB .

Background

Let A be a set of propositional atoms. A formula ϕ is a combination of atoms by logical connectives ⊥, ∧, ∨, and ←. As usual, we define ⊤ def = ⊥ → ⊥ and ¬ϕ def = ϕ → ⊥. A theory is a set of formulas.

We denote an interpretation over A by I ⊆ A and an HT-interpretation over A by H , T where H ⊆ T ⊆ A are interpretations. Since we want to abstract from the specific form of atoms, we rely upon denotations for fixing their semantics. A denotation of atoms in A is a function • A : A → 2 As usual, an equilibrium model of a theory Γ is a (total) HT-interpretation T , T such that T , T |= Γ and there is no H ⊂ T such that H , T |= Γ . Then, T is also called a stable model of Γ .

Let us recall some characteristic properties of HT. For HT-interpretations H , T and T , T and formula ϕ over A both H , T |= ϕ implies T , T |= ϕ (persistence) and H , T |= ϕ → ⊥ iff T , T |= ϕ (negation) holds. Furthermore, Γ 1 ∪ Γ and Γ 2 ∪ Γ have the same stable models for theories Γ 1 and Γ 2 and any theory Γ over A iff Γ 1 and Γ 2 have the same HT-models (strong equivalence).

Lower Bound Founded Logic of Here-and-There

In what follows, we introduce the logic of Here-and-There with lower bound founded variables, short HT LB , and elaborate on its formal properties.

HT LB Properties

The language of HT LB is defined over a set of atoms A X comprising variables, X , and constants over an ordered domain (D, ). For simplicity, we assume that each element of D is uniquely represented by a constant and abuse notation by using elements from D to refer to constants. Similarly, we identify with its syntactic representative. The specific syntax of atoms is left open but assumed to refer to elements of X and D. The only requirement is that we assume that an atom depends on a subset of variables in X . An atom can be understood to hold or not once all variables in it are substituted by domain elements. Clearly, variables not occurring in an atom are understood as irrelevant for its evaluation. Examples of ordered domains are ({0, 1, 2, 3}, ≥) and (Z, ≥), respectively; corresponding atoms are x = y and x ≥ 42. An example of a formula is 'y < 42 ∧ ¬(x = y) → x ≥ 42'. We let vars(ϕ) ⊆ X be the set of variables and atoms(ϕ) ⊆ A X the atoms occurring in a formula ϕ.

For capturing partiality, we introduce a special domain element u, standing for undefined, and extend (D, ) to (D u , u ) where

D u def = D ∪ {u} and u def = ∪ {(c, u) | c ∈ D u }.
With it, we define a (partial) valuation over X , D as a function v : X → D u mapping each variable to a domain value or undefined. For comparing valuations by set-based means, we alternatively represent them by subsets of X × D. Basically, any function v is a set of pairs (x, c) such that v (x) = c for c ∈ D. In addition, we view a pair (x, c) as x c and add its downward closure (x ↓ c) def = {(x, d) | c, d ∈ D, c d}. Given this, a valuation v is represented by the set v (x)=c,x∈X (x ↓ c). 3 As an example, consider variables x and y over domain ({0, 1, 2, 3}, ≥). The valuation v = {x → 2, y → 0} can be represented by v = (x ↓ 2) ∪ (y ↓ 0) = {(x, 0), (x, 1), (x, 2), (y, 0)}. Then, v ′ = {x → 1, y → u}, viz. {(x, 0), (x, 1)} in set notation, can be regarded as "smaller" than v because v ′ ⊆ v . The comparison of two valuations v and v ′ by set-inclusion ⊆ amounts to a twofold comparison. That is, v and v ′ are compared regarding the occurrence of variables and their particular values wrt . We let V X ,D stand for the set of valuations over X and D.

We define the satisfaction of formulas over A X wrt atom denotations over X , D, which are functions • X ,D : A X → 2 V X ,D mapping atoms to sets of valuations. Let a be an atom of A X and a X ,D its denotation. Then, a X ,D is the set of valuations making a true. Since a depends on variables vars(a) ⊆ X , we have for each v ∈ a X ,D and valuation

v ′ with v (x) = v ′ (x) for x ∈ vars(a) that v ′ ∈ a X ,D .
Intuitively, values of X \ vars(a) may vary freely without changing the membership of a valuation to a X ,D . For simplicity, we drop indices X , D whenever clear from context.

For instance, interpreting the atoms x ≥ 42, 42 ≥ 0 and 0 ≥ 42 over (Z, ≥) yields the following denotations:

x ≥ 42 def = {v | v (x) ≥ 42} 42 ≥ 0 def = V 0 ≥ 42 def = ∅.
x ≥ 42 is the set of valuations assigning x to values greater or equal than 42 and all variables in X \ {x} take any value in D u , eg (x ↓ 45) and (x ↓ 45) ∪ (y ↓ 0) for y ∈ X \ {x} are possible valuations. Interestingly, atoms like x

x with x x = {v | v (x) = u} force variables to be defined over D per definition of . A valuation v is defined for a set of variables Y ⊆ X if v (x) = u for all x ∈ Y.

We define an HT LB -valuation over X , D as a pair h, t of valuations over X , D with h ⊆ t. We define satisfaction of formulas in HT LB as follows.

Definition 2. Let h, t be an HT LB -valuation over X , D and ϕ be a formula over A X . Then, h, t satisfies ϕ, written h, t |= ϕ, if the following holds:

1. h, t |= ⊥ 2. h, t |= a iff v ∈ a X ,D for atom a ∈ A X and for both v ∈ {h, t} 3. h, t |= ϕ 1 ∧ ϕ 2 iff h, t |= ϕ 1 and h, t |= ϕ 2 4. h, t |= ϕ 1 ∨ ϕ 2 iff h, t |= ϕ 1 or h, t |= ϕ 2 5. h, t |= ϕ 1 → ϕ 2 iff v , t |= ϕ 1 or v , t |= ϕ 2 for both v ∈ {h, t}
As usual, we call h, t an HT LB -model of a theory Γ , if h, t |= ϕ for all ϕ in Γ . For a simple example, consider the theory containing atom x ≥ 42 only. Then, every HT LB -valuation h, t with h, t ∈ x ≥ 42 is an HT LB -model of x ≥ 42. Note that, different to HT, satisfaction of atoms in HT LB forces satisfaction in both h and t, instead of h only. We discuss this in detail below when comparing to a Ferraris-like stable model semantics.

Our first result shows that the characteristic properties of persistence and negation hold as well when basing satisfaction on valuations and denotations. Proposition 2. Let h, t and t, t be HT LB -valuations over X , D, and ϕ be a formula over A X . Then, 1. h, t |= ϕ implies t, t |= ϕ, and 2. h, t |= ϕ → ⊥ iff t, t |= ϕ.

Persistence implies that all atoms satisfied by h, t are also satisfied by t, t . To make this precise, let At( h, t ) def = {a ∈ A X | h ∈ a and t ∈ a } be the set of atoms satisfied by h, t .

Corollary 1. Let h, t and t, t be HT LB -valuations over X , D. Then, At( h, t ) ⊆ At( t, t ).

Finally, we define an equilibrium model in HT LB . Definition 3. An HT LB -valuation t, t over X , D is an HT LB -equilibrium model of a theory Γ iff t, t |= Γ and there is no h ⊂ t such that h, t |= Γ .

We refer to an HT LB -equilibrium model t, t of Γ as an HT LB -stable model t of Γ . Let us reconsider the theory containing atom x ≥ 42 only. Then, t = (x ↓ 42) is an HT LB -stable model of x ≥ 42, since t ∈ x ≥ 42 and there is no h ⊂ t with h ∈ x ≥ 42 . In contrast, neither HT LB -model t ′ , t ′ with t ′ = (x ↓ 42) ∪ (y ↓ 0) nor t ′′ , t ′′ with t ′′ = (x ↓ 53) are HT LB -stable models since t is a proper subset of both and t, t ′ |= x ≥ 42 as well as t, t ′′ |= x ≥ 42 holds. Hence, HT LBstable models make sure that each variable is assigned to its smallest founded value.

Note that HT LB -equilibrium models induce the non-monotonic counterpart of the monotonic logic of HT LB . Following well-known patterns, we show that HT LB allows us to decide strong equivalence wrt HT LB -equilibrium models.

Proposition 3 (Strong Equivalence). Let Γ 1 , Γ 2 and Γ be theories over A X .

Then, theories Γ 1 ∪ Γ and Γ 2 ∪ Γ have the same HT LB -stable models for every theory Γ iff Γ 1 and Γ 2 have the same HT LB -models.

The idea is to prove the only if direction via contraposition, and the if direction by proving its direct implication. The contraposition assumes that there exists an HT LB -valuation that satisfies Γ 1 but not Γ 2 which implies that the stable models of Γ 1 ∪ Γ and Γ 2 ∪ Γ do not coincide. There are two cases to construct Γ in a way that Γ 1 ∪ Γ has a stable model which is not a stable model of Γ 2 ∪ Γ and the other way around. Consider an example to illustrate the idea of the construction of Γ . Let h = (x ↓ 0) and t = (x ↓ 2) ∪ (y ↓ 0) be HT LB -valuation over {x, y}, {0, 1, 2, 3} with h, t |= Γ 1 and h, t |= Γ 2 . For the first case, assume that t, t |= Γ 2 . Since t cannot be a model of Γ 2 ∪ Γ by assumption, we construct Γ in a way that t is a stable model of

Γ 1 ∪ Γ . Hence, let Γ = {z c | (z, c) ∈ t} = {x 0, x 1, x 2
, y 0} be the theory with the only stable model t. By persistence of h, t wrt Γ 1 and construction of Γ , we get that t is a stable model of Γ 1 ∪ Γ but not of Γ 2 ∪ Γ . For the second case, we assume t, t |= Γ 2 . Now, we construct Γ in a way that t is a stable model of Γ 2 ∪ Γ but not of Γ 1 ∪ Γ . By assumption, we have that h, t |= Γ 1 and h, t |= Γ 2 as well as t, t |= Γ 2 , thus we want to have h, t and v , v ′ with t ⊆ v ⊆ v ′ as the only models of Γ . Hence, let Γ = Γ ′ ∪ Γ ′′ with Γ ′ = {z c | (z, c) ∈ h} = {x 0} be the theory satisfied by everything greater or equal than h, and

Γ ′′ = {z t(z) → z ′ t(z ′ ), z c → z t(z) | (z, c), (z, t(z)), (z ′ , t(z ′ )) ∈ t \ h, z = z ′ } = {x 2 → y 0, y 0 → x 2, x 1 → x 2, x 2 → x 2}
the theory deriving values of t for each v ′′ with h ⊂ v ′′ ⊂ t. Since h, t |= Γ 2 and by construction of Γ , we get that t is a stable model of

Γ 2 ∪ Γ but not of Γ 1 ∪ Γ .
The following result shows that a formula a ← ¬a has no stable model if a cannot be derived by some other formula. Proposition 4. Let Γ be a theory over A X containing a formula of form a ← ¬a and for each HT LB -stable model v of Γ \ {a ← ¬a} over X , D we have that v , v |= a.

Then, Γ has no HT LB -stable model.

This proposition may seem to be trivial but we show in Sect. 4 that Aziz' original approach does not satisfy this property.

Negation in HT LB

In the following, we elaborate on complements of atoms and their relation to negation, since A X may contain atoms like x ≥ 42 and x < 42. Intuitively, the complement of an atom holds whenever the atom itself does not hold. This can be easily expressed by using atom denotations. More formally, the complement a of atom a is defined by its denotation a X ,D def = 2 V X ,D \ a X ,D . To illustrate that the simple complement of an atom is insufficient to yield something similar to strong negation let us take a closer look at propositional atoms in HT LB . For mimicking Boolean truth values, we consider the domain ({t, f }, {t f }). Then, the denotation of propositional atoms in HT LB can be defined as follows:

p = t A,{t,f } def = {v | v (p) = t} and p = f A,{t,f } def = {v | v (p) = f }.
Note that p = t and p = f are regarded as strong negations of each other, as in the standard case [START_REF] Gelfond | Logic programs with classical negation[END_REF]; their weak negations are given by ¬(p = t) and ¬(p = f ), respectively. For instance, the complement p = t is characterized by denotation

p = t A,{t,f } = 2 V A,{t,f } \ p = t A,{t,f } = {v | v (p) = t}.
However, this complement allows for valuations v with v (p) = u which are not in p = f A,{t,f } .

Let us define another complement to exclude assigning undefined to variables of an atom. First, we define a denotation a X ,D of an atom a as strict if each v ∈ a X ,D is defined for vars(a). Then, we characterize the strict complement a s of atom a by the strict denotation a s

X ,D def = 2 V X ,D \ ( a X ,D ∪ {v | v (x) =
u for some x ∈ vars(a)}). Informally, the strict complement of an atom holds whenever all variables are defined and the atom itself does not hold. That is, atoms p = f and p = t are strict complements of each other.

More generally, an atom with a strict denotation and its strict complement can be regarded as being strongly negated to each other. For instance, consider atom x ≥ 42 and its strict denotation x ≥ 42 X ,D = {v | v (x) ≥ 42}. Then, its strict complement x ≥ 42 s is defined by x ≥ 42 s X ,D = {v | u = v (x) < 42}. As in the Boolean case, the strict complement x ≥ 42 s can be seen as the strong negation of x ≥ 42. For making the relation of complements and negation precise, we define entailment: A theory Γ over A X entails a formula ϕ over A X , written Γ |= ϕ, if all HT LB -models of Γ are HT LB -models of ϕ. Then, we have the following result.

Proposition 5. Let a be an atom over A X , and a and a s its complement and its strict complement over A X , respectively. Then, {a s } |= a and {a} |= ¬a.

This implies that the strict complement a s of an atom a implies its negation ¬a, just as strong negation implies weak negation in the standard case [START_REF] Pearce | Equilibrium logic[END_REF]. To illustrate that in general the negation of an atom does not entail its complement, viz {¬a} |= a, consider atom x ≤ 42 with strict denotation x ≤ 42

X ,D = {v | u = v (x) ≤ 42}. Then, its complement x ≤ 42 is defined by x ≤ 42 X ,D = 2 V X ,D \ x ≤ 42 X ,D = {v | v (x) = u or v (x) > 42}.
For valuations h = (x ↓ 42) and t = (x ↓ 50), we have h, t |= ¬(x ≤ 42) since (x ↓ 50) ∈ x ≤ 42 X ,D . In contrast, h, t |= x ≤ 42, since (x ↓ 42) ∈ x ≤ 42 X ,D . Thus, the complement a can be seen as a kind of negation in between strong and weak negation.

HT LB versus HT

Analogously to [8], we next show that HT can be seen as a special case of HT LB . Note that both types of denotations p A in HT and p = t A,{t} in HT LB of a propositional atom p collect interpretations and valuations assigning true to p. To begin with, we define a transformation τ relating each propositional atom p with corresponding atom p = t by τ (p) def = p = t. Let Γ be a propositional theory, then τ (Γ ) is obtained by substituting each p ∈ atoms(Γ ) by τ (p). Moreover, we extend τ to interpretations I by τ (I ) def = {(p, t) | p ∈ I } to obtain a corresponding valuation over A, {t}. The next proposition establishes that HT can be seen as a special case of HT LB . Proposition 6. Let Γ be a theory over propositional atoms A and H , T an HT-interpretation over A. Let τ (Γ ) be a theory over atoms {p = t | p ∈ A} and τ (H ), τ (T ) an HT LB -valuation over A, {t}.

Then, H ,

T |= Γ iff τ (H ), τ (T ) |= τ (Γ ).
This can be generalized to any arbitrary singleton domain {d} and corresponding atoms p = d and the relationship still holds. We obtain the following result relating HT LB and HT:

Proposition 7. Let Γ be a theory over A X and h, t an HT LB -model of Γ over X , D. Then, At( h, t ), At( t, t ) is an HT-model of Γ over A X .

That is, the collected atoms satisfied by an HT LB -model of Γ can be seen as an HT-model of Γ by interpreting A X as propositional atoms. For instance, consider the theory containing only atom x = y and its denotation x = y def = {v | u = v (x) = v (y) = u}. Let h = (x ↓ 0) ∪ (y ↓ 4) and t = (x ↓ 0) ∪ (y ↓ 42) be valuations and hence At( h, t ) = At( t, t ) = {x = y} interpretations. Then, h, t |= x = y in HT LB and At( h, t ), At( t, t ) |= x = y in HT. Furthermore, we relate tautologies in HT and HT LB .

Proposition 8. Let ϕ be a tautology in HT over A and ϕ ′ a formula over A X obtained by replacing each atom in ϕ by an atom of A X . Then, ϕ ′ is a tautology in HT LB .

That is, tautologies in HT are independent of the form of atoms. For example, consider the well known tautology p → p over A. Then, x ≥ 42 → x ≥ 42 over A X is a tautology as well. Note that the other direction of the implication does not hold, since x ≥ 42 → y ≥ 42 over A X with domain {42} is a tautology, but p → q over A is not.

HT LB -stable versus Ferraris-style stable models

As mentioned, in Definition 2 satisfaction of atoms differs from HT by forcing satisfaction in both h and t, instead of h only. This is necessary to guarantee persistence in HT LB . To see this, consider an HT LB -valuation h, t satisfying atom a in A X . Hence, by persistence, HT LB -valuation t, t satisfies a as well. However, this does not necessarily mean that HT LB -valuations v , t with h ⊂ v ⊂ t satisfy a. For instance, consider atom x = 42 with x = 42 def = {v | u = v (x) = 42} and valuations h = (x ↓ 0) and t = (x ↓ 53). Then, h, t |= x = 42 and t, t

|= x = 42, but v , t |= x = 42 for v = (x ↓ 42) with h ⊂ v ⊂ t.
A question that arises now is whether HT LB behaves in accord with stable models semantics. To this end, we give straightforward definitions of classical satisfaction and the reduct by Ferraris [START_REF] Ferraris | Answer sets for propositional theories[END_REF] in our setting and show that equilibrium models correspond to stable models according to the resulting Ferraris-like stable model semantics.

We define the counterpart of classical satisfaction as follows.

Definition 4. Let t be a valuation over X , D and ϕ a formula over A X . Then, t satisfies ϕ, written t |= cl ϕ, if the following holds:

1. t |= cl ⊥ 2. t |= cl a iff t ∈ a X ,D for atom a ∈ A X 3. t |= cl ϕ 1 ∧ ϕ 2 iff t |= cl ϕ 1 and t |= cl ϕ 2 4. t |= cl ϕ 1 ∨ ϕ 2 iff t |= cl ϕ 1 or t |= cl ϕ 2 5. t |= cl ϕ 1 → ϕ 2 iff t |= cl ϕ 1 or t |= cl ϕ 2 .
We call t a classical model of a theory Γ , if t |= cl ϕ for all ϕ in Γ . Then, we define a Ferraris-like reduct for formulas over A X as follows.

Definition 5. Let ϕ be a formula over A X and t a valuation over X , D. Then, the reduct of ϕ wrt t, written ϕ t , is defined as

ϕ t def =      ⊥ if t |= cl ϕ a if t |= cl ϕ and ϕ = a is an atom in A X ϕ 1 t ⊗ ϕ 2 t if t |= cl ϕ and ϕ = (ϕ 1 ⊗ ϕ 2 ) for ⊗ ∈ {∧, ∨, →}
For theory Γ and HT LB -valuation t, we define Γ t def = {ϕ t | ϕ ∈ Γ }. Note that in case of propositional formulas our reduct corresponds to Ferraris' original [START_REF] Ferraris | Answer sets for propositional theories[END_REF].

With it, we define a Ferraris-like stable model as expected.

Definition 6. A valuation t over X , D is a Ferraris-like stable model of theory

Γ over A X iff t |= cl Γ t and there is no h ⊂ t such that h |= cl Γ t .
In analogy to the standard case [START_REF] Ferraris | Answer sets for propositional theories[END_REF], the next proposition shows that models in HT LB can be alternatively characterized in the style of Ferraris: Proposition 9. Let h, t be an HT LB -valuation over X , D and Γ a theory over

A X . Then, h |= cl Γ t iff h, t |= Γ .
As a special case, we obtain that every HT LB -stable model corresponds to a Ferraris-like stable model and vice versa.

Corollary 2. Let t be a valuation over X , D and Γ a theory over A X . Then, t is an HT LB -stable model of Γ iff t is a Ferraris-like stable model of Γ .

The last two results show that our logic follows well known patterns wrt different representations of stable models.

Modeling with Bound Founded Programs

In what follows, we define logic programs over linear constraint atoms to illustrate the modeling capabilities of HT LB on an example.

We define linear constraint atoms over the integers (Z, ≥) as

m i=1 w i x i ≺ k
where w i , k ∈ Z are constants, x i ∈ X are distinct variables, and ≺∈ {≥, ≤, =, =}4 is a binary relation. The denotation of a linear constraint atom is given by

m i=1 w i x i ≺ k def = {v | m i=1 w i v (x i ) ≺ k, v (x i ) = u}.
We denote the set of linear constraint atoms over variables X and domain (Z, ≥) by L X .

a 1 ∨ • • • ∨ a n ← l 1 ∧ • • • ∧ l n ′ (3)
where a i is a linear constraint atom for 1 ≤ i ≤ n and l j is a literal for 1 ≤ j ≤ n ′ . A logic program is a theory over L X of rules of form (3).

As an example, consider the dependency of the revolutions per minute (rpm) of the engine of our car to its maximal range. The maximal range of a car decreases with higher rpm; we need more fuel when choosing a smaller gear which increases the rpm assuming the same conditions like speed. For simplicity, we do not model gears, fuel or speed. Assume that our car needs at least 2000 rpm. Moreover, we know that our car has a range of at least 100 km. If we go by less than 4000 rpm, then our range is at least 200 km. Then, the following program P models the dependency of rpm and range without explicitly using negation or minimization: rpm ≥ 2000 range ≥ 100 range ≥ 200 ← rpm < 4000

The HT LB -stable model of P is (range ↓ 200) ∪ (rpm ↓ 2000), since 2000 is the minimal value satisfying rpm ≥ 2000 and thus rpm < 4000 holds and yields range ≥ 200. For instance, if we extend P by the new statement rpm ≥ 4000, then we get the HT LB -stable model (range ↓ 100) ∪ (rpm ↓ 4000), since the minimal value derived by rpm ≥ 4000 does not produce range ≥ 200 any more. Thus, 100 is the minimal value for range derived by range ≥ 100. Intuitively, it makes no sense to go by higher rpm and thus decrease the range if one is not forced to.

This example behaves similar to the example in [START_REF] Aziz | Answer set programming: founded bounds and model counting[END_REF]. The intuition is to minimize the value of rpm first since it does not depend on range. Afterwards, we derive the minimal value of range out of the obtained consequences. Note that this example can also be modeled by other approaches like [START_REF] Aziz | Answer set programming: founded bounds and model counting[END_REF]8], but those may not provide the same intuitive modeling to achieve a bound founded semantics or behave counter intuitive on some well known modeling techniques like integrity constraints. For instance, the approach of [8] yields solutions for P consisting of any arbitrary pair of values with rpm ≥ 2000 and range ≥ 100 where range is further restricted to values greater or equal to 200 if the choice of rpm is smaller than 4000. To achieve the same bound founded intuition as in HT LB with approaches like [8] we need to rewrite the rpm example in a less intuitive way. This is similar to representing formula p ← q under stable models semantics in propositional logic.

Related Work

We start by comparing our approach to Aziz' Bound Founded ASP (BFASP; [START_REF] Aziz | Answer set programming: founded bounds and model counting[END_REF]). Both aim at generalizing foundedness to ordered domains. In BFASP, an arbitrary formula is called constraint and a rule is defined as a pair of a constraint and a variable called head. The constraint needs to be increasing wrt its head variable. Informally, a constraint is increasing in a variable if the constraint is monotonic in this variable. Note that increasing is defined on constraints instead of atoms. For an example, the constraint x ≤ 42 is not increasing in x, but the constraint x ≤ 42 ← y < 0 is increasing in x over domain N. Stable models are defined in BFASP via a reduct depending on the monotonicity of constraints wrt their variables and by applying a fix point operation.

Both, BFASP and HT LB assign variables to their smallest domain value by default. Interestingly, they differ in their understanding of smallest domain values. In HT LB , the smallest domain value is always the value 'undefined' to capture partiality, whereas in BFASP partiality is not considered if undefined is not explicitly part of the domain.

The value of a head variable is derived by the constraint even if it contains no implication. For instance, consider rule (x + y ≥ 42, x) over N in BFASP. Then, BFASP yields one stable model with x → 42 and y → 0. By default the value of y is 0, since y appears nowhere as a head. The value of x is derived from the value of 42-y. In contrast, HT LB results in 43 stable models from (x ↓ 0)∪(y ↓ 42) to (x ↓ 42) ∪ (y ↓ 0) for theory {x + y ≥ 42}. In HT LB , the variables of an (head) atom are treated in an equal way instead of an implicatory way by declaring one of them as head.

As already mentioned, BFASP does not satisfy Proposition 4. Rule p ← ¬p has no stable model in ASP and HT LB , but BFASP yields a stable model containing p, since the BFASP reduct never replaces head variables and produces the rule as is and yields p as the minimal (and only) model of the rule. This means that BFASP provides a bound founded semantics but behaves unexpectedly on rules representing integrity constraints.

Next, we compare HT LB to the logic of HT with constraints (HT C ; [8]). First, note that both are based on HT and capture theories over (constraint) atoms in a non-monotonic setting and can thus express default values. The difference is that HT C follows the rationality principle by accepting any value satisfying an atom and thus foundedness is focused on atom level. Unlike this, foundedness in HT LB is focused on variable level by following the rationality principle in accepting minimal values only. The latter is achieved by additionally comparing models wrt the values assigned to variables to determine equilibrium models. For instance, reconsider the fact x ≥ 42 over {x}, N and valuations v and v ′ with v (x) = 42 and v ′ (x) = 43. Then, in HT C we have v = v ′ , whereas in HT LB we have v ⊂ v ′ . Hence, v and v ′ are solutions in HT C but only v is a solution in HT LB . The theories in (1) and [START_REF] Balduccini | Representing constraint satisfaction problems in answer set programming[END_REF] show that the semantics of HT LB cannot be obtained by adding separate minimization to HT C .

On the other hand, both HT LB and HT C define atomic satisfaction in terms of atom denotations. A difference is that in HT C denotations need to be closed. Informally, a denotation is (upwards) closed if it is closed under the superset relation. For HT LB , this cannot be maintained, due to the additional comparison of valuations regarding values. The closure of denotations is significant to satisfy persistence in HT C . In contrast, in HT LB persistence is established by forcing atomic satisfaction in both h and t, instead of h only as in HT C . The corresponding benefit is that this allows us to consider denotations of atoms in HT LB which are not allowed in HT C , like x . = y with x . = y def = {v | v (x) = v (y)} which is not closed in HT C .

The integration of non-Boolean variables into ASP is also studied in ASP modulo Theories [START_REF] Balduccini | Representing constraint satisfaction problems in answer set programming[END_REF][START_REF] Banbara | aspartame: solving constraint satisfaction problems with answer set programming[END_REF][START_REF] Banbara | Clingcon: the next generation[END_REF][START_REF] Bartholomew | System aspmt2smt: computing ASPMT theories by SMT solvers[END_REF]7,[START_REF] Drescher | A translational approach to constraint answer set solving[END_REF][START_REF] Gebser | Theory solving made easy with clingo 5[END_REF][START_REF] Gebser | Constraint answer set solving[END_REF][START_REF] Janhunen | Clingo goes linear constraints over reals and integers[END_REF][START_REF] Janhunen | Tight integration of non-ground answer set programming and satisfiability modulo theories[END_REF][START_REF] Lierler | SMT-based constraint answer set solver EZSMT (system description)[END_REF][START_REF] Liu | Answer set programming via mixed integer programming[END_REF]. The common idea of these hybrid approaches is to integrate monotone theories, like constraint or linear programming, into the non-monotonic setting of ASP. Similar to HT C , foundedness is only achieved at the atomic level-if at all. In fact, many approaches avoid this entirely by limiting the occurrence of theory atoms to rule bodies.

Finally, logic programs with linear constraints under HT LB 's semantics amount to a non-monotonic counterpart of Integer Linear Programming (ILP; [START_REF] Schrijver | Theory of linear and integer programming[END_REF]). As a matter of fact, the monotonicity of ILP makes it hard to model default values and recursive concepts like reachability. It will be interesting future work to see whether HT LB can provide a non-monotonic alternative to ILP.

Conclusion

We presented a logical reconstruction of the idea of foundedness over ordered domains in the setting of the logic of Here-and-There. We have shown that important properties like persistence, negation and strong equivalence hold in our approach. Also, we showed that HT is a special case of HT LB , and that HT LBstable models correspond to stable models according to a Ferraris'-like stable model semantics. We instantiated HT LB with linear constraints to illustrate its modeling capabilities by means of an example representing the dependency of the rpm of a car and its range. Finally, we compared our approach to related work to point out that foundedness is a non-trivial key feature of HT LB . Although HT LB and BFASP share the same motivation, they differ in their treatment of partiality. Furthermore, we indicated that HT LB can be seen as a non-monotonic counterpart of monotonic theories such as ILP.

Interestingly, HT LB offers a new view of aggregates under Ferraris' semantics as atoms. In fact, sum aggregates are related to linear constraint atoms in HT LB . As we will show in a follow-up work, aggregates under Ferraris' semantics [START_REF] Ferraris | Logic programs with propositional connectives and aggregates[END_REF] can be represented by atoms in HT LB . This is interesting since then aggregates are no longer an extension of an existing approach, but rather an integral atomic parts of HT LB . Hence, results shown in this work also apply to aggregates (under Ferraris' semantics) and provide a way to elaborate upon properties and relationships to other conceptions of aggregates. The view on aggregates as atoms provided by HT LB may thus help us to better understand the differences among various aggregate semantics.

  2 A mapping atoms in A to sets of interpretations over A. Accordingly,p A |= p iff H ∈ p A for propositional atom p ∈ A 3. H , T |= ϕ 1 ∧ ϕ 2 iff H , T |= ϕ 1 and H , T |= ϕ 2 4. H , T |= ϕ 1 ∨ ϕ 2 iff H , T |= ϕ 1 or H , T |= ϕ 2 5. H , T |= ϕ 1 → ϕ 2 iff I , T |= ϕ 1 or I , T |= ϕ 2 for both I ∈ {H , T } '. H , T |= p iff p ∈ H for propositional atom p ∈ AIt is easy to see that both definitions of HT satisfaction coincide. Proposition 1. Let H , T be an HT-interpretation and ϕ a formula over A.Then, H , T |= ϕ iff H , T |= ϕ by replacing Condition 2 by 2'.

	def = {I | p ∈ I }
	represents the set of interpretations where atom p holds.
	With it, we next define satisfaction of formulas in HT.
	Definition 1. Let H , T be an HT-interpretation over A and ϕ a propositional
	formula over A. Then, H , T satisfies ϕ, written H , T |= ϕ, if the following
	conditions hold:
	1. H , T |= ⊥
	2. H , T As usual, we call H , T an HT-model of a theory Γ , if H , T |= ϕ for all ϕ
	in Γ . The usual definition of HT satisfaction (cf. [23]) is obtained by replacing
	Condition 2 above by

1

Upper bound founded variables are treated analogously.

2

We provide an extended version including all proofs at: www.cs.uni-potsdam.de/ ∼ seschell/JELIA19-paper-proofs.pdf. 2

Note that (x ↓ u) = ∅, since u ∈ D.

As usual, w 1 x 1 , + • • • + w n x n < k and w 1 x 1 , + • • • + w n x n > k can be expressed by w 1 x 1 , + • • • + w n x n ≤ k -1 and w 1 x 1 , + • • • + w n x n ≥ k + 1, respectively.

Appendix of Proofs

Proof of Proposition 2. It is enough to prove the proposition for the base case, since the rest follows directly by structural induction for each formula over A X . Let h, t an HT LB -valuation over X , D and a atom of A X .

First, we prove persistence, represented by 1 of the proposition. We have

Proof of Proposition 5. Let a be an atom over A X , and a and a s its complement and its strict complement over A X , respectively. First, we prove a s |= a. For any HT LB -valuation h, t over X , D we have

Secondly, we prove a |= ¬a. For any HT LB -valuation h, t over X , D we have

It is enough to prove the proposition for the base case, since the rest follows directly by structural induction for each theory over A.

Let Γ be a theory over propositional atoms A and H , T an HTinterpretation over A. Let τ (Γ ) be a theory over atoms {p = t | p ∈ A} and τ (H ), τ (T ) an HT LB -valuation over A, {t}. Then we have

Proof of Proposition 7. It is enough to prove the proposition for the base case, since the rest follows directly by structural induction for each theory over A X .

First, note that the pair H , T over A X with H = At( h, t ) and T = At( t, t ) is a well formed HT-interpretation, since H ⊆ T holds by h ⊆ t and Proposition 1. Then we have

Proof of Proposition 9. It is enough to prove the proposition for the base case, since the rest follows directly by structural induction for each theory over A X .

Let Γ be a theory over A X and h, t an HT LB -valuation over X , D.