Person:
Rubio Cuéllar, Rubén Rafael

First Name

Rubén Rafael

Last Name

Rubio Cuéllar

URI

https://hdl.handle.net/20.500.14352/80838

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

Simulating and model checking membrane systems using strategies in Maude
(Journal of Logical and Algebraic Methods in Programming, 2021) Rubio Cuéllar, Rubén Rafael; Martí Oliet, Narciso; Pita Andreu, María Isabel; Verdejo López, José Alberto
Membrane systems are a biologically-inspired computational model based on the structure of biological cells and the way chemicals interact and traverse their membranes. Although its dynamics is described by rules, encoding membrane systems into rewriting logic is not straightforward due to its complex control mechanisms, and multiple alternatives have been proposed in the literature and implemented in the Maude specification language. The recent release of the Maude strategy language and its associated strategy-aware model checker allow specifying these systems more easily, so that they become executable and verifiable for free. An interactive environment based on a previous prototype by Oana Andrei and Dorel Lucanu is available to operate with the membranes.
An overview of the Maude strategy language and its applications
(2022) Rubio Cuéllar, Rubén Rafael; Bae, Kyungmin
In the Maude specification language, the behavior of systems is modeled by nondeterministic rewrite rules, whose free application may not always be desirable. Hence, a strategy language has been introduced to control the application of rules at a high level, without the intricacies of metaprogramming. In this paper, we give an overview of the Maude strategy language, its applications, related verification tools, and extensions, illustrated with examples.
Model checking strategy-controlled systems in rewriting logic
(Automated Software Engineering, 2021) Rubio Cuéllar, Rubén Rafael; Martí Oliet, Narciso; Pita Andreu, María Isabel; Verdejo López, José Alberto
Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive. In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared.
Maude as a library: an efficient all-purpose programming interface
(2022) Rubio Cuéllar, Rubén Rafael; Bae, Kyungmin
We present a general and efficient programming interface to Maude from Python and other programming languages. All relevant Maude entities and operations are exposed in a documented object-oriented library to facilitate the integration of Maude into external programs and vice versa. This paper describes the design and implementation of the library, explains how to use it, and discusses some mature applications.
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
(2022) Francisco Durán; Steven Eker; Santiago Escobar; Martí Oliet, Narciso; José Meseguer; Rubio Cuéllar, Rubén Rafael; Carolyn Talcott; Jasmin Blanchette; Laura Kovács; Dirk Pattinson
Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.
Project number: 18
Juez automático para el aprendizaje de bases de datos
(2021) Martín Martín, Enrique; Burgoa Muñoz, Iker; Rubio Cuéllar, Rubén Rafael; Cerro Cañizares, Pablo; Correas Fernández, Jesús; Montenegro Montes, Manuel; Riesco Rodríguez, Adrián
Proponemos desarrollar un juez automático para el aprendizaje de bases de datos. Este sistema web permitirá a los estudiantes practicar con diferentes ejercicios de bases de datos desde casa y recibir retroalimentación inmediata sobre los fallos.
The semantics of the Maude strategy language
(2021) Rubio Cuéllar, Rubén Rafael; Martí Oliet, Narciso; Pita Andreu, María 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.
Efficient Normalization of Linear Temporal Logic
(Journal of the ACM, 2024) Esparza, Javier; Rubio Cuéllar, Rubén Rafael; Salomon Sickert
In the mid 1980s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of Linear Temporal Logic (LTL) with past operators) is equivalent to a formula of the form ⋀ⁿ_i=1GF φ_i ∨ FG ψ_i where φ_i and ψ_i contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalization procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present direct and purely syntactic normalization procedures for LTL, yielding a normal form very similar to the one by Chang, Manna, and Pnueli, that exhibit only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalizes the formula, translates it into a special very weak alternating automaton, and applies a simple determinization procedure, valid only for these special automata.
Model checking strategy-controlled rewriting systems (extended version)
(2019) Martí Oliet, Narciso; Pita Andreu, María Isabel; Verdejo López, José Alberto; Rubio Cuéllar, Rubén Rafael
Strategies are widespread in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages, where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware LTL model checker for the Maude specification language, based on rewriting logic, and its strategy language. This extended version includes the proofs of the propositions in the conference paper, and a complete description of the small-step operational semantics used to define model checking for the Maude strategy language.
Strategies, model checking and branching-time properties in Maude
(Journal of Logical and Algebraic Methods in Programming, 2021) Rubio Cuéllar, Rubén Rafael; Martí Oliet, Narciso; Pita Andreu, María Isabel; Verdejo López, José Alberto
Rewriting logic and its implementation Maude are a natural and expressive framework for the specification of concurrent systems and logics. Its nondeterministic local transformations are described by rewriting rules, which can be controlled at a higher level using a builtin strategy language added to Maude 3. This specification resource would not be of much interest without tools to analyze their models, so in a previous work, we extended the Maude LTL model checker to verify strategy-controlled systems. In this paper, CTL* and μ-calculus are added to the repertoire of supported logics, after discussing which adaptations are needed for branching-time properties. The new extension relies on some external model checkers that are exposed the Maude models through general and efficient connections, profitable for future extensions and further applications. The performance of these model checkers is compared.