Complete proof systems for weighted modal logic, Theor

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 vari-ous 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 mod-els. 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 prob-lem. This work emphasizes a series of similarities between WML and the probabilis-tic/stochastic modal logics for Markov processes and Harsanyi type spaces, such as the use of particular infinitary rules to guarantee the strong-completeness