Projects per year
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 language | English |
---|---|
Title of host publication | Dependable Software Engineering: Theories, Tools, and Applications : Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings |
Editors | Martin Fränzle, Deepak Kapur, Naijun Zhan |
Publisher | Springer |
Publication date | 2016 |
Pages | 213-228 |
ISBN (Print) | 978-3-319-47676-6 |
ISBN (Electronic) | 978-3-319-47677-3 |
DOIs | |
Publication status | Published - 2016 |
Event | 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 - Beijing, China Duration: 9 Nov 2016 → 11 Nov 2016 |
Conference
Conference | 2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016 |
---|---|
Country/Territory | China |
City | Beijing |
Period | 09/11/2016 → 11/11/2016 |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 9984 |
ISSN | 0302-9743 |
Fingerprint
Dive into the research topics of 'A Complete Approximation Theory for Weighted Transition Systems'. Together they form a unique fingerprint.Projects
- 2 Finished
-
Approximate Reasoning for Stochastic Markovian Systems
Mardare, R. & Larsen, K. G.
01/11/2015 → 31/10/2019
Project: Research
-
IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research
Activities
- 1 Conference presentations
-
2nd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2016
Mikkel Hansen (Speaker)
9 Nov 2016 → 11 Nov 2016Activity: Talks and presentations › Conference presentations