A Logic for Accumulated-Weight Reasoning on Multiweighted Modal
Automata

D 2012

A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata

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

Základní údaje

Originální název

A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata

Autoři

BAUER, Sebastian S. (276 Německo), Line JUHL (208 Dánsko), Kim G. LARSEN (208 Dánsko), Axel LEGAY (56 Belgie) a Jiří SRBA (203 Česká republika, garant, domácí)

Vydání

USA, Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12), od s. 77-84, 8 s. 2012

Nakladatel

IEEE Computer Society Press

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Web

Kód RIV

RIV/00216224:14330/12:00062430

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4673-2353-6

DOI

http://dx.doi.org/10.1109/TASE.2012.9

Klíčová slova anglicky

modal automata; specification theory; energy games; multiweighted automata

Změněno: 23. 4. 2013 09:34, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

LA09016, projekt VaV

Název: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Akronym: ERCIM)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Účast ČR v European Research Consortium for Informatics and Mathematics

Citovat

BAUER, Sebastian S., Line JUHL, Kim G. LARSEN, Axel LEGAY a Jiří SRBA. A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata. In Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12). USA: IEEE Computer Society Press, 2012, s. 77-84. ISBN 978-1-4673-2353-6. Dostupné z: https://dx.doi.org/10.1109/TASE.2012.9.

@inproceedings{1079129,
   author = {Bauer, Sebastian S. and Juhl, Line and Larsen, Kim G. and Legay, Axel and Srba, Jiří},
   address = {USA},
   booktitle = {Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12)},
   doi = {http://dx.doi.org/10.1109/TASE.2012.9},
   keywords = {modal automata; specification theory; energy games; multiweighted automata},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {USA},
   isbn = {978-1-4673-2353-6},
   pages = {77-84},
   publisher = {IEEE Computer Society Press},
   title = {A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata},
   url = {http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9},
   year = {2012}
}

TY  - JOUR
ID  - 1079129
AU  - Bauer, Sebastian S. - Juhl, Line - Larsen, Kim G. - Legay, Axel - Srba, Jiří
PY  - 2012
TI  - A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata
PB  - IEEE Computer Society Press
CY  - USA
SN  - 9781467323536
KW  - modal automata
KW  - specification theory
KW  - energy games
KW  - multiweighted automata
UR  - http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9
L2  - http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9
N2  - 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.
ER  -

BAUER, Sebastian S., Line JUHL, Kim G. LARSEN, Axel LEGAY a Jiří SRBA. A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata. In \textit{Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12)}. USA: IEEE Computer Society Press, 2012, s.~77-84. ISBN~978-1-4673-2353-6. Dostupné z: https://dx.doi.org/10.1109/TASE.2012.9.

Podrobný výpis o publikaci