Automata vs Linear-Programming Discounted-Sum Inclusion

Authors: Suguman Bansal, Swarat Chaudhuri and Moshe Vardi

Paper Information

Title:Automata vs Linear-Programming Discounted-Sum Inclusion
Authors:Suguman Bansal, Swarat Chaudhuri and Moshe Vardi
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Quantitative analysis, Discounted-sum inclusion, Empirical evaluation, Discounted-sum determinization, Comparator, Language inclusion, Runtime complexity

ABSTRACT. The problem of {\em quantitative inclusion} formalizes the goal of comparing quantitative dimensions between systems such as worst-case execution time, resource consumption, and the like. Such systems are typically represented by formalisms such as weighted logics or weighted automata. Despite its significance in analyzing the quality of computing systems, the study of quantitative inclusion has mostly been conducted from a theoretical standpoint. In this work, we conduct the first empirical study of quantitative inclusion for discounted-sum weighted automata (\DS-inclusion, in short).

Currently, two contrasting approaches for \DS-inclusion exist: the linear-programming based \cct{DetLP} and the purely automata-theoretic \cct{BCV}. Theoretical complexity of \DetLPt is exponential in time and space while of \BCVt is \cct{PSPACE}-complete. All practical implementations of \cct{BCV}, however, are also exponential in time and space. Hence, it is not clear which of the two algorithms renders a superior implementation.

In this work we present the first implementations of these algorithms, and perform extensive experimentation to compare between the two approaches. Our empirical analysis shows how the two approaches complement each other. This is a nuanced picture that is much richer than the one obtained from the theoretical study alone.

Talk:Jul 17 09:00 (Session 117A: Theory and Security)