Complete proof systems for weighted modal logic

The weighted transition systems (WTS) considered in this paper are transition systems having both states and transitions labeled with real numbers: the state labels denote quantitative resources, while the transition labels denote costs of transitions in terms of resources. Weighted Modal Logic (WML) is a multi-modal logic that expresses qualitative and quantitative properties of WTSs. While WML has been studied in various contexts and for various application domains, no proof system has been developed for it. In this paper we solve this open problem and propose both weak-complete and strong-complete axiomatizations for WML against WTSs. We prove a series of metatheorems including the finite model property and the existence of canonical models. We show how the proof system can be used in the context of a process-algebra semantics for WML to convert a model-checking problem into a theorem-proving problem. This work emphasizes a series of similarities between WML and the probabilistic/stochastic modal logics for Markov processes and Harsanyi type spaces, such as the use of particular infinitary rules to guarantee the strong-completeness.