# Incremental Closure for Systems of Two Variables Per Inequality

Howe, Jacob M., King, Andy, Simon, Axel (2019) Incremental Closure for Systems of Two Variables Per Inequality. Theoretical Computer Science, 768 . pp. 1-64. ISSN 0304-3975. (doi:10.1016/j.tcs.2018.12.001) (KAR id:70546)

 PDF Publisher pdf Language: English This work is licensed under a Creative Commons Attribution 4.0 International License. Download this file(PDF/2MB) Preview Request a format suitable for use with assistive technology e.g. a screenreader PDF Author's Accepted Manuscript Language: English This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. Download this file(PDF/580kB) Preview Request a format suitable for use with assistive technology e.g. a screenreader Official URL:https://doi.org/10.1016/j.tcs.2018.12.001

## Abstract

Subclasses of linear inequalities where each inequality has at most two variables are popular in abstract interpretation and model checking, because they strike a balance between what can be described and what can be efficiently computed. This paper focuses on the TVPI class of inequalities, for which each coefficient of each two variable inequality is unrestricted. An implied TVPI inequality can be generated from a pair of TVPI inequalities by eliminating a given common variable (echoing resolution on clauses). This operation, called result, can be applied to derive TVPI inequalities which are entailed (implied) by a given TVPI system. The key operation on TVPI is calculating closure: satisfiability can be observed from a closed system and a closed system also simplifies the calculation of other operations. A closed system can be derived by repeatedly applying the result operator. The process of adding a single TVPI inequality to an already closed input TVPI system and then finding the closure of this augmented system is called incremental closure. This too can be calculated by the repeated application of the result operator. This paper studies the calculus defined by result, the structure of result derivations, and how derivations can be combined and controlled. A series of lemmata on derivations are presented that, collectively, provide a pathway for synthesising an algorithm for incremental closure. The complexity of the incremental closure algorithm is analysed and found to be O((n^2+m^2)lg(m)), where n is the number of variables and $m$ the number of inequalities of the input TVPI system.

Item Type: Article 10.1016/j.tcs.2018.12.001 Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing Andy King 02 Dec 2018 10:00 UTC 11 Jan 2024 00:25 UTC https://kar.kent.ac.uk/id/eprint/70546 (The current URI for this page, for reference purposes)

## University of Kent Author Information

### King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822

### Simon, Axel.

• Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.