Complete proof systems for weighted modal logic (Q2253184)

Weighted Modal Logic (WML) is a multi-modal logic that expresses qualitative and quantitative properties of Weighted Transition Systems (WTS), i.e., the 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. Here, both weak-complete and strong-complete axiomatizations for WML against WTSs is proposed as well as a series of metatheorems including the finite model property and the existence of canonical models. It is shown how the proof system can be used in the context of a process algebra semantics for WML to convert a model-checking problem in to a theorem-proving problem.