Logics
URI permanente para esta colección:
Artículos en la categoría Logics publicados en las Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018).
Notificar un error en esta colección
Examinar
Envíos recientes
Resumen Institutions for navigational logics for graphical structuresOrejas, Fernando; Pino, Elvira; Navarro, Marisa; Lambers, Leen. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex. Article in press in Theoretical Computer Science (2018) https://doi.org/10.1016/j.tcs.2018.02.031Artículo Directions of Operational TerminationLucas, Salvador. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.A theory S in a logic supplied with an inference system is operationally terminating if no goal has an infinite well-formed proof tree. Well-formed proof trees are those which an interpreter would incrementally build when trying to solve a condition at a time from left to right. For this reason, infinite well-formed proof trees have a unique infinite branch which is called the spine. This paper introduces the notion of a directed proof tree for S and a set of formulas ?, which we call a direction. Intuitively, a direction ? is intended to collect formulas that are infinitely often used in the spine of an infinite well-formed proof tree (which is then called ?-directed) due to the repeated use of some specific inference rules. Then we introduce the notion of ?-directed operational termination of a theory as the absence of ?-directed proof trees. This new notion permits the definition of different termination properties which can be useful to distinguish different computational behaviors. It also gives a new characterization of operational termination of a (finite) theory S as the conjunction of the ?-directed operational termination of S for each direction ? in a (finite) set of directions.Artículo An Event-driven Interval Temporal Logic for Hybrid SystemsGallardo, María del Mar; Panizo, Laura. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.Nowadays, hybrid systems are present in many crucial tasks of our daily life. The hybrid character derives from the merge of continuous and discrete dynamics that are intrinsically related. The verification of critical properties of hybrid systems is of special importance, but sometimes it is not feasible due to their inherent complexity. In the last few years, several model-based testing and runtime verification techniques have been proposed to support the verification and validation of hybrid systems. In this paper, we present an interval logic that is suitable for specifying properties of event-driven hybrid systems. We introduce the syntax and semantics of the logic, and propose an automatic mechanism to transform each logic formula into a network of timed automata that can act as observers of the property in each test case using the UPPAAL tool.