Cloud computing enables elasticity – rapid provisioning and deprovisioning of computational re-sources. Elasticity allows cloud users to quickly adapt resource allocation to meet changes in theirworkloads. For cloud providers, elasticity complicates capacity management as the amount of re-sources that can be requested by users is unknown and can vary significantly over time. Overbookingtechniques allow providers to increase utilization of their data centers. For safe overbooking, cloudproviders need admission control mechanisms to handle the tradeoff between increased utilization(and revenue), and risk of exhausting resources, potentially resulting in penalty fees and/or lost cus-tomers. We propose a flexible approach (implemented with fuzzy logic programming) to admissioncontrol and the associated risk estimation. Our measures exploit different fuzzy logic operators inorder to model optimistic, realistic, and pessimistic behaviour under uncertainty. An experimen-tal evaluation confirm that our fuzzy admission control approach can significantly increase resourceutilization while minimizing the risk of exceeding the total available capacity.
Autores: Fernando Orejas / Elvira Pino /
Palabras Clave: Admission Control - Cloud Computing - Fuzzy Logic Programming - Risk Assessment
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.031
Autores: Fernando Orejas / Elvira Pino / Marisa Navarro / Leen Lambers /
Palabras Clave: Graph logics - Institutions - Navigational logics
In the context of software model-driven development, artifacts are specified by several models describing different aspects, e.g., different views, dynamic behaviour, structure, etc. Then, a given set of models is emph{consistently integrated} if they describe some artifact. Along the process of designing and implementing an artifact, and also after the artifact is implemented, it may be common to modify or update some aspects of a given model, or of several models. These changes may cause an inconsistency between the given set of models. To restore consistency, we have to emph{propagate} the given modifications to the rest of the models. This process is called emph{model synchronization}. If each time we propagate the updates on just one model, synchronization is emph{sequential}, but if we propagate simultaneously updates on two models, synchronization is called emph{concurrent}. The sequential case is quite simpler than the concurrent one, since in the latter case we may have to deal with conflicts between the modifications applied to different models, implying that we may need to backtrack some updates. For simplicity, we assume that the set of models describing an artifact consists just of two models.Then, following the ideas of a previous paper on sequential synchronization, in the current paper, we propose an incremental procedure for the concurrent case, meaning that our procedure does not build the resulting models from scratch, but it only modifies the parts of the models affected by the update.
Autores: Elvira Pino / Marisa Navarro / Fernando Orejas /
Palabras Clave: (Concurrent) Model Synchronization - Incremental Model Synchronization - Model Transformation - Triple Graph Grammars
In this paper we provide semantics for normal logic programs enriched with structuring mechanisms and scoping rules. Specifically, we consider constructive negation and expressions of the form QG in goals, where Q is a program unit, G is a goal and stands for the so-called embedded implication. Allowing the use of these expressions can be seen as adding block structuring to logic programs. In this context, we consider static and dynamic rules for visibility in blocks. In particular, we provide new semantic definitions for the class of normal logic programs with both visibility rules. For the dynamic case we follow a standard approach. We first propose an operational semantics. Then, we define a model-theoretic semantics in terms of ordered structures which are a kind of intuitionistic Beth structures. Finally, an (effective) fixpoint semantics is provided and we prove the equivalence of these three definitions. In order to deal with the static case, we first define an operational semantics and then we present an alternative semantics in terms of a transformation of the given structured programs into flat ones. We finish by showing that this transformation preserves the computed answers of the given static program.
Autores: Edelmira Pasarella / Fernando Orejas / Elvira Pino / Marisa Navarro /
Palabras Clave: embedded implication - intuitionistic structures - normal logic programs - Semantics - structuring mechanism - visibility rules
Graph databases are now playing an important role, not only because they allow us to overcome some limitations of relational databases, but also because they provide a good model for searching the web. In particular, graph databases differ from relational databases in that the topology of data is as important as the data itself. Thus, typical graph database queries are navigational, asking whether some nodes are connected by paths satisfying some specific properties. While relational databases were designed upon logical and algebraic foundations, the development of graph databases has been quite ad-hoc. In this sense, the aim of this paper is to provide them with some logical foundations. More precisely, in previous work we introduced a navigational logic, called +AFw-GNL+AFw (Graph Navigational Logic) that allows us to describe graph navigational properties. Moreover, this logic is equipped with a deductive tableau method that we proved to be sound and complete.In the current paper, we show how graph queries +AHsAXA-it +AOA la+AH0 Cypher can be expressed using a fragment of +AFw-GNL, defining for them a logical and an operational semantics. Moreover, we show that this operational semantics is sound and complete.
Autores: Elvira Pino / Fernando Orejas / Nicos Mylonakis / Edelmira Pasarella /
Palabras Clave: Graph Databases - Logic of Graphs - Query Languages
In this work, we present an approach for specifying the structure of XML documents using three kinds of constraints based on XPath, together with a sound and complete method for reasoning about them. Currently, the standard specification of classes of XML documents is done by means of DTDs or XML Schemas. In both cases, we essentially describe the abstract syntax of the class of documents and the types of its attributes. This is quite limited. In particular, we may want to state more complex conditions about the structure of documents in a given class or about their contents. For example, with respect to the structure of documents, we may want to state that if an element includes an attribute with a given content, then these documents should not include some other element. Or, with respect to the contents of documents, we may want to express that the value of some numeric attribute of a certain element is smaller than the value of another attribute of a different element. In this paper, we concentrate on the specification of the structure of documents, not paying much attention to their contents. In this sense, we present an abstract approach for the specification of (the structure of) classes of XML documents using sets of constraints that are based on XPath [8, 9] queries, as given in [4], using the concept of tree patterns. Roughly, a tree pattern describes a basic property on the structure of documents. Its root repre sents the root of documents. Nodes represent elements that must be present on the given documents and their labels represent their contents, i.e. the names of elements and their value, if any. A wild card (the symbol ∗), means that we don’t know or we don’t care about the contents of that element. Finally, single edges represent parent/child relations between elements, while double edges represent a descendant relationship between elements. Again, if any of these two relations is included in a tree pattern, then it should also be included in the documents satisfying that property. For instance, on the left of Fig. 1 we show a tree pattern p describing documents D whose root node is labelled with a, some child node of the root node in D is labelled b, and some descendant node of the root node in D has two child nodes labelled c and d, respectively. Similarly, we represent, in an abstract way, XML documents using the same kind of trees. The difference between a document and a tree pattern is that a document does not include double edges or wildcards. For example, on the right of Fig. 1 we show a document that satisfies the pattern on the left. In particular, we may see that the root of the document is labelled by a. Moreover, that root has a child node labelled b and a descendant node (the element labelled f) that has two child nodes labelled c and d, respectively. We consider three kinds of (atomic) constraints. The first one, called positive constraints, are tree patterns. The second one are negative constraints, ¬p, where p is a tree pattern, expressing that documents should not satisfy p. Finally, the third sort of constraint are conditional constraints, written ∀(c : p → q), where both p and q are tree patterns. Roughly speaking, these constraints express that if a document satisfies p then it must also satisfy q. Moreover, these constraints can be combined using the connectives ∧ and ∨. These kinds of constraints are similar to the graph constraints studied in [6, 7] in the context of graph transformation. The work presented in those papers, shows how to use graph constraints as a specification formalism, and how to reason about these specifications. However, the application of these ideas to our setting is not trivial. Specifically, the descendant relation in our constraints makes non-trivial the application of these techniques since, the descendent relation would be second-order in the logic of graph constraints defined in [6, 7]. Obviously, there are conditions on the structure of XML documents that are not expressible using the kind of constraints studied in this paper. However, our experience in the area of graph transformation [6, 7] shows that, in practice, these constraints are sufficient in most cases. Nevertheless, we believe that the ideas presented here can be extended to a class of XML constraints, similar to the class of nested graph conditions that has been shown equivalent to first-order logic of graphs [2]. However, we also believe that this extension is not straightforward. Since our aim is to be able to reason about these specifications, we present inference rules that are shown, by means of tableaux, to define a sound and complete refutation procedure for checking satisfiability of a given specification. We strongly believe that satisfiability problem for this class of constraints is only semidecidable, since we believe that it would be similar to the (un)decidability of the satisfiability problem for the Horn clause fragment of first-order logic. As a consequence, if a given specification is inconsistent, we can be sure that our procedure will terminate showing that unsatisfiability. However, our procedure may not terminate if the given specification is satisfiable. Nevertheless, we may like to have an idea about the performance of our approach when the procedure terminates. One could think, that this performance would be quite poor, since checking if there is a monomorphism between two trees (a basic operation in our deduction procedure) is an NP-complete problem [3]. Actually, this is not our experience with the tool that we have implemented [1]. We think that the situation is similar to what happens with graph transformation tools. In these tools, applying a graph transformation rule means finding a subgraph isomorphism, which is also a wellknown NP-complete problem. However, the fact that the graphs are typed (in our case, the trees are labelled), in practice, reduces considerably the search. Finally, in the future, we plan to extend our approach to consider also cross-references and properties about the contents of documents. The former problem means, in fact, to extend our approach to graphs and graph patterns. For the latter case, we plan to follow the same approach that we used to extend our results for graphs in [6, 7] to the case of attributed graphs in [5].
Autores: Marisa Navarro / Fernando Orejas / Elvira Pino /
Palabras Clave:
