Reasoning about bounds in weighted transition systems

Mikkel Hansen, Kim Guldstrand Larsen, Radu Mardare, Mathias Ruggaard Pedersen

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)
4 Downloads (Pure)


We propose a way of reasoning about minimal and maximal values of the weights of transitions in a weighted transition system (WTS). This perspective induces a notion of bisimulation that is coarser than the classic bisimulation: it relates states that exhibit transitions to bisimulation classes with the weights within the same boundaries. We propose a customized modal logic that expresses these numeric boundaries for transition weights by means of particular modalities. We prove that our logic is invariant under the proposed notion of bisimulation. We show that the logic enjoys the finite model property and we identify a complete axiomatization for the logic. Last but not least, we use a tableau method to show that the satisfiability problem for the logic is decidable.

Original languageEnglish
Article number19
Number of pages32
JournalLogical Methods in Computer Science
Issue number4
Publication statusPublished - 26 Nov 2018


  • axiomatization
  • bisimulation
  • completeness
  • finite model property
  • modal logic
  • satisfiability
  • weighted transition system


Dive into the research topics of 'Reasoning about bounds in weighted transition systems'. Together they form a unique fingerprint.

Cite this