Resumé
| Originalsprog | Engelsk |
|---|---|
| Titel | Dependable Software Engineering: Theories, Tools, and Applications : Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings |
| Redaktører | Martin Fränzle, Deepak Kapur, Naijun Zhan |
| Forlag | Springer |
| Publikationsdato | 2016 |
| Sider | 213-228 |
| ISBN (Trykt) | 978-3-319-47676-6 |
| ISBN (Elektronisk) | 978-3-319-47677-3 |
| DOI | |
| Status | Udgivet - 2016 |
| Begivenhed | 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, Kina Varighed: 9 nov. 2016 → 11 nov. 2016 |
Konference
| Konference | 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 |
|---|---|
| Land | Kina |
| By | Beijing |
| Periode | 09/11/2016 → 11/11/2016 |
| Navn | Lecture Notes in Computer Science |
|---|---|
| Vol/bind | 9984 |
| ISSN | 0302-9743 |
Fingerprint
Citer dette
}
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 proceeding › Konferenceartikel i proceeding › Forskning › peer 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 -