A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata
| Authors | |
|---|---|
| Year of publication | 2012 |
| Type | Article in Proceedings |
| Conference | Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12) |
| MU Faculty or unit | |
| Citation | |
| Web | Web |
| Doi | http://dx.doi.org/10.1109/TASE.2012.9 |
| Field | Informatics |
| Keywords | modal automata; specification theory; energy games; multiweighted automata |
| Description | 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. |
| Related projects: |