A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BAUER Sebastian S. JUHL Line LARSEN Kim G. LEGAY Axel SRBA Jiří

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.