Towards the exact complexity of realizability for Safety LTL
(2024) In Journal of Logical and Algebraic Methods in Programming 141.- Abstract
We study the realizability and strong satisfiability problems for SAFETY LTL, a syntactic fragment of Linear Temporal Logic ([Formula presented]) capturing safe formulas. While it is well-known that realizability for this fragment lies in [Formula presented], the best-known lower bound is [Formula presented]-hardness. Surprisingly, closing this gap has proven an elusive task. Previous works have claimed first [Formula presented]-completeness [1] and later [Formula presented]-completeness [2] for this problem, but both of these proofs turned out to be incorrect. We revisit the problem of the exact classification of the complexity of realizability for [Formula presented] through the lens of seemingly weaker fragments. While we cannot... (More)
We study the realizability and strong satisfiability problems for SAFETY LTL, a syntactic fragment of Linear Temporal Logic ([Formula presented]) capturing safe formulas. While it is well-known that realizability for this fragment lies in [Formula presented], the best-known lower bound is [Formula presented]-hardness. Surprisingly, closing this gap has proven an elusive task. Previous works have claimed first [Formula presented]-completeness [1] and later [Formula presented]-completeness [2] for this problem, but both of these proofs turned out to be incorrect. We revisit the problem of the exact classification of the complexity of realizability for [Formula presented] through the lens of seemingly weaker fragments. While we cannot settle the question for [Formula presented], we study a subfragment of it consisting of formulas of the form [Formula presented], where α is a present formula over system variables and ψ contains Next as the only temporal operator. We prove that the realizability problem for this new fragment, which we call [Formula presented], is [Formula presented]-complete, and observe that this fragment is equirealizable to existing more expressive fragments, such as the class [Formula presented] [3]. Furthermore, we revisit the techniques used in the purported proof of [Formula presented]-completeness of Arteche and Hermo [1], and observe that, while incorrect in their original claims, their proofs can be modified to classify the complexity of strong satisfiability, a necessary condition for realizability introduced by Kupferman, Sadigh, and Seshia [4]. We prove that, with regards to strong satisfiability, the fragments [Formula presented] and [Formula presented] are in fact equivalent under polynomial-time many-one reductions.
(Less)
- author
- Arteche, Noel LU and Hermo, Montserrat
- organization
- publishing date
- 2024-10
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- Complexity theory, Realizability, Strong satisfiability, Synthesis, Temporal logic
- in
- Journal of Logical and Algebraic Methods in Programming
- volume
- 141
- article number
- 101002
- publisher
- Elsevier
- external identifiers
-
- scopus:85200485014
- ISSN
- 2352-2208
- DOI
- 10.1016/j.jlamp.2024.101002
- language
- English
- LU publication?
- yes
- id
- 04e8fc0e-bf04-4fc7-8b55-99991544ff10
- date added to LUP
- 2024-09-03 15:34:42
- date last changed
- 2025-06-03 13:14:59
@article{04e8fc0e-bf04-4fc7-8b55-99991544ff10,
abstract = {{<p>We study the realizability and strong satisfiability problems for SAFETY LTL, a syntactic fragment of Linear Temporal Logic ([Formula presented]) capturing safe formulas. While it is well-known that realizability for this fragment lies in [Formula presented], the best-known lower bound is [Formula presented]-hardness. Surprisingly, closing this gap has proven an elusive task. Previous works have claimed first [Formula presented]-completeness [1] and later [Formula presented]-completeness [2] for this problem, but both of these proofs turned out to be incorrect. We revisit the problem of the exact classification of the complexity of realizability for [Formula presented] through the lens of seemingly weaker fragments. While we cannot settle the question for [Formula presented], we study a subfragment of it consisting of formulas of the form [Formula presented], where α is a present formula over system variables and ψ contains Next as the only temporal operator. We prove that the realizability problem for this new fragment, which we call [Formula presented], is [Formula presented]-complete, and observe that this fragment is equirealizable to existing more expressive fragments, such as the class [Formula presented] [3]. Furthermore, we revisit the techniques used in the purported proof of [Formula presented]-completeness of Arteche and Hermo [1], and observe that, while incorrect in their original claims, their proofs can be modified to classify the complexity of strong satisfiability, a necessary condition for realizability introduced by Kupferman, Sadigh, and Seshia [4]. We prove that, with regards to strong satisfiability, the fragments [Formula presented] and [Formula presented] are in fact equivalent under polynomial-time many-one reductions.</p>}},
author = {{Arteche, Noel and Hermo, Montserrat}},
issn = {{2352-2208}},
keywords = {{Complexity theory; Realizability; Strong satisfiability; Synthesis; Temporal logic}},
language = {{eng}},
publisher = {{Elsevier}},
series = {{Journal of Logical and Algebraic Methods in Programming}},
title = {{Towards the exact complexity of realizability for Safety LTL}},
url = {{http://dx.doi.org/10.1016/j.jlamp.2024.101002}},
doi = {{10.1016/j.jlamp.2024.101002}},
volume = {{141}},
year = {{2024}},
}