Autor:
Arteche, Noel

Foto de perfil
E-mails conocidos
noel.arteche@cs.lth.se
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Arteche
Nombre de pila
Noel
Nombre
Nombres alternativos
Afiliaciones conocidas
Lund University, Sweden
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

20231
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 1 de 1
  • Miniatura
    Artículo
    An Open Problem on the Complexity of Realizability for Safety LTL and Related Subfragments
    Arteche, Noel; Hermo, Montserrat. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    We study the realizability problem for Safety LTL, the syntactic fragment of Linear Temporal Logic capturing safe formulas. It is known that realizability for formulas in this fragment is EXP-hard, and the best-known upper bound is 2EXP. In this work, we approach the exact classification of the complexity of realizability for Safety LTL by studying seemingly weaker subfragments. In particular, we study the fragment consisting of formulas of the form α ∧ Gψ, 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 GX_0, is also EXP-complete, and observe that this fragment is equirealizable to existing more expressive fragments, such as the LTL_EBR system of Cimatti et al.[8]. We show how trying to prove equirealizability between the full Safety LTL and the existing EXP-complete fragments fails. We highlight the practical relevance of fast algorithms for Safety LTL and point at the open problem of providing a tighter bound on the exact computational complexity of realizability for the full Safety LTL fragment.