Prime congruences and Krull dimension for additively idempotent semirings

We propose a definition for prime congruences which allows us to define Krull dimension of a semiring as the length of the longest chain of prime congruences. We give a complete description of prime congruences in the polynomial and Laurent polynomial semirings over the tropical semifield $\mathbb{R}_{\max}$, the semifield $\mathbb{Z}_{\max}$ and the Boolean semifield $\mathbb{B}$. We show that the dimension of the polynomial and Laurent polynomial semiring over these idempotent semifields is equal to the number of variables plus the dimension of the ground semifield. We extend this result to all additively idempotent semirings. We relate this notion of Krull dimension to dimension of tropical varieties.