Counting to infinity: Graded modal logic with an infinity diamond

We extend the languages of both basic and graded modal logic with the infinity diamond, a modality that expresses the existence of infinitely many successors having a certain property. In both cases we define a natural notion of bisimilarity for the resulting formalisms, that we dub ML^∞ and GML^∞;, respectively. We then characterise these logics as the bisimulation-invariant fragments of the naturally corresponding predicate logic, viz., the extension of first-order logic with the infinity quantifier. Furthermore, for both ML^∞ and GML^∞; we provide a sound and complete axiomatisation for the set of formulas that are valid in every Kripke frame, we prove a small model property with respect to a widened class of weighted models, and we establish decidability of the satisfiability problem.