On quantified linear implications

A Quantified Linear Implication (QLI) is an inclusion query over two polyhedral sets, with a quantifier string that specifies which variables are existentially quantified and which are universally quantified. Equivalently, it can be viewed as a quantified implication of two systems of linear inequalities. In this paper, we provide a 2-person game semantics for the QLI problem, which allows us to explore the computational complexities of several of its classes. More specifically, we prove that the decision problem for QLIs with an arbitrary number of quantifier alternations is PSPACE-hard. Furthermore, we explore the computational complexities of several classes of 0, 1, and 2-quantifier alternation QLIs. We observed that some classes are decidable in polynomial time, some are NP-complete, some are coNP-hard and some are \(\boldsymbol{\Pi}_{\textbf 2}^{\textbf P}\) -hard. We also establish the hardness of QLIs with 2 or more quantifier alternations with respect to the first quantifier in the quantifier string and the number of quantifier alternations. All the proofs that we provide for polynomially solvable problems are constructive, i.e., polynomial-time decision algorithms are devised that utilize well-known procedures. QLIs can be utilized as powerful modelling tools for real-life applications. Such applications include reactive systems, real-time schedulers, and static program analyzers.     

Tractable Fragments of Presburger Arithmetic

In this paper we introduce a problem called Quantified Integer Programming, which generalizes the Quantified Satisfiability problem (QSAT). In a Quantified Integer Program (QIP) the program variables can assume arbitrary integral values, as opposed to the boolean values that are assumed by the variables of an instance of QSAT. QIPs naturally represent two-person integer matrix games. The Quantified Integer Programming problem is PSPACE-hard in general, since the QSAT problem is PSPACE-complete. Quantified Integer Programming can be thought of as a restriction of Presburger Arithmetic, in that we allow only conjunctions of linear inequalities. We focus on analyzing various special cases of the general problem, with a view to discovering subclasses that are tractable. Subclasses of the general QIP problem are obtained by restricting either the constraint matrix or quantifier specification or both. We show that if the constraint matrix is totally unimodular, the problem of deciding a QIP can be solved in polynomial time. We also establish the computational complexities of Oblivious strategy games and Clairvoyant strategy games.     

Relatively quantified constraint satisfaction

The constraint satisfaction problem (CSP) is a convenient framework for modelling search problems; the CSP involves deciding, given a set of constraints on variables, whether or not there is an assignment to the variables satisfying all of the constraints. This paper is concerned with the more general framework of quantified constraint satisfaction, in which variables can be quantified both universally and existentially. We study the relatively quantified constraint satisfaction problem (RQCSP), in which the values for each individual variable can be arbitrarily restricted. We give a complete complexity classification of the cases of the RQCSP where the types of constraints that may appear are specified by a constraint language.     

Out of order quantifier elimination for Standard Quantified Linear Programs

In this paper, we present an out of order quantifier elimination algorithm for a class of Quantified Linear Programs (QLPs) called Standard Quantified Linear Programs (SQLPs). QLPs in general and SQLPs in particular are extremely useful constraint logic programming structures that find wide applicability in the modeling of real-time schedulability specifications; see Subramani [Subramani, K., 2005a. A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. The Computer Journal 48 (3), 259–272]. Consequently any algorithmic advance in their solution has a strong practical impact. Prior to this work, the only known approaches to the solution of QLPs involved sequential variable elimination; see Subramani [Subramani, K., 2003b. An analysis of quantified linear programs. In: Calude, C.S. et al. (Eds.), Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science. DMTCS. In: Lecture Notes in Computer Science, vol. 2731. Springer-Verlag, pp. 265–277]. In the sequential approach, the innermost quantified variable is eliminated first, followed by the variable which then becomes the innermost quantified variable and so on, until we are left with a single variable from which the satisfiability of the original formula is easily deduced. This approach is applicable in both discrete and continuous domains; however, it is to be noted that the logic demanding the sequential approach requires that the variables are discrete-valued. To the best of our knowledge, the necessity for sequential elimination over continuous-valued variables has not been investigated in the literature. The techniques used in the development of our elimination algorithm may find applications in domains such as classical logic and finite model theory. The final aspect of our research concerns the structure-preserving nature of the algorithm that we introduce here; in general, it is not known whether discrete domains admit such elimination procedures.     

Toward an abstract theory of data compression

This paper extends the usual notion of abstract program size complexity, studied by Kolmogorov, Chaitin and others, to a theory that can better model the concept of a ‘practical’ compression method. The contraction of a string is defined, as in standard program size complexity, to be the shortest program which produces that string. However, this is in general an undecidable problem. Here, a model for an abstract compression ‘scheme’ is proposed. An abstract compression scheme not only allows the programming language and cost function to be specified, but also a restricted domain of programs that may be used as compressed forms. Limitations and inherent trade-offs are discussed and a class of ‘good’ schemes is considered.     

USING A THEOREM PROVER FOR REASONING ON CONSTRAINT PROBLEMS

