一句话：提出加权迁移系统中转移权重上下界的推理方法，定义更粗互模拟，并给出模态逻辑、完全公理化与可判定性。
论文研究加权迁移系统（WTS）中转移权重的最小值与最大值推理。作者提出一种基于权重边界的互模拟，它比经典互模拟更粗：若状态可经转移到达同一互模拟类，且权重落在相同边界内，则它们被视作等价。为刻画这种等价，论文设计了一种定制模态逻辑，用特殊模态表达转移权重的数值上下界，并证明该逻辑在所提互模拟下不变。进一步，论文证明该逻辑具有有限模型性质，给出完全公理化系统，并利用 tableau 方法证明其可满足性问题是可判定的。
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.
@article{paperbot352,
title = {Reasoning About Bounds in Weighted Transition Systems},
author = {Mikkel Hansen and Kim Guldstrand Larsen and Radu Mardare and Mathias Ruggaard Pedersen},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:19)2018}
}