Recursos de colección

RiuNet. Repositorio institucional de la Universitat de Valencia (73.332 recursos)

RiuNet es el Repositorio Institucional de la Universitat Politècnica de València, gestionado por la Biblioteca, cuyo objetivo es ofrecer acceso en Internet a la producción científica, académica y corporativa de la comunidad universitaria con la finalidad de aumentar su visibilidad y hacerla accesible y preservable.

Informes técnicos de investigación DSIC-ELP

Mostrando recursos 1 - 10 de 10

  1. Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting

    Gutiérrez Gil, Raúl; Lucas Alba, Salvador
    Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions of subterms that can be rewritten; or frozen, i.e., positions that cannot. Frozen positions can be used to denote subexpressions whose evaluation is delayed or just forbidden. A typical example is the if-then-else operator whose second and third arguments are not evaluated until the evaluation of the first argument yields either true or false. Imposing replacement restrictions can improve the termination behavior of rewriting-based computational systems. Termination of...

  2. ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance (extended version)

    María Alpuente; Santiago Escobar; Javier Espert; José Meseguer
    Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers (also called \anti-uni ers") of two structures in a typed language modulo a set of equational axioms. By supporting types and any combination of associativity (A), commutativity (C), and unity (U) algebraic axioms for function symbols, ACUOS allows reasoning about typed data structures, e.g. lists, trees, and (multi-)sets, and typical hierarchical/structural relations such as is a and part of. This paper discusses the modular ACU generalization tool ACUOS and illustrates its use in a classical arti ficial intelligence...

  3. Abstract Diagnosis for tccp using a Linear Temporal Logic

    COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
    Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which rep- resents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and some- times the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpreta- tion techniques)...

  4. A Condensed Goal-Independent Bottom-Up Fixpoint Semantics Modeling the Behavior of tccp

    COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
    In this paper, we present a new compositional bottom-up semantics for the Timed Concurrent Constraint Language (tccp in short) which is defined for the full language. In particular, is able to deal with the non- monotonic characteristic of tccp, which constitutes a substantial addi- tional technical difficulty w.r.t. other compositional denotational seman- tics present in literature (which do not tackle the full language). The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems and they may not terminate with...

  5. A Condensed Goal-Independent Bottom-Up Fixpoint Semantics Modeling the Behavior of tccp

    COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
    In this paper, we present a new compositional bottom-up semantics for the Timed Concurrent Constraint Language (tccp in short). Such semantics is defined for the full language. In particular, is able to deal with the non-monotonic characteristic of the language, which constitutes a substantial additional technical difficulty w.r.t. other compositional denotational semantics present in literature (which do not tackle the full language). The semantics is proved to be (correct and) fully abstract w.r.t. the full behavior of tccp, including infinite computations. This is particularly important since tccp has been defined to model reactive systems. The overall of these features makes our proposal...

  6. A Dependency Pair Framework for AvC-Termination

    Alarcón Jiménez, Beatriz; Gutierrez Gil, Raúl; Lucas, Salvador; Meseguer, José
    The development of powerful techniques for proving termination of rewriting modulo a set of equational axioms is essential when dealing with rewriting logic-based programming languages like CafeOBJ, Maude, ELAN, OBJ, etc. One of the most important techniques for proving termination over a wide range of variants of rewriting (strategies) is the dependency pair approach. Several works have tried to adapt it to rewriting modulo associative and commutative (AC) equational theories, and even to more general theories. However, as we discuss in this paper, no appropriate notion of minimality (and minimal chain of dependency pairs) which is well-suited to develop a...

  7. Innermost Termination of Context-Sensitive Rewriting

    Alarcón Jiménez, Beatriz; Lucas, Salvador
    Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude, OBJ, etc, which incorporate an innermost strategy which is used to break down the nondeterminism which is inherent to reduction relations. Furthermore, innermost termination of rewriting is often easier to prove than termination. Thus, under appropriate conditions, a useful strategy for proving termination of rewriting is trying to prove termination of innermost rewriting. This phenomenon has also been investigated for context-sensitive rewriting. Up to now, only few transformation-based methods have been proposed and used to (specifically) prove termination of innermost...

  8. Backward Trace Slicing for Rewriting Logic Theories -Technical report -

    Alpuente Frasnedo, María; Ballis, Demis; Espert, Javier; Romero, Daniel
    Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations...

  9. Backward Trace Slicing for Rewriting Logic Theories -Technical report -

    Alpuente Frasnedo, María; Ballis, D.; Espert, J.; Romero, D.
    Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations...

  10. On Unfolding Completeness for Rewriting Logic Theories

    Alpuente Frasnedo, María; Baggi, Michele; Ballis, Demis; Falaschi, Moreno
    Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of...

Aviso de cookies: Usamos cookies propias y de terceros para mejorar nuestros servicios, para análisis estadístico y para mostrarle publicidad. Si continua navegando consideramos que acepta su uso en los términos establecidos en la Política de cookies.