Fuzzy logic programming / Verification

URI permanente para esta colección:

https://hdl.handle.net/11705/PROLE/2021/FLPV
Artículos en la categoría Fuzzy logic programming / Verification publicados en las Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021).
Notificar un error en esta colección

Examinar

Envíos recientes

Mostrando 1 - 3 de 3
  • Miniatura
    Artículo
    Verification of ROS Navigation using Maude
    Martin-Martin, Enrique; Montenegro, Manuel; Riesco, Adrián; Rodríguez-Hortalá, Juan; Rubio, Rubén. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The emph{Navigation Stack} stands out among the different libraries available in ROS. This library provides a set of reusable components that developers can use to build robots with autonomous navigation capabilities. This is a critical component, as navigation failures could have catastrophical consequences for applications like self-driving cars. Here we show our work on the verification of the C++ code for the navfn planner, which is the main planner component of the Navigation Stack. We have ported the planner to a Maude specification, and validated their equivalence using differential testing techniques. For this purpose, we integrated the specification into ROS using a novel high performance Python interface for Maude. We then analyzed the Maude specification by means of model checking and functional verification techniques, using not only the built-in tools of Maude, but also a translation into Dafny, and a manual but systematic generation of verification conditions from the Maude specification. Along the way we also encountered counterexamples for some soundness properties —e.g. that paths should not collide with obstacles— and optimatility —paths should have the lowest possible cost— of the NavFn planner.
  • Miniatura
    Resumen
    A System implementing Fuzzy Hypothetical Datalog
    Julián Iranzo, Pascual; Sáenz Pérez, Fernando. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    This paper presents a system implementing a novel addition to a fuzzy deductive database: hypothetical queries. Such queries allow users to dynamically make assumptions on a given database instance, either by adding or removing data, without changing the instance. Further, since a fuzzy database includes fuzzy relations, these relations can also be changed with assumptions. This ability for dynamic change seamlessly enables writing “what-if” applications such as decision-support systems. Here, the new language Fuzzy Hypothetical Datalog is presented, along with an operational semantics and stratified inference. It has been implemented in a working system DES readily available on-line. IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), 2020, pp. 1-8, doi: 10.1109/FUZZ48607.2020.9177715.
  • Miniatura
    Artículo
    Seeking a Safe and Efficient Similarity-based Unfolding Rule
    Julián Iranzo, Pascual; Moreno, Ginés; Riaza Valverde, José Antonio. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    The unfolding transformation has been widely used in many declarative frameworks for improving the efficiency of programs. Inspired by our previous experiences in fuzzy logic languages not dealing with similarity relations, in this work we try to adapt such operation to the so-called FASILL language (acronym of "Fuzzy Aggregators and Similarity Into a Logic Language") which has been developed in our research group for coping with implicit/explicit truth degree annotations, a great variety of connectives and unification by similarity. The traditional unfolding transformation is based on the application of unifiers on the heads and computational steps on the bodies of program rules. However, when considering similarity relations, the premature generation and application of weak (similarity-based) unifers at unfolding time could destroy the correctness of the transformation. In this paper we study how to avoid this risk by compiling what we call similarity constraints on transformed rules, whose further evaluation is delayed at running time. Moreover, our technique minimizes the size and number of occurrences of such constructs in transformed programs to gain efficiency while preserving semantics.