Abstract
Multiweighted modal automata provide a specification theory for multiweighted transition systems that have recently attracted interest in the context of energy games. We propose a simple fragment of CTL that is able to express properties about accumulated weights along maximal runs of multiweighted modal automata. Our logic is equipped with a game-based semantics and guarantees both soundness (formula satisfaction is propagated to the modal refinements) as well as completeness (formula non-satisfaction is propagated to at least one of its implementations). We augment our theory with a summary of decidability and complexity results of the generalized model checking problem, asking whether a specification - abstracting the whole set of its implementations - satisfies a given formula.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012 |
Antal sider | 8 |
Forlag | IEEE Computer Society Press |
Publikationsdato | 1 jan. 2012 |
Sider | 77-84 |
ISBN (Trykt) | 978-1-4673-2353-6 |
DOI | |
Status | Udgivet - 1 jan. 2012 |
Begivenhed | Sixth International Symposium on Theoretical Aspects of Software Engineering - Beijing, Kina Varighed: 4 jul. 2012 → 6 jul. 2012 |
Konference
Konference | Sixth International Symposium on Theoretical Aspects of Software Engineering |
---|---|
Land/Område | Kina |
By | Beijing |
Periode | 04/07/2012 → 06/07/2012 |