摘要：We propose a way of reasoning about minimal and maximal values of the weightsof transitions in a weighted transition system (WTS). This perspective inducesa notion of bisimulation that is coarser than the classic bisimulation: itrelates states that exhibit transitions to bisimulation classes with theweights within the same boundaries. We propose a customized modal logic thatexpresses these numeric boundaries for transition weights by means ofparticular modalities. We prove that our logic is invariant under the proposednotion of bisimulation. We show that the logic enjoys the finite model propertyand we identify a complete axiomatization for the logic. Last but not least, weuse a tableau method to show that the satisfiability problem for the logic isdecidable.
关键词：Computer Science - Logic in Computer Science;Computer Science - Formal Languages and Automata Theory;F.4.1;F.1.1
