Reasoning about bounds in weighted transition systems

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

Research output: Contribution to journalArticle

Abstract

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.

LanguageEnglish
Article number19
Number of pages32
JournalLogical Methods in Computer Science
Volume14
Issue number4
DOIs
Publication statusPublished - 26 Nov 2018

Fingerprint

Bisimulation
Transition Systems
Reasoning
Logic
Finite Models
Tableau
Satisfiability Problem
Axiomatization
Modal Logic
Numerics
Modality
Express
Invariant

Keywords

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

Cite this

Hansen, Mikkel ; Larsen, Kim Guldstrand ; Mardare, Radu ; Pedersen, Mathias Ruggaard. / Reasoning about bounds in weighted transition systems. In: Logical Methods in Computer Science. 2018 ; Vol. 14, No. 4.
@article{623f6c0932814d198bea0171746b87b1,
title = "Reasoning about bounds in weighted transition systems",
abstract = "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.",
keywords = "axiomatization, bisimulation, completeness, finite model property, modal logic, satisfiability, weighted transition system",
author = "Mikkel Hansen and Larsen, {Kim Guldstrand} and Radu Mardare and Pedersen, {Mathias Ruggaard}",
year = "2018",
month = "11",
day = "26",
doi = "10.23638/LMCS-14(4:19)2018",
language = "English",
volume = "14",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "4",

}

Reasoning about bounds in weighted transition systems. / Hansen, Mikkel; Larsen, Kim Guldstrand; Mardare, Radu; Pedersen, Mathias Ruggaard.

In: Logical Methods in Computer Science, Vol. 14, No. 4, 19, 26.11.2018.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Reasoning about bounds in weighted transition systems

AU - Hansen, Mikkel

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu

AU - Pedersen, Mathias Ruggaard

PY - 2018/11/26

Y1 - 2018/11/26

N2 - 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.

AB - 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.

KW - axiomatization

KW - bisimulation

KW - completeness

KW - finite model property

KW - modal logic

KW - satisfiability

KW - weighted transition system

UR - http://www.scopus.com/inward/record.url?scp=85060199198&partnerID=8YFLogxK

U2 - 10.23638/LMCS-14(4:19)2018

DO - 10.23638/LMCS-14(4:19)2018

M3 - Article

VL - 14

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 4

M1 - 19

ER -