Mikkel Hansen ; Kim Guldstrand Larsen ; Radu Mardare ; Mathias Ruggaard Pedersen - Reasoning About Bounds in Weighted Transition Systems

lmcs:4345 - Logical Methods in Computer Science, November 26, 2018, Volume 14, Issue 4 - https://doi.org/10.23638/LMCS-14(4:19)2018
Reasoning About Bounds in Weighted Transition SystemsArticle

Authors: Mikkel Hansen ; Kim Guldstrand Larsen ; Radu Mardare ; Mathias Ruggaard Pedersen

    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.


    Volume: Volume 14, Issue 4
    Published on: November 26, 2018
    Accepted on: November 14, 2018
    Submitted on: March 6, 2018
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,F.4.1,F.1.1
    Funding:
      Source : OpenAIRE Graph
    • Learning, Analysis, SynthesiS and Optimization of Cyber-Physical Systems; Funder: European Commission; Code: 669844

    1 Document citing this article

    Consultation statistics

    This page has been seen 1540 times.
    This article's PDF has been downloaded 543 times.