A Complete Approximation Theory for Weighted Transition Systems
Translated title
Term
4. term
Education
Publication year
2015
Submitted on
2015-06-01
Pages
32
Abstract
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.
Keywords
Documents