Parameterized Weighted Containment

摘要

Partially specified systems and specifications are used in formal methods such as stepwise design and query checking. Existing methods consider a setting in which systems and their correctness are Boolean. In recent years, there has been growing interest and need for quantitative formal methods, where systems may be weighted and specifications may be multivalued. Weighted automata, which map input words to a numerical value, play a key role in quantitative reasoning. Technically, every transition in a weighted automaton A has a cost, and the value A assigns to a finite word w is the sum of the costs on the transitions traversed along the most expensive accepting run of A on w. We study parameterized weighted containment: given three weighted automata A, B, and C, with B being partial, the goal is to find an assignment to the missing costs in B so that we end up with B' for which A <= B' <= C, where <= is the weighted counterpart of containment. We also consider a one-sided version of the problem, where only A or only C is given in addition to B, and the goal is to find a minimal assignment with which A <= B' or, respectively, a maximal one with which B' <= C. We argue that both problems are useful in stepwise design of weighted systems as well as approximated minimization of weighted automata.