A Complete Approximation Theory for Weighted Transition Systems

Publication: Research - peer-reviewArticle in proceeding

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 which allows us to prove the decidability of satisfiability and provide an algorithm for satisfiability checking. Last but not least, we identify a complete axiomatization for this logic, thus solving a long-standing open problem in this field. All our results are proven for a class of WTSs without the image-finiteness restriction, a fact that makes this development general and robust.
Close

Details

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 which allows us to prove the decidability of satisfiability and provide an algorithm for satisfiability checking. Last but not least, we identify a complete axiomatization for this logic, thus solving a long-standing open problem in this field. All our results are proven for a class of WTSs without the image-finiteness restriction, a fact that makes this development general and robust.
Original languageEnglish
Title of host publicationDependable Software Engineering: Theories, Tools, and Applications : Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings
EditorsMartin Fränzle, Deepak Kapur, Naijun Zhan
PublisherSpringer
Publication date2016
Pages213-228
ISBN (print)978-3-319-47676-6
ISBN (electronic)978-3-319-47677-3
DOI
StatePublished - 2016
Event2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, China

Conference

Conference2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016
LandChina
ByBeijing
Periode09/11/201611/11/2016
SeriesLecture Notes in Computer Science
Volume9984
ISSN0302-9743

Activities

ID: 245820506