arXiv subjects

Montserrat Hermo

Publications and source records attributed to Montserrat Hermo.

6 recordsLinked to original sources

arXiv2026

Learning Unions of Intersecting Affine Modules in One Dimension with Queries

We study the exact learnability of finite unions of intersecting affine modules in one dimension. An affine module is a set of the form $a+\sum_{j=1}^{s}b_j \mathbb{Z}$, where $a,b_1,\ldots,b_s\in\mathbb{N}$. We say that a set definable as a finite union of affine modules is a union of intersecting affine modules if it admits a representation in which all modules have a non-empty intersection. We show that this class is efficiently exactly learnable using equivalence and subset queries. Moreover, subset queries can be replaced with membership queries when a common element is known. Our algorithm requires at most $k\log(2|x_\ell|)+2k$ counterexamples, where $k$ is the number of affine modules in the smallest representation and $x_\ell$ is the largest counterexample. This implies polynomial-time learnability in the binary representation.

cs.DM↗

arXiv2026

A Correct Algorithm for Identifying Independent Variable Sets in Reactive Systems

Recent work has proposed algorithms for decomposing reactive synthesis specifications into simpler and independent subspecifications. Motivated by the DecomposeContract algorithm introduced by Antonio Iannopollo, we revisit this approach and provide a mathematical account of the notion of independence on which it is based. The central idea in this setting is to identify independence among system-controlled variables in linear temporal logic formulae by exploiting the power of a model checker. Although the original DecomposeContract algorithm is sound, it is not complete. We support this observation by presenting a concrete counterexample, and we then propose a refined decomposition procedure that preserves the model-checking-based nature of the original method while ensuring completeness. Beyond this algorithmic result, our main contribution is a rigorous semantic analysis of the method, which reveals the principles behind it and makes its limitations explicit.

cs.LO↗

arXiv2022

A Tableau Method for the Realizability and Synthesis of Reactive Safety Specifications

We introduce a tableau decision method for deciding realizability of specifications expressed in a safety fragment of LTL that includes bounded future temporal operators. Tableau decision procedures for temporal and modal logics have been thoroughly studied for satisfiability and for translating temporal formulae into equivalent Büchi automata, and also for model checking, where a specification and system are provided. However, to the best of our knowledge no tableau method has been studied for the reactive synthesis problem. Reactive synthesis starts from a specification where propositional variables are split into those controlled by the environment and those controlled by the system, and consists on automatically producing a system that guarantees the specification for all environments. Realizability is the decision problem of whether there is one such system. In this paper we present a method to decide realizability of safety specifications, from which we can also extract (i.e. synthesize) a correct system (in case the specification is realizable). Our method can easily be extended to handle richer domains (integers, etc) and bounds in the temporal operators in ways that automata approaches for synthesis cannot.

cs.LO↗

arXiv2022

On the Complexity of Realizability for Safety LTL and Related Subfragments

We study the realizability problem for Safety LTL, the syntactic fragment of Linear Temporal Logic capturing safe formulas. We show that the problem is EXP-complete, disproving the existing conjecture of 2EXP-completeness. We achieve this by comparing the complexity of Safety LTL with seemingly weaker subfragments. In particular, we show that every formula of Safety LTL can be reduced to an equirealizable formula of the form $α\land \Box ψ$, where $α$ is a present formula over system variables and $ψ$ contains Next as the only temporal operator. The realizability problem for this new fragment, which we call $\mathsf{GX}_{\mathsf{0}}$, is also EXP-complete.

cs.LO↗

arXiv2019

Automatic White-Box Testing of First-Order Logic Ontologies

Formal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies, and their important role in the Semantic Web area, is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization can not only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of, or even preventing, the inference. In this paper, we introduce a novel, fully automatic white-box testing framework for first-order logic ontologies. Our methodology is based on the detection of inference-based redundancies in the given axiomatization. The application of the proposed testing method is fully automatic since a) the automated generation of tests is guided only by the syntax of axioms and b) the evaluation of tests is performed by automated theorem provers. Our proposal enables the detection of defects and serves to certify the grade of suitability --for reasoning purposes-- of every axiom. We formally define the set of tests that are generated from any axiom and prove that every test is logically related to redundancies in the axiom from which the test has been generated. We have implemented our method and used this implementation to automatically detect several non-trivial defects that were hidden in various first-order logic ontologies. Throughout the paper we provide illustrative examples of these defects, explain how they were found, and how each proof --given by an automated theorem-prover-- provides useful hints on the nature of each defect. Additionally, by correcting all the detected defects, we have obtained an improved version of one of the tested ontologies: Adimen-SUMO.

cs.AI↗

arXiv2016

New Steps on the Exact Learning of CNF

A major problem in computational learning theory is whether the class of formulas in conjunctive normal form (CNF) is efficiently learnable. Although it is known that this class cannot be polynomially learned using either membership or equivalence queries alone, it is open whether CNF can be polynomially learned using both types of queries. One of the most important results concerning a restriction of the class CNF is that propositional Horn formulas are polynomial time learnable in Angluin's exact learning model with membership and equivalence queries. In this work we push this boundary and show that the class of multivalued dependency formulas (MVDF) is polynomially learnable from interpretations. We then provide a notion of reduction between learning problems in Angluin's model, showing that a transformation of the algorithm suffices to efficiently learn multivalued database dependencies from data relations. We also show via reductions that our main result extends well known previous results and allows us to find alternative solutions for them.

cs.LG↗