Title: Featured Weighted Automata,
Abstract: A featured transition system is a transition system in which the transitions
are annotated with feature expressions: Boolean expressions on a finite number
of given features. Depending on its feature expression, each individual
transition can be enabled when some features are present, and disabled for
other sets of features. The behavior of a featured transition system hence
depends on a given set of features. There are algorithms for featured
transition systems which can check their properties for all sets of features at
once, for example for LTL or CTL properties.
Here we introduce a model of featured weighted automata which combines
featured transition systems and (semiring-) weighted automata. We show that
methods and techniques from weighted automata extend to featured weighted
automata and devise algorithms to compute quantitative properties of featured
weighted automata for all sets of features at once. We show applications to
minimum reachability and to energy properties.