A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata
| Autoři | |
|---|---|
| Rok publikování | 2012 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12) |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | Web |
| Doi | http://dx.doi.org/10.1109/TASE.2012.9 |
| Obor | Informatika |
| Klíčová slova | modal automata; specification theory; energy games; multiweighted automata |
| Popis | 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. |
| Související projekty: |