<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>
Many verification problems can be formulated as a language inclusion problem where the task is to decide whether the language of the system model (given by the runs of the system) is contained in the language induced by a logical specification. The corresponding verification problem for non-functional properties is the quantitative inclusion problem where both the system model and the specification are given by weighted automata and the task is to decide whether the weight for each input string in the automaton for the system is less than that in the automaton for the specification. Here, the weight of a string is defined as an aggregate value of the weights assigned to the states and/or transitions in that string. So, the essential task of the quantitative inclusion problem is to compare the aggregate weight of two input strings. Comparator automata yield an elegant automata-based approach to reason about multiple instances of the quantitative inclusion problem and other algorithmic problems for weighted structures. Speaking roughly, they are defined as automata that take as input two infinite weighted sequences and relate their aggregate values. Among others, they have used to introduce generic algorithms for quantitative inclusion problems and other verification problems for weighted system models. The article by Sugumal Bansal presents an introduction to comparator automata and a summary of their application areas.
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |