A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00062430" target="_blank" >RIV/00216224:14330/12:00062430 - isvavai.cz</a>
Result on the web
<a href="http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9" target="_blank" >http://doi.ieeecomputersociety.org/10.1109/TASE.2012.9</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/TASE.2012.9" target="_blank" >10.1109/TASE.2012.9</a>
Alternative languages
Result language
angličtina
Original language name
A Logic for Accumulated-Weight Reasoning on Multiweighted Modal Automata
Original language 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-satisfactionis 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/LA09016" target="_blank" >LA09016: Czech Republic membership in the European Research Consortium for Informatics and Mathematics (ERCIM)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12)
ISBN
9781467323536
ISSN
—
e-ISSN
—
Number of pages
8
Pages from-to
77-84
Publisher name
IEEE Computer Society Press
Place of publication
USA
Event location
China
Event date
Jan 1, 2012
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—