Autor:
Arteche, Noel

Cargando...
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

Resultados de la búsqueda

Mostrando 1 - 1 de 1
  • 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.