A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

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

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.