The efficiency of systems for constraint programming (CP) is currently highly affected by the actual formulation of the input problem. To this end, several choices have to be made by modelers in order to write efficient specifications and handle instances of realistic size, and this, of course, represents a major obstacle to reach full declarativeness. Several structural properties of problem specifications have been investigated in order to provide techniques that reformulate a constraint program into one which is more efficiently evaluable by the solver at hand. In this paper we consider two such properties, symmetries and functional dependencies among variables, and show that, by characterizing problem specifications as logical formulae, the task of deciding whether such properties hold, and consequently that of performing the relevant reformulations, can be practically mechanized by means of automated theorem proving (ATP) technology. In particular, we report the results on using ATP technology for checking the existence of symmetries, checking whether a given constraint is symmetry-breaking, and checking the existence of functional dependencies in a specification. The output of the reasoning phase is a transformed constraint program, consisting in a reformulated specification and, possibly, a search strategy. We show our techniques on problems such as graph coloring, Sailco inventory, and protein folding.     

程序模型检查器综述

模型检查实际程序设计语言编写的程序是近年来程序验证领域的研究热点之一,出现了一批针对C,C++或Java语言的程序模型检查器原型.总结了程序模型检查中的主要问题及相关技术,以是否使用中间建模语言为标准,对现有程序模型检查器进行了分类,并具体地介绍了一些代表性工具中的模型获取及化简技术,最后展望了程序模型检查器未来的研究方向.     

An incremental algorithm for DLO quantifier elimination via constraint propagation

The first-order logical theory of dense linear order has long been known to admit quantifier elimination. This paper develops an explicit algorithm that yields an equivalent quantifier free form of its input formula. This algorithm performs existential quantifier elimination via constraint propagation. The result is computed incrementally using functional programming techniques. This approach may be of interest in implementing query languages for constraint databases.     

Analyzing restricted fragments of the theory of linear arithmetic

The theory of linear arithmetic (TLA), also known as the Theory of Rationals, is an extremely well-studied theory. It has been widely applied to a number of domains, including program verification and constraint specification. This paper discusses the computational complexities of two broad fragments of TLA, namely Quantified Linear Programs (QLPs) and Quantified Linear Implications (QLIs). These fragments are ideal for expressing specifications in real-time scheduling, and for modeling reactive systems. In this paper, we study the computational complexities of several variants of QLPs and QLIs. Our principal result shows that there exists a one-to-one correspondence between alternations in a class of QLIs and the complexity classes comprising the polynomial hierarchy PH. In other words, for each class of the PH, there exists a class of QLIs that is complete for that class. Our work mirrors the work in [L.J. Stockmeyer, The Polynomial-Time Hierarchy, Theoretical Computer Science, 3:1-22, 1977] which established the connection between the classes of PH and quantifier alternations in a Quantified Boolean Formula. Our results are surprising, since the variables in the fragments that we consider are continuous, as opposed to discrete.     

Reachability and optimal control for linear hybrid automata: a quantifier elimination approach

This paper considers an optimal control problem for linear hybrid automata (LHA). First, we present a controller synthesis algorithm based on reachability analysis. The algorithm computes the maximal initial set from which the controller drives the system to a given target set. It is shown that, using quantifier elimination (QE), an under-approximation of the maximal reachable set can be derived. Next, a weighted time-optimal control problem is solved by transforming it into a constrained optimization problem whose constraints are a set of inequalities with quantifiers. Quantifier elimination (QE) techniques are employed in order to derive the quantifier free inequalities that are shown to be linear. Thus, the optimal cost is obtained using linear programming. For any state belonging to the maximal initial set the optimal switching times and the optimal continuous control inputs are computed. These are used in order to derive a hybrid controller which is optimal with respect to the cost function. Our results are applied to an air traffic management example which is of practical interest.     

Designing checkers for programs that run in parallel

Program correctness for parallel programs is an even more problematic issue than for serial programs. We extend the theory of program result checking to parallel programs, and find general techniques for designing such result checkers that work for many basic problems in parallel computation. These result checkers are simple to program and are more efficient than the actual computation of the result. For example, sorting, multiplication, parity, the all-pairs shortest-path problem and majority all have constant depth result checkers, and the result checkers for all but the last problem use a linear number of processors. We show that there are P-complete problems (evaluating straight-line programs, linear programming) that have very fast, even constant depth, result checkers.This research was done while at the Computer Science Division, University of California, Berkeley, and the International Computer Science Institute, Berkeley, California. Supported in part by an IBM Graduate Fellowship and NSF Grant No. CCR 88-13632.     

Solving quantified constraint satisfaction problems with value selection rules

Solving a quantified constraint satisfaction problem (QCSP) is usually a hard task due to its computational complexity. Exact algorithms play an important role in solving this problem, among which backtrack algorithms are effective. In a backtrack algorithm, an important step is assigning a variable by a chosen value when exploiting a branch, and thus a good value selection rule may speed up greatly. In this paper, we propose two value selection rules for existentially and universally quantified variables, respectively, to avoid unnecessary searching. The rule for universally quantified variables is prior to trying failure values in previous branches, and the rule for existentially quantified variables selects the promising values first. Two rules are integrated into the state-of-the-art QCSP solver, i.e., QCSPSolve, which is an exact solver based on backtracking. We perform a number of experiments to evaluate improvements brought by our rules. From computational results, we can conclude that the new value selection rules speed up the solver by 5 times on average and 30 times at most. We also show both rules perform well particularly on instances with existentially and universally quantified variables occurring alternatively.     

Stability analysis of systems with uncertain time-varying delays

Stability of systems in the presence of bounded uncertain time-varying delays in the feedback loop is studied. The delay parameter is assumed to be an unknown time-varying function for which the upper bounds on the magnitude and the variation are given. The stability problem is treated in the integral quadratic constraint (IQC) framework. Criteria for verifying robust stability are formulated as feasibility problems over a set of frequency-dependent linear matrix inequalities. The criteria can be equivalently formulated as semi-definite programs (SDP) using Kalman-Yakubovich-Popov lemma. As such, checking robust stability can be performed in a computationally efficient fashion.     

协同设计中定量化约束求解方法

通过对约束满足与约束冲突的分析，提出了约束求解的定量化策略．基于变量不确定性，量化了约束满足程度与约束冲突程度，解决了约束求解过程中的优先权问题；给出了约束变化量及关联函数，为约束求解确立了具体的目标和实施方法，实现了约束求解过程的有序搜索．定量化约束求解策略不仅实现了对约束的有序及有效求解，而且真正地实现了在上游约束求解过程中定量地考虑下游约束求解问题．最后，利用随机仿真技术实现了基于变量不确定性的约束求解策略的验证．     

Solving quantified linear arithmetic by counterexample-guided instantiation

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic and linear integer arithmetic formulas with one quantifier alternation. We discuss extensions of these techniques for handling mixed real and integer arithmetic, and to formulas with arbitrary quantifier alternations. For the latter, we use a novel strategy that handles quantified formulas that are not in prenex normal form, which has advantages with respect to existing approaches. All of these techniques can be integrated within the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation in the SMT solver cvc4 outperforms existing tools for quantified linear arithmetic.     

Program equivalence checking by two-tape automata

This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If a dynamic frame is acyclic (i.e., all program statements are irreversible), then it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs in which the semantics of operators is determined by acyclic dynamic frames can be reduced to the emptiness problem for two-tape automata (compound machines).     

Quantifier elimination in automatic loop parallelization

We present an application of quantifier elimination techniques in the automatic parallelization of nested loop programs. The technical goal is to simplify affine inequalities whose coefficients may be unevaluated symbolic constants. The values of these so-called structure parameters are determined at run time and reflect the problem size. Our purpose here is to make the research community of quantifier elimination, in a tutorial style, aware of our application domain–loop parallelization–and to highlight the role of quantifier elimination, as opposed to alternative techniques, in this domain. Technically, we focus on the elimination method of Weispfenning.     

Disjoint pattern matching and implication in strings

We deal with the problem of deciding whether a given set of string patterns implies the presence of a fixed pattern. While checking whether a set of patterns occurs in a string is solvable in polynomial time, this implication problem is well known to be intractable. Here we consider a version of the problem when patterns in the set are required to be disjoint. We show that for such a version of the problem the situation is reversed: checking whether a set of patterns occurs in a string is NP-complete, but the implication problem is solvable in polynomial time.     

Efficient recognition of trace languages defined by repeat-until loops

A sequence of operations may be validly reordered, provided that only pairs of independent operations are commuted. Focusing on a program scheme, idealized as a local finite automaton, we consider the problem of checking whether a given string is a valid permutation of a word recognized by the automaton. Within the framework of trace theory, this is the membership problem for rational trace languages. Existing general algorithms, although time-polynomial, have unbounded degree related to some properties of the dependence graph. Here we present two original linear-time solutions. A straightforward algorithm is suitable for any finite automaton such that all the transitions starting from the same state are labelled by dependent symbols. The second approach is currently restricted to automata representing programs of nested repeat-until loops. Using integer compositions to represent loop iterations and under suitable conditions, the algorithm constructs the syntax tree of a possible word equivalent to the input string. The same procedures show that, under our hypotheses, the uniform version of the membership problem (which is NP-complete in the general case) is solvable in polynomial time.     

字符串分析研究进展

随着软件应用范围的不断扩大,尤其是数据库软件和Web软件的广泛应用,字符串变量在软件程序中扮演的角色日益重要与此同时,针对字符串变量的程序分析技术——字符串分析,也取得了长足的发展,并在软件工程中的很多领域中得到了成功的应用.字符串分析的基本应用模式是首先使用字符串值分析获得字符串变量的所有可能取值,然后使用字符串约束求解判断这些变量的取值是否满足一定约束,从而对程序进行正确性验证.为了使得字符串分析能够应用在安全分析和软件维护应用中,研究人员对字符串分析进行了扩展,进一步分析字符串变量的数据来源.综述了字符串分析技术的研究进展,提出了字符串分析的问题构型,介绍了这一领域现在的主要研究内容:字符串值分析、字符串约束求解、字符串数据来源分析以及字符串分析在软件工程中的应用.