On modal logics of linear inequalities

Abstract

We consider probabilistic modal logic, graded modal logic and stochastic modal logic, where linear inequalities may be used to express numerical constraints between quantities. For each of the logics, we construct a cut-free sequent calculus and show soundness with respect to a natural class of models. The completeness of the associated sequent calculi is then established with the help of coalgebraic semantics which gives completeness over a (typically much smaller) class of models. With respect to either semantics, it follows that the satisfiability problem of each of these logics is decidable in polynomial space.