The Hardness of Finding Linear Ranking Functions for Lasso Programs
Finding whether a linear-constraint loop has a linear ranking function is an important key to understanding the loop behavior, proving its termination and establishing iteration bounds. If no preconditions are provided, the decision problem is known to be in coNP when variables range over the intege...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1408.5955v1 |
| _version_ | 1811313405415391232 |
|---|---|
| author | Amir M. Ben-Amram |
| author_facet | Amir M. Ben-Amram |
| author_sort | Amir M. Ben-Amram |
| collection | DOAJ |
| description | Finding whether a linear-constraint loop has a linear ranking function is an important key to understanding the loop behavior, proving its termination and establishing iteration bounds. If no preconditions are provided, the decision problem is known to be in coNP when variables range over the integers and in PTIME for the rational numbers, or real numbers. Here we show that deciding whether a linear-constraint loop with a precondition, specifically with partially-specified input, has a linear ranking function is EXPSPACE-hard over the integers, and PSPACE-hard over the rationals. The precise complexity of these decision problems is yet unknown. The EXPSPACE lower bound is derived from the reachability problem for Petri nets (equivalently, Vector Addition Systems), and possibly indicates an even stronger lower bound (subject to open problems in VAS theory). The lower bound for the rationals follows from a novel simulation of Boolean programs. Lower bounds are also given for the problem of deciding if a linear ranking-function supported by a particular form of inductive invariant exists. For loops over integers, the problem is PSPACE-hard for convex polyhedral invariants and EXPSPACE-hard for downward-closed sets of natural numbers as invariants. |
| first_indexed | 2024-04-13T10:53:13Z |
| format | Article |
| id | doaj.art-4318253262dc44959e50459e024b71e9 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T10:53:13Z |
| publishDate | 2014-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-4318253262dc44959e50459e024b71e92022-12-22T02:49:36ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-08-01161Proc. GandALF 2014324510.4204/EPTCS.161.6:14The Hardness of Finding Linear Ranking Functions for Lasso ProgramsAmir M. Ben-AmramFinding whether a linear-constraint loop has a linear ranking function is an important key to understanding the loop behavior, proving its termination and establishing iteration bounds. If no preconditions are provided, the decision problem is known to be in coNP when variables range over the integers and in PTIME for the rational numbers, or real numbers. Here we show that deciding whether a linear-constraint loop with a precondition, specifically with partially-specified input, has a linear ranking function is EXPSPACE-hard over the integers, and PSPACE-hard over the rationals. The precise complexity of these decision problems is yet unknown. The EXPSPACE lower bound is derived from the reachability problem for Petri nets (equivalently, Vector Addition Systems), and possibly indicates an even stronger lower bound (subject to open problems in VAS theory). The lower bound for the rationals follows from a novel simulation of Boolean programs. Lower bounds are also given for the problem of deciding if a linear ranking-function supported by a particular form of inductive invariant exists. For loops over integers, the problem is PSPACE-hard for convex polyhedral invariants and EXPSPACE-hard for downward-closed sets of natural numbers as invariants.http://arxiv.org/pdf/1408.5955v1 |
| spellingShingle | Amir M. Ben-Amram The Hardness of Finding Linear Ranking Functions for Lasso Programs Electronic Proceedings in Theoretical Computer Science |
| title | The Hardness of Finding Linear Ranking Functions for Lasso Programs |
| title_full | The Hardness of Finding Linear Ranking Functions for Lasso Programs |
| title_fullStr | The Hardness of Finding Linear Ranking Functions for Lasso Programs |
| title_full_unstemmed | The Hardness of Finding Linear Ranking Functions for Lasso Programs |
| title_short | The Hardness of Finding Linear Ranking Functions for Lasso Programs |
| title_sort | hardness of finding linear ranking functions for lasso programs |
| url | http://arxiv.org/pdf/1408.5955v1 |
| work_keys_str_mv | AT amirmbenamram thehardnessoffindinglinearrankingfunctionsforlassoprograms AT amirmbenamram hardnessoffindinglinearrankingfunctionsforlassoprograms |