Autor: Hermo, Montserrat
Cargando...
E-mails conocidos
montserrat.hermo@ehu.eus
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Hermo
Nombre de pila
Montserrat
Nombre
Nombres alternativos
Afiliaciones conocidas
University of the Basque Country, Spain
Universidad del País Vasco, Spain
University of the Basque Country (UPV/EHU), Spain
Universidad del País Vasco
Languages and Information Systems The University of the Basque Country (UPV/EHU)
The Universtiy of the Basque Country, Spain
Universidad del País Vasco, Spain
University of the Basque Country (UPV/EHU), Spain
Universidad del País Vasco
Languages and Information Systems The University of the Basque Country (UPV/EHU)
The Universtiy of the Basque Country, Spain
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor
7 resultados
Resultados de la búsqueda
Mostrando 1 - 7 de 7
Artículo Towards the Automatic Verification of QCSP tractability resultsAbuin, Alex; Chen, Hubie; Hermo, Montserrat; Lucio, Paqui. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a rst-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results.Artículo Context-based Model Checking using SMT-solversAbuin, Alex; Díaz de Cerio, Unai; Hermo, Montserrat; Lucio, Paqui. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.Artículo Using Model Checking in Requirement-based Test Generation for Reactive SystemsHermo, Montserrat; Lucio, Paqui; Oca, Josu. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.In this article we propose an automatic test generation technique for evaluating the implementation of a reactive system with respect to the set of requirements from which it has been developed. We consider reactive systems that interact with its environment via variables whose values (at each instant) depends on events or sensors. Our test cases are graphs that represent a collection of executions (or traces) of the system that captures all possible behaviours of the environment. Our proposal is a technique to automatically construct these graphs exploding the ability of model checkers to generate counter-examples for temporal properties that are not satisfied by a system model. Further work includes to implement a prototype for experimenting the technique on a test suite of industrial requirements, and also to design and implement some techniques to gain scalability.Artículo An 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.[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.Artículo Towards 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ículo Learning a Subclass of Multivalued Dependencies Formulas from EntailmentsHermo, Montserrat; Ozaki, Ana. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.Functional and multivalued dependencies play an important role in the design of relational databases. There is a strong connection between data dependencies and some fragments of the propositional logic. In particular, functional dependencies are closely related to Horn formulas. Also, multivalued dependencies are characterized in terms of multivalued formulas. It is known that both Horn formulas and sets of functional dependencies are efficiently learnable in the exact model of learning with queries. In this work, we study the learnability of a non-trivial subclass of multivalued formulas called CRMVDF. We use Angluin’s exact learning model with membership and equivalence queries and present a polynomial time algorithm which exactly learns CRMVDF from entailments.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.