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.
Original language | English |
---|---|
Title of host publication | Proceedings - IEEE 6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012 |
Number of pages | 8 |
Publisher | IEEE Computer Society Press |
Publication date | 1 Jan 2012 |
Pages | 77-84 |
ISBN (Print) | 978-1-4673-2353-6 |
DOIs | |
Publication status | Published - 1 Jan 2012 |
Event | Sixth International Symposium on Theoretical Aspects of Software Engineering - Beijing, China Duration: 4 Jul 2012 → 6 Jul 2012 |
Conference
Conference | Sixth International Symposium on Theoretical Aspects of Software Engineering |
---|---|
Country/Territory | China |
City | Beijing |
Period | 04/07/2012 → 06/07/2012 |