Search

In formal verification, qualitative and quantitative aspects are both relevant, and high-level formalisms are convenient to naturally specify the systems under study and their properties. In this paper, we present a framework for describing probabilistic models on top of nondeterministic specifications in the highly-expressive language Maude, based on rewriting logic. Quantitative properties can be checked and calculated on them using both probabilistic and statistical methods with external tools like PRISM, Storm, MultiVeSta, and custom implementations as backends. At the same time, the underlying nondeterministic system can be verified using the qualitative model-checking and deductive tools already available in Maude., Agencia Estatal de Investigación, Ministerio de Universidades, Depto. de Sistemas Informáticos y Computación, Fac. de Informática, TRUE, pub

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., Agencia Estatal de Investigación, Junta de Andalucía, FEDER, European Union, Generalitat Valenciana, U. S. Office of Naval Research, Depto. de Sistemas Informáticos y Computación, Fac. de Informática, TRUE, pub

A lo largo de las últimas décadas se ha intentado abordar el problema P vs NP de varias maneras. Una de las más interesantes es a través de funciones y circuitos booleanos. Con el fin de aumentar el conocimiento de este campo, presentamos en este texto un análisis sobre cómo se comportan los circuitos que computan el problema clique. Desarrollamos en detalle uno de los grandes resultados sobre circuitos monótonos: cualquier circuito monótono que compute clique necesita una cantidad superpolinómica de puertas. Después, estudiamos cómo se comportan dos métricas bajo el problema del clique. Analizamos una métrica semántica que se centra en la precisión de los resultados y una métrica sintáctica que se centra en las estructura de las funciones. Por último, realizamos experimentos y simulaciones con ambas métricas en grafos de 8 vértices y cliques de tamaño 4., Over the last decades, several attemps have been made to address the P vs NP problem. One of the most interesting ways is through boolean functions and circuits. In order to enhance the knowledge in this area, we present in this text an analysis about how the circuits that compute the clique problem behave. We elaborate on one of the great results in monotone circuits: every monotone circuit that computes the clique problem needs a superpolynomial amount of gates. Next, we study hoy two metrics behave under the clique problem. We analyze a semantic metric that focuses on the accuracy of results and a syntactic metric that focuses on the structure of functions. Finally, we perform experiments and simulations with both metrics on 8-vertex graphs and cliques of size 4.

In the reflective Maude specification language, based on rewriting logic, a strategy language has been introduced to control rule rewriting while avoiding complex and verbose metalevel programs. However, just as multiple levels of reflection are required for some metaprogramming tasks, reflective manipulation and generation of strategies are convenient in multiple situations. Some examples of reflective strategy transformations are presented, which implement special forms of evaluation or extend the strategy language while preserving its advantages.

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.

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 $\mu$-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.

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 their dynamics are described by rules, encoding membrane systems into rewriting logic is not straightforward due to its complex control mechanisms. 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 easily-extensible interactive environment transforms membrane specifications into rewrite theories controlled by appropriate strategies, and allows simulating and verifying membrane computations by means of them.

CRUE-CSIC (Acuerdos Transformativos 2023), 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., Agencia Estatal de Investigación, Ministerio de Universidades, Depto. de Sistemas Informáticos y Computación, Fac. de Informática, TRUE, pub

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., Agencia Estatal de Investigación, Ministerio de Ciencia, Innovación y Universidades, Depto. de Sistemas Informáticos y Computación, Fac. de Informática, TRUE, pub

The study of Boolean functions has made limited progress in recent years. Despite significant efforts, fundamental questions regarding the complexity and behavior of Boolean functions remain unresolved. The lack of comprehensive mathematical models and techniques hinders advancements in this field, leaving many open questions and avenues for future research. In this work, we aim to expand our limited knowledge in this field by proposing and studying two notions that could help unravel when a Boolean function is computed by super-polynomial circuits. The first notion is equanimity, which captures the condition where the output of a Boolean function is equally influenced by all input variables and/or subsets of the input. We will observe that this definition is not capable of classifying when a function cannot be computed by a polynomial circuit, although it remains a good indicator. Therefore, we need to introduce another concept, namely entanglement. This concept measures the amount of information needed from each subset of the input variables in order to obtain the output of the function. Finally, we will provide empirical evidence that a highly entangled and highly equanimous function must necessarily be computed by large circuits, ideally super-polynomial ones. This could lead to a potential new approach to demonstrate that P ̸= NP., El estudio de las funciones booleanas ha tenido un progreso limitado en los últimos años. A pesar de algunos resultados significativos, quedan todavía muchas preguntas fundamentales sobre la complejidad y el comportamiento de las funciones booleanas. La falta de modelos matemáticos completos y técnicas exhaustivas obstaculiza los avances en este campo, dejando muchas preguntas abiertas y vías para futuras investigaciones. En este trabajo, tenemos como objetivo ampliar nuestro conocimiento limitado en este campo al proponer y estudiar dos conceptos que podrían ayudar a desentrañar cuándo una función booleana es calculada por circuitos superpolinómicoss. El primer concepto es el de ecuanimidad, que pretende capturar cuándo una función booleana es igualmente influenciada por todas las variables de entrada o subconjuntos de la entrada. Observaremos que esta definición no es capaz de clasificar cuándo una función no puede ser calculada por un circuito polinómico, aunque sigue siendo un buen indicador. Por lo tanto, necesitamos introducir el otro concepto, el de enredo. Este concepto mide la cantidad de información necesaria de cada subconjunto de las variables de entrada para obtener la salida de la función. Finalmente, proporcionaremos evidencia empírica de que una función altamente enredada y ecuánime debe ser necesariamente computada por circuitos grandes, idealmente superpolinómicos. Esto podría conducir a un nuevo enfoque prometedor para demostrar que P ̸= NP.