ArtículoTowards an Efficient Implementation of Tableaux for Reactive Safety SpecificationsAlonso, Ander; Hermo, Montserrat; Oca, Josu. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.In this article, we take the first steps to implement a tableau method for deciding realizability of specifications expressed in a safety fragment of linear temporal logic. This tableau method also allows us to extract (i.e., synthesize) a correct system in the case the specification is realizable. In particular, we explain here how to efficiently implement a new normal form called terse normal form, which is crucial to the development of such tableau method. ArtículoAn Open Problem on the Complexity of Realizability for Safety LTL and Related SubfragmentsArteche, 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.. 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. ArtículoxeLTL: Extending eLTL with variablesPanizo, Laura; Gallardo, María del Mar. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Our daily activity is increasingly integrated with systems that somehow adapt their behaviour to our state or reactions. These systems are usually called reactive systems since they evolve based on internal or external events produced by their environment. The massive use of smartphones and wearable devices for health monitoring is just an example of how these systems impact in our lives. In addition, some systems, such as those for assisted or autonomous driving, carry out critical tasks. Thus, it is important to ensure that reactive systems satisfy safety requirements in which, in many cases, is relevant the evolution of time or other physical magnitudes. In this paper, we present the eXtended Event-driven Temporal Logic (xeLTL) that can express requirements over intervals of parameterized events.