This paper introduces some novel features of Maude 2.7. We have added support for: (i) built-in order-sorted unification modulo associativity, commutativity, and identity, (ii) built-in variant generation, (iii) built-in order-sorted unification modulo a finite variant theory, and (iv) symbolic reachability modulo a finite variant theory.
Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Martí-Oliet / José Meseguer / Carolyn Talcott /
Palabras Clave: associativity commutativity and identity - Maude - narrowing - Order-sorted - unification
With the rise of Big Data technologies, distributed stream processing systems (SPS) have gained popularity in the last years. Among these systems Spark Streaming stands out as a particularly attractive option, with a growing adoption in the industry, so we will consider in particular some features of SPS in Spark Streaming. Maude is a high-performance logical framework where other systems can be easily specified and executed. In this paper we show how a Maude specification of Spark Streaming would allow developers to analyze and prove properties on their programs.
Autores: Adrián Riesco / Miguel Palomino / Narciso Martí-Oliet /
Palabras Clave: Maude - Model checking - Stream processing systems
We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unifica- tion problems u =? v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in prac- tice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incom- plete. This paper describes this associative unification algorithm imple- mented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrow- ing based symbolic reachability analysis have been extended to deal with associativity.
Autores: Francisco Durán / Steven Eker / Santiago Escobar / Narciso Marti-Oliet / Jose Meseguer / Carolyn Talcott /
Palabras Clave: associativity - narrowing - Rewriting Logic - unification
Strategies are a widespread but ambiguous concept 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 model checker built on top of the Maude specification language, based on rewriting logic, and its strategy language.Pendiente de publicación en «International Conference on Formal Structures for Computation and Deduction» (FSCD) 2019. Se envía la versión aceptada. La versión definitiva estará lista a finales de abril.
Autores: Rubén Rubio / Narciso Marti-Oliet / Isabel Pita / Alberto Verdejo /
Palabras Clave: Maude - Model checking - Rewriting Logic - strategies