Semantics
URI permanente para esta colección:
Artículos en la categoría Semantics publicados en las Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015).
Notificar un error en esta colección
Examinar
Envíos recientes
Resumen Reasoning about policy behavior in logic-based trust management systems: Some complexity results and an operational frameworkPasarella, Edelmira; Lobo, Jorge. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.In this paper we show that the logical framework proposed by Becker et al. [1] to reason about security policy behavior in a trust management context can be captured by an operational framework that is based on the language proposed by Miller in 1989 to deal with scoping and/or modules in logic programming. The framework of Becker et al. uses propositional Horn clauses to represent both policies and credentials, implications in clauses are interpreted in counterfactual logic, a Hilbertstyle proof system is defined and a system based on SAT is used to prove whether properties about credentials, permissions and policies are valid, i.e. true under all possible policies. Our contributions in this paper are three. First, we show that this kind of validation can rely on an operational semantics (derivability relation) of a language very similar to Miller’s language, which is very close to derivability in logic programs. Second, we are able to establish that, as in propositional logic, validity of formulas is a co-NP-complete problem. And third, we present a provably correct implementation of a goal-oriented algorithm for validity.Artículo Proving Continuity of Coinductive Global Bisimulation Distances: A Never Ending StoryRomero-Hernández, David; de Frutos Escrig, David; Della Monica, Dario. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.We have developed a global approach to define bisimulation distances which goes somehow further away than the bisimulation distances based on the bisimulation game, previously proposed by some other authors. Our proposal is based on the cost of transformations: how much we need to modify one of the compared processes to obtain the other. Our original definition only covered finite processes, but a coinductive approach extends it to cover infinite but finitary trees. We have shown many interesting properties of our distances, and we wanted to prove their continuity with respect to projections, bur unfortunately we have not been able to accomplish that task. However, we have obtained several partial results that we now present in this paper.Artículo A Declarative Semantics for a Fuzzy Logic Language Managing Similarities and Truth DegreesJulián Iranzo, Pascual; Moreno, Ginés; Penabad, Jaime; Vázquez, Carlos. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.This work proposes a declarative semantics based on a fuzzy variant of the classical notion of least Herbrand model for the so-called FASILL language (acronym of “Fuzzy Aggregators and Similarity Into a Logic Language”) which has being recently designed and implemented in our research group for coping with implicit/explicit truth degree annotations, a great variety of connectives and unification by similarity.Artículo A discretized operational semantics for the implementation of Hy-tccpGallardo, María del Mar; Panizo, Laura; Titolo, Laura. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.The language Hy-tccp was proposed as an extension of the Timed Concurrent Constraint paradigm (tccp) with continuous time and suitable mechanisms to handle continuous behaviors. This language provides a powerful model for hybrid and cyber-physical systems including concurrency and syn chronization features. In this paper, we propose a discretized operational semantics for Hy-tccp and an extension of the standard LTL to reason about temporal properties of Hy-tccp programs. The semantics and the logics will be the basis for the definition of formal verification and analysis tools, such as model checkers and theorem provers.