A complete approximation theory for weighted transition systems

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

2 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationDependable Software Engineering
Subtitle of host publicationTheories, Tools, and Applications - 2nd International Symposium, SETTA 2016, Proceedings
EditorsMartin Franzle, Deepak Kapur, Naijun Zhan
Place of PublicationCham
PublisherSpringer-Verlag
Pages213-228
Number of pages16
ISBN (Print)9783319476766
DOIs
Publication statusPublished - 6 Oct 2016
Event2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, China
Duration: 9 Nov 201611 Nov 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9984 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016
CountryChina
CityBeijing
Period9/11/1611/11/16

    Fingerprint

Keywords

  • modal logic
  • axiomatic system
  • finite model
  • complete axiomatization
  • arbitrary formula

Cite this

Hansen, M., Larsen, K. G., Mardare, R., Pedersen, M. R., & Xue, B. (2016). A complete approximation theory for weighted transition systems. In M. Franzle, D. Kapur, & N. Zhan (Eds.), Dependable Software Engineering: Theories, Tools, and Applications - 2nd International Symposium, SETTA 2016, Proceedings (pp. 213-228). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9984 LNCS). Cham: Springer-Verlag. https://doi.org/10.1007/978-3-319-47677-3_14