Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917216399654912 |
|---|---|
| author | Lichtner, Kilian Bergsträßer, Pascal Ganardi, Moses Lin, Anthony W. Zetzsche, Georg |
| author_facet | Lichtner, Kilian Bergsträßer, Pascal Ganardi, Moses Lin, Anthony W. Zetzsche, Georg |
| contents | Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques, which are not expressible in first-order logic. Among others, these include liveness verification and monadic decomposability. We present the tool REAL, which implements an efficient elimination of Ramsey quantifiers in existential linear arithmetic theories over integers (LIA), reals (LRA), and the mixed case (LIRA). The tool supports a convenient input format, which is an extension of SMT-LIB over the aforementioned theories with Ramsey quantifiers. We also demonstrate a substantial speedup from the original prototype. As an application, we provide an automatic translation from FASTer (a tool for verifying reachability over infinite-state systems) output format to our extension of SMT-LIB and show how our tool extends FASTer to liveness checking. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_05323 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking) Lichtner, Kilian Bergsträßer, Pascal Ganardi, Moses Lin, Anthony W. Zetzsche, Georg Logic in Computer Science Formal Languages and Automata Theory Ramsey quantifiers have recently been proposed as a unified framework for handling properties of interests in program verification involving proofs in the form of infinite cliques, which are not expressible in first-order logic. Among others, these include liveness verification and monadic decomposability. We present the tool REAL, which implements an efficient elimination of Ramsey quantifiers in existential linear arithmetic theories over integers (LIA), reals (LRA), and the mixed case (LIRA). The tool supports a convenient input format, which is an extension of SMT-LIB over the aforementioned theories with Ramsey quantifiers. We also demonstrate a substantial speedup from the original prototype. As an application, we provide an automatic translation from FASTer (a tool for verifying reachability over infinite-state systems) output format to our extension of SMT-LIB and show how our tool extends FASTer to liveness checking. |
| title | Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking) |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2511.05323 |