Person:
Martí Oliet, Narciso

First Name

Narciso

Last Name

Martí Oliet

Affiliation

Universidad Complutense de Madrid

Faculty / Institute

Informática

Department

Sistemas Informáticos y Computación

Area

Lenguajes y Sistemas Informáticos

Identifiers

Full item page

Search Results

Now showing 1 - 10 of 21

Strategies in Conditional Narrowing Modulo SMT Plus Axioms
(2021-11-05) Aguirre Garcia, Luis Manuel; Martí Oliet, Narciso; Palomino, Miguel; Pita Andreu, Isabel
Narrowing calculus that uses strategies to solve reachability problems in order-sorted rewrite theories whose underlying equational logic is composed of SMT theories plus some combination of associativity, commutativity, and identity. Both the strategies and the rewrite rules are allowed to be parameterized, i.e., they may have a set of common constants that are given a value as part of the solution of a problem. The soundness and weak completeness of the calculus are proved.
The Maude strategy language
(Elsevier, 2023-06-06) Verdejo López, José Alberto; Eker, Steven; Martí Oliet, Narciso; Meseguer, José; Rubio Cuéllar, Rubén Rafael
Rewriting logic is a natural and expressive framework for the specification of concurrent systems and logics. The Maude specification language provides an implementation of this formalism that allows executing, verifying, and analyzing the represented systems. These specifications declare their objects by means of terms and equations, and provide rewriting rules to represent potentially non-deterministic local transformations on the state. Sometimes a controlled application of these rules is required to reduce non-determinism, to capture global, goal-oriented or efficiency concerns, or to select specific executions for their analysis. That is what we call a strategy. In order to express them, respecting the separation of concerns principle, a Maude strategy language was proposed and developed. The first implementation of the strategy language was done in Maude itself using its reflective features. After ample experimentation, some more features have been added and, for greater efficiency, the strategy language has been implemented in C++ as an integral part of the Maude system. This paper describes the Maude strategy language along with its semantics, its implementation decisions, and several application examples from various fields.
The semantics of the Maude strategy language
(2021-08-30) Rubio Cuéllar, Rubén Rafael; Martí Oliet, Narciso; Pita Andreu, Isabel; Verdejo López, José Alberto
The syntax and three equivalent semantics of the Maude strategy language: a set-theoretic denotational semantics, a nondeterministic small-step operational semantics, and an operational rewriting semantics. The proofs of their equivalence are included.
La gamificación en la educación universitaria: aplicación a asignaturas de programación
(2019-10-23) Gómez Martín, Marco Antonio; Segura Díaz, Clara María; Ortega Mallén, Yolanda; Verdejo López, José Alberto; Martí Oliet, Narciso; Gómez Martín, Pedro Pablo; Carballa Corredoira, Boris; García Baameiro, Daniel; Martín Sánchez, Oscar; Domenech Arellano, Jesús Javier; Costero Valero, Luis María; Jacynycz García, Viktor Shamel
Informe sobre la experiencia de aplicar técnicas de gamificación en la asignatura “Estructura de Datos y Algoritmos”, obligatoria de 2º curso en los grados impartidos en la Facultad de Informática de la UCM.
A Declarative Debugger for Maude Specifications: User Guide
(2009) Riesco Rodríguez, Adrián; Verdejo López, José Alberto; Martí Oliet, Narciso; Caballero, Rafael
We show in this guide how to use our declarative debugger for Maude specifications. Declarative debugging is a semi-automatic technique that starts from a computation considered incorrect by the user (error symptom) and locates a program fragment responsible for the error by asking questions to an external oracle, which is usually the user. In our case the debugging tree is obtained from a proof tree in a suitable semantic calculus; more concretely, we abbreviate the proof trees obtained from this calculus in order to ease and shorten the debugging process while preserving the correctness and completeness of the technique. We present the main features of our tool, what is assumed about the modules introduced by the user, the list of available commands, and the kinds of questions used during the debugging process. Then, we use several examples to illustrate how to use the debugger. We refer the interested reader to the webpage http://maude.sip.ucm.es/debugging, where these and other examples can be found together with more information about the theory underlying the debugger, its implementation and the Maude source files.
Bisimilarity congruences for open terms and term graphs via tile logic
(Springer, 2000) Bruni, Roberto; Frutos Escrig, David de; Martí Oliet, Narciso; Montanari, Ugo; Palamidessi, Catuscia
The definition of sos formats ensuring that bisimilarity on closed terms is a congruence has received much attention in the last two decades. For dealing with open terms, the congruence is usually lifted from closed terms by instantiating the free variables in all possible ways; the only alternatives considered in the literature are Larsen and Xinxin’s context systems and Rensink’s conditional transition systems. We propose an approach based on tile logic, where closed and open terms are managed uniformly, and study the ‘bisimilarity as congruence’ property for several tile formats, accomplishing different concepts of open system.
Declarative Debugging of Maude Modules
(2008) Riesco Rodríguez, Adrián; Verdejo López, José Alberto; Caballero, Rafael; Martí Oliet, Narciso
We introduce a declarative debugger for Maude modules: functional modules correspond to executable specifications in membership equational logic, while system modules correspond to rewrite theories. First we describe the construction of appropriate debugging trees for oriented equational and membership inferences and rewrite rules. These trees are obtained as the result of collapsing in proof trees all those nodes whose correction does not need any justification. We include several extended examples to illustrate the use of the declarative debugger and its main features, such as two possible constructions of the debugging tree, two different strategies to traverse it, use of a correct module to reduce the number of questions asked to the user, selection of trusted vs. suspicious statements by means of labels, and trusting of statements “on the ﬂy.” Since Maude supports the reflective features in its underlying logic, it includes a predefined META-LEVEL module providing access to metalevel concepts such as specifications or computations as usual data. This allows us to generate and navigate the debugging tree of a Maude computation using operations in Maude itself. Even the user interface of the declarative debugger for Maude can be specified in Maude itself. We describe in detail this metalevel implementation of our tool.
Notes on Model Checking and Abstraction in Rewriting Logic
(2003-12-08) Meseguer Guaita, José; Palomino, Miguel; Martí Oliet, Narciso
Alternating bit protocol as an example of compositional system specification
(2018-01-30) Martín, Óscar; Verdejo López, Alberto; Martí Oliet, Narciso
We show a complete modular specification of the alternating bit protocol. We use the syntax of Maude extended with our constructs for the synchronous composition. Also, we make intensive use of parameterized programming to encapsulate components and specify interfaces. This paper must be considered a companion to some of our previous ones.
Generalization and completeness of stochastic local search algorithms
(Elsevier, 2021-09-15) Loscos Barroso, Daniel; Martí Oliet, Narciso; Rodríguez Laguna, Ismael
We generalize Stochastic Local Search (SLS) heuristics into a unique formal model. This model has two key components: a common structure designed to be as large as possible and a parametric structure intended to be as small as possible. Each heuristic is obtained by instantiating the parametric part in a different way. Particular instances for Genetic Algorithms (GA), Ant Colony Optimization (ACO), and Particle Swarm Optimization (PSO) are presented. Then, we use our model to prove the Turing-completeness of SLS algorithms in general. The proof uses our framework to construct a GA able to simulate any Turing machine. This Turing-completeness implies that determining any non-trivial property concerning the relationship between the inputs and the computed outputs is undecidable for GA and, by extension, for the general set of SLS methods (although not necessarily for each particular method). Similar proofs are more informally presented for PSO and ACO.