Lógica Temporal Lineal
URI permanente para esta colección:
Artículos en la categoría Lógica Temporal Lineal publicados en las Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo IndVarLTL: A tool which identifies independent variables in LTL expressionsOca, Josu; Hermo, Montserrat. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.A reactive system is a system that interacts with the environment through sensors and is usually specified by means of Linear Temporal Logic formulas. In order to verify that under no circumstances can there be a failure in these systems, it is necessary to know that the system has a response for any possible behavior of the environment. In other words, the aim is to know whether the specification of the system is realizable. Unfortunately, the complexity of this problem is doubly exponential, so different techniques have been tried to speed up how to solve the realizability problem. One of them proposes to decompose the specification of a system into smaller specifications to be able to treat them independently, and then through a correct interpretation of the results to know if the initial specification was realizable. This article presents a tool for the extraction of independent variables in a given specification based on a sound and complete algorithm. Throughout the article, it is explained how the tool works and how to work with it.Artículo Unconditional Unrealizability Detection in Reactive Systems Modulo TheoriesRodriguez, Andoni; Sánchez, César. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.Linear Temporal Logic modulo theories (LTLT ) extends LTL by allowing atomic propositions to be literals from the theory T . Realizability of an LTLT specification φ is proven to be decidable by a Boolean abstraction that generates an equi-realizable LTL specification from φ. This abstraction method also opens the door for a more thoughtful analysis of LTLT specifications. In this work in progress, we address how to produce informative traces of LTLT specifications by finding strategies of the players such that certain desired or undesired goals are reached. In particularly, we show how to produce unconditional unrealizability witnesses for an uncontrollable environment. We present two approaches based on unrollings of formulae: the first one characterizes the problem using SMT-with-quantifiers; the second one Booleanizes the LTLT formula and then uses QBF solving. We show the latter is faster and provides more termination guarantees. To the best of our knowledge, this is the first such specification analysis over such an expressive fragment of the logic.Resumen Tableaux for Realizability of Safety SpecificationsHermo, Montserrat; Lucio, Paqui; Sánchez, César. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.This work was presented at Formal Methods 2023 conference in Lübeck, Germany.