A Complete Approximation Theory for Weighted Transition Systems

Student thesis: Master Thesis and HD Thesis

  • Peter Christoffersen
  • Mathias Ruggaard Pedersen
  • Mikkel Hansen
4. term, Computer Science, Master (Master Programme)
In this paper we explore a proof theoretic approach to approximate reasoning about weighted transition systems. We introduce generalized weighted transition systems (GTS) as an extension of the classical notion of a weighted transition system by replacing exact transition weights with intervals over non-negative real numbers. We define a modal logic over GTSs that can reason about said intervals by taking operators known from probabilistic logics and adjusting their interpretation for a weighted context. Semantically we can then describe whether a transition with at least some weight or at most some weight can be taken to a state satisfying some property. We show that our logic has the Hennesy-Milner property, i.e. it is semantically invariant under an appropriate bisimulation relation. As our main contribution we provide a sound and weak-complete axiomatization of our logic. To achieve the completeness result we have used a common technique for modal and Markovian logics involving the construction of a canonical model.
Publication date1 Jun 2015
Number of pages32
ID: 213391375