The Complexity of Computing the Behaviour of Weighted Büchi Automata over Lattices
Karsten Lehmann, Rafael Peñaloza · BOA (University of Milano-Bicocca) · 2012
Automata have long been recognized as a useful mechanism for solving logic-based reasoning tasks. For example, to decide whether a formula is satisfiable, one can construct an automaton that recognizes all the (well-structured) models of this formula, and decide whether the language accepted by the automaton is empty—in which case the formula is unsatisfiable—or not—and then the formula has a model, i.e. is satisfiable. When logical reasoning is reduced to the (non-)emptiness of an automaton, as in the previous example, it is usually possible to use a simplified alphabet of cardinality one: the models of the input formula are described by the accepting runs, rather than by the recognized language. This kind of construction has been generalized to weighted automata over lattices, as a means to deal with non-standard logical semantics. Briefly, every model of the input formula is associated with a weight, and we are interested in finding the supremum of the weights of all these models. Suppose that we can associate every transition of the constructed automaton with a weight, in such a way that the infimum of the weights of all the transitions appearing in a successful run (that is, the weight of the run itself) corresponds exactly to the weight of the model it represents. Then, reasoning in this non-standard semantics reduces to computing the behaviour of a weighted automaton. To understand the complexity of our non-standard