Variants of Quantified Linear Programming and Quantified Linear Implication.
Piotr Jerzy Wojciechowski, Pavlos Eirinakis, K. Subramani · ISAIM · 2014
A Quantified Linear Program (QLP) consists of a set of linear inequalities and a corresponding quantifier string, in which each universally quantified variable is bounded. By extending the quantification of variables to implications of two linear systems, we explore Quantified Linear Implications (QLIs). QLPs and QLIs offer a rich language that is ideal for expressing specifications in real-time scheduling and for modelling reactive systems. In this paper, we show that the variants of QLP and QLI that arise when the universally quantified variables are partially bounded or unbounded can be decided in polynomial time. Moreover, we show that for each class of the polynomial hierarchy (PH), there exists a form of QLI that is complete for that class, thus providing a continuous analogue of the way Quantified Boolean Formulas cover the PH. We also prove that the generic QLI problem is PSPACE-complete and solve some open problems on QLIs with one quantifier alternation.