A Complete Approximation Theory for Weighted Transition Systems

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

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (Scopus)
68 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
TitelDependable Software Engineering: Theories, Tools, and Applications : Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings
RedaktørerMartin Fränzle, Deepak Kapur, Naijun Zhan
ForlagSpringer
Publikationsdato2016
Sider213-228
ISBN (Trykt)978-3-319-47676-6
ISBN (Elektronisk)978-3-319-47677-3
DOI
StatusUdgivet - 2016
Begivenhed2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, Kina
Varighed: 9 nov. 201611 nov. 2016

Konference

Konference2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016
LandKina
ByBeijing
Periode09/11/201611/11/2016
NavnLecture Notes in Computer Science
Vol/bind9984
ISSN0302-9743

Fingerprint

Bisimulation
Approximation Theory
Transition Systems
Logic
Finite Models
Axiomatization
Modal Logic
Decidability
Finiteness
Numerics
Modality
Open Problems
Express
Reasoning
Restriction
Invariant
Class

Citer dette

Hansen, M., Larsen, K. G., Mardare, R. I., Pedersen, M. R., & Xue, B. (2016). A Complete Approximation Theory for Weighted Transition Systems. I M. Fränzle, D. Kapur, & N. Zhan (red.), Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings (s. 213-228). Springer. Lecture Notes in Computer Science, Bind. 9984 https://doi.org/10.1007/978-3-319-47677-3_14
Hansen, Mikkel ; Larsen, Kim Guldstrand ; Mardare, Radu Iulian ; Pedersen, Mathias Ruggaard ; Xue, Bingtian. / A Complete Approximation Theory for Weighted Transition Systems. Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. red. / Martin Fränzle ; Deepak Kapur ; Naijun Zhan. Springer, 2016. s. 213-228 (Lecture Notes in Computer Science, Bind 9984).
@inproceedings{c11acf2bf3a34f34b042d3638e48583b,
title = "A Complete Approximation Theory for Weighted Transition Systems",
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.",
author = "Mikkel Hansen and Larsen, {Kim Guldstrand} and Mardare, {Radu Iulian} and Pedersen, {Mathias Ruggaard} and Bingtian Xue",
year = "2016",
doi = "10.1007/978-3-319-47677-3_14",
language = "English",
isbn = "978-3-319-47676-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "213--228",
editor = "Martin Fr{\"a}nzle and Deepak Kapur and Naijun Zhan",
booktitle = "Dependable Software Engineering: Theories, Tools, and Applications",
address = "Germany",

}

Hansen, M, Larsen, KG, Mardare, RI, Pedersen, MR & Xue, B 2016, A Complete Approximation Theory for Weighted Transition Systems. i M Fränzle, D Kapur & N Zhan (red), Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Springer, Lecture Notes in Computer Science, bind 9984, s. 213-228, Beijing, Kina, 09/11/2016. https://doi.org/10.1007/978-3-319-47677-3_14

A Complete Approximation Theory for Weighted Transition Systems. / Hansen, Mikkel; Larsen, Kim Guldstrand; Mardare, Radu Iulian; Pedersen, Mathias Ruggaard; Xue, Bingtian.

Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. red. / Martin Fränzle; Deepak Kapur; Naijun Zhan. Springer, 2016. s. 213-228 (Lecture Notes in Computer Science, Bind 9984).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - A Complete Approximation Theory for Weighted Transition Systems

AU - Hansen, Mikkel

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu Iulian

AU - Pedersen, Mathias Ruggaard

AU - Xue, Bingtian

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-47677-3_14

DO - 10.1007/978-3-319-47677-3_14

M3 - Article in proceeding

SN - 978-3-319-47676-6

T3 - Lecture Notes in Computer Science

SP - 213

EP - 228

BT - Dependable Software Engineering: Theories, Tools, and Applications

A2 - Fränzle, Martin

A2 - Kapur, Deepak

A2 - Zhan, Naijun

PB - Springer

ER -

Hansen M, Larsen KG, Mardare RI, Pedersen MR, Xue B. A Complete Approximation Theory for Weighted Transition Systems. I Fränzle M, Kapur D, Zhan N, red., Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings. Springer. 2016. s. 213-228. (Lecture Notes in Computer Science, Bind 9984). https://doi.org/10.1007/978-3-319-47677-3_14