A Complete Approximation Theory for Weighted Transition Systems

Studenteropgave: Kandidatspeciale og HD afgangsprojekt

  • Peter Christoffersen
  • Mathias Ruggaard Pedersen
  • Mikkel Hansen
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
Udgivelsesdato1 jun. 2015
Antal sider32
ID: 213391375