Max and Sum Semantics for Alternating Weighted Automata

Abstract. In the traditional Boolean setting of formal verification, alternating automata are the key to many algorithms and tools. In this setting, the correspondence between disjunctions/conjunctions in the specification and nondeterministic/universal transitions in the automaton for the specification is straightforward. A recent exciting research direction aims at adding a quality measure to the satisfaction of specifications of reactive systems. The corresponding automata-theoretic framework is based on weighted automata, which map input words to numerical values. In the weighted setting, nondeterminism has a minimum semantics – the weight that an automaton assigns to a word is the cost of the cheapest run on it. For universal branches, researchers have studied a (dual) maximum semantics. We argue that a summation semantics is of interest too, as it captures the intuition that one has to pay for the cost of all conjuncts. We introduce and study alternating weighted automata o...

• Type: Journal
• Year: 2011
• Where: ATVA
• Authors: Shaull Almagor, Orna Kupferman
• Keywords: Arithmetic Operations, ATVA 2011, Hardware, Input Words, Weighted Automata