. . . "[A33E0A471378]" . . "Legay, Axel" . "Larsen, Kim G." . . "China" . "modal automata; specification theory; energy games; multiweighted automata"@en . . "A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata"@en . "5"^^ . "RIV/00216224:14330/12:00062430" . "IEEE Computer Society Press" . "8"^^ . . "A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata" . "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."@en . . "A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata" . . . "1"^^ . "USA" . "2012-01-01+01:00"^^ . . . . "Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12)" . "Srba, Ji\u0159\u00ED" . . . . "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." . . "RIV/00216224:14330/12:00062430!RIV13-MSM-14330___" . "120280" . "I, P(LA09016)" . "http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9" . "A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata"@en . . "10.1109/TASE.2012.9" . . "Juhl, Line" . "Bauer, Sebastian S." . "14330" . "9781467323536" .