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.
Language | English |
---|---|
Publication date | 1 Jun 2015 |
Number of pages | 32 |