Articles de revista
http://hdl.handle.net/2117/3093
Mon, 05 Oct 2015 04:07:41 GMT2015-10-05T04:07:41ZAnalysing web-orchestrations under stress using uncertainty profiles
http://hdl.handle.net/2117/77274
Analysing web-orchestrations under stress using uncertainty profiles
Gabarró Vallès, Joaquim; Serna Iglesias, María José; Stewart, Alan
An orchestration is a multi-threaded computation that invokes a number of remote services. In practice, the responsiveness of a web-service fluctuates with demand; during surges in activity service responsiveness may be degraded, perhaps even to the point of failure. An uncertainty profile formalizes a user's perception of the effects of stress on an orchestration of web-services; it describes a strategic situation, modelled by a zero-sum angel-daemon game. Stressed web-service scenarios are analysed, using game theory, in a realistic way, lying between over-optimism (services are entirely reliable) and over-pessimism (all services are broken). The 'resilience' of an uncertainty profile can be assessed using the valuation of its associated zero-sum game. In order to demonstrate the validity of the approach, we consider two measures of resilience and a number of different stress models. It is shown how (i) uncertainty profiles can be ordered by risk (as measured by game valuations) and (ii) the structural properties of risk partial orders can be analysed.
Sat, 01 Nov 2014 00:00:00 GMThttp://hdl.handle.net/2117/772742014-11-01T00:00:00ZAbstract constraint data types
http://hdl.handle.net/2117/76978
Abstract constraint data types
Fiadeiro, Jose Luis; Orejas Valdés, Fernando
Martin Wirsing is one of the earliest contributors to the area of Algebraic Specification (e.g., [2]), which he explored in a variety of domains over many years. Throughout his career, he has also inspired countless researchers in related areas. This paper is inspired by one of the domains that he explored thirty years or so after his first contributions when leading the FET Integrated Project SENSORIA [14]: the use of constraint systems to deal with non-functional requirements and preferences [13,8]. Following in his footsteps, we provide an extension of the traditional notion of algebraic data type specification to encompass soft-constraints as formalised in [1]. Finally, we relate this extension with institutions [6] and recent work on graded consequence in institutions [3].
Thu, 01 Jan 2015 00:00:00 GMThttp://hdl.handle.net/2117/769782015-01-01T00:00:00ZModel synchronization based on triple graph grammars: correctness, completeness and invertibility
http://hdl.handle.net/2117/76970
Model synchronization based on triple graph grammars: correctness, completeness and invertibility
Hermann, Frank; Ehrig, Hartmut; Orejas Valdés, Fernando; Czarnecki, Krzysztof; Diskin, Zinovy; Xiong, Yingfei; Gottmann, Susann; Engel, Thomas
Triple graph grammars (TGGs) have been used successfully to analyze correctness and completeness of bidirectional model transformations, but a corresponding formal approach to model synchronization has been missing. This paper closes this gap by providing a formal synchronization framework with bidirectional update propagation operations. They are generated from a given TGG, which specifies the language of all consistently integrated source and target models. As our main result, we show that the generated synchronization framework is correct and complete, provided that forward and backward propagation operations are deterministic. Correctness essentially means that the propagation operations preserve and establish consistency while completeness ensures that the operations are defined for all possible inputs. Moreover, we analyze the conditions under which the operations are inverse to each other. All constructions and results are motivated and explained by a running example, which leads to a case study, using concrete visual syntax and abstract syntax notation based on typed attributed graphs.
Sun, 01 Feb 2015 00:00:00 GMThttp://hdl.handle.net/2117/769702015-02-01T00:00:00ZThe ordering principle in a fragment of approximate counting
http://hdl.handle.net/2117/28288
The ordering principle in a fragment of approximate counting
Atserias Peri, Albert; Thapen, Neil
The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over T-2(1). This answers an open question raised in Buss et al. [2012] and completes their program to compare the strength of Jerabek's bounded arithmetic theory for approximate counting with weakened versions of it.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/2117/282882014-01-01T00:00:00ZProcess discovery algorithms using numerical abstract domains
http://hdl.handle.net/2117/28272
Process discovery algorithms using numerical abstract domains
Carmona Vargas, Josep; Cortadella Fortuny, Jordi
The discovery of process models from event logs has emerged as one of the crucial problems for enabling the continuous support in the life-cycle of an information system. However, in a decade of process discovery research, the algorithms and tools that have appeared are known to have strong limitations in several dimensions. The size of the logs and the formal properties of the model discovered are the two main challenges nowadays. In this paper we propose the use of numerical abstract domains for tackling these two problems, for the particular case of the discovery of Petri nets. First, numerical abstract domains enable the discovery of general process models, requiring no knowledge (e.g., the bound of the Petri net to derive) for the discovery algorithm. Second, by using divide and conquer techniques we are able to control the size of the process discovery problems. The methods proposed in this paper have been implemented in a prototype tool and experiments are reported illustrating the significance of this fresh view of the process discovery problem.
Mon, 01 Dec 2014 00:00:00 GMThttp://hdl.handle.net/2117/282722014-12-01T00:00:00ZFirefighting as a game
http://hdl.handle.net/2117/28172
Firefighting as a game
Álvarez Faura, M. del Carme; Blesa Aguilera, Maria Josep; Molter, Hendrik
The Firefighter Problem was proposed in 1995 [16] as a deterministic discrete-time model for the spread (and containment) of a fire. Its applications reach from real fires to the spreading of diseases and the containment of floods. Furthermore, it can be used to model the spread of computer viruses or viral marketing in communication networks.
In this work, we study the problem from a game-theoretical perspective. Such a context seems very appropriate when applied to large networks, where entities may act and make decisions based on their own interests, without global coordination.
We model the Firefighter Problem as a strategic game where there is one player for each time step who decides where to place the firefighters. We show that the Price of Anarchy is linear in the general case, but at most 2 for trees. We prove that the quality of the equilibria improves when allowing coalitional cooperation among players. In general, we have that the Price of Anarchy is in T(n/k) where k is the coalition size. Furthermore, we show that there are topologies which have a constant Price of Anarchy even when constant sized coalitions are considered.
Wed, 10 Dec 2014 00:00:00 GMThttp://hdl.handle.net/2117/281722014-12-10T00:00:00ZLower bounds for DNF-refutations of a relativized weak pigeonhole principle
http://hdl.handle.net/2117/28085
Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
Atserias Peri, Albert; Müller, Moritz; Oliva Valls, Sergi
The relativized weak pigeonhole principle states that if at least 2n out of n(2) pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size 2((log n)3/2-is an element of) for every is an element of > 0 and every sufficiently large n. By reducing it to the standard weak pigeonhole principle with 2n pigeons and n holes, we also show that this lower bound is essentially tight in that there exist DNF-refutations of size 2((log n)O(1)) even in R(log). For the lower bound proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition.
Mon, 01 Jun 2015 00:00:00 GMThttp://hdl.handle.net/2117/280852015-06-01T00:00:00ZBounded-width QBF is PSPACE-complete
http://hdl.handle.net/2117/27300
Bounded-width QBF is PSPACE-complete
Atserias Peri, Albert; Oliva Valls, Sergi
Tree-width and path-width are two well-studied parameters of structures that measure their similarity to a tree and a path, respectively. We show that QBF on instances with constant path-width, and hence constant tree-width, remains PSPACE-complete. This answers a question by Vardi. We also show that on instances with constant path-width and a very slow-growing number of quantifier alternations (roughly inverse-Ackermann many in the number of variables), the problem remains NP-hard. Additionally, we introduce a family of formulas with bounded tree-width that do have short refutations in Q-resolution, the natural generalization of resolution for quantified Boolean formulas.
Sat, 01 Nov 2014 00:00:00 GMThttp://hdl.handle.net/2117/273002014-11-01T00:00:00ZA boolean rule-based approach for manufacturability-aware cell routing
http://hdl.handle.net/2117/27267
A boolean rule-based approach for manufacturability-aware cell routing
Cortadella Fortuny, Jordi; Petit Silvestre, Jordi; Gómez Fernández, Sergio; Moll Echeto, Francisco de Borja
An approach for cell routing using gridded design rules is proposed. It is technology-independent and parameterizable for different fabrics and design rules, including support for multiple-patterning lithography. The core contribution is a detailed-routing algorithm based on a Boolean formulation of the problem. The algorithm uses a novel encoding scheme, graph theory to support floating terminals, efficient heuristics to reduce the computational cost, and minimization of the number of unconnected pins in case the cell is unroutable. The versatility of the algorithm is demonstrated by routing single-and double-height cells. The efficiency is ascertained by synthesizing a library with 127 cells in about one hour and a half of CPU time. The layouts derived by the implemented tool have also been compared with the ones from a commercial library; thus, showing the competitiveness of the approach for gridded geometries.
Sat, 01 Mar 2014 00:00:00 GMThttp://hdl.handle.net/2117/272672014-03-01T00:00:00ZArea-optimal transistor folding for 1-D gridded cell design
http://hdl.handle.net/2117/27265
Area-optimal transistor folding for 1-D gridded cell design
Cortadella Fortuny, Jordi
The 1-D design style with gridded design rules is gaining ground for addressing the printability issues in subwavelength photolithography. One of the synthesis problems in cell generation is transistor folding, which consists of breaking large transistors into smaller ones (legs) that can be placed in the active area of the cell. In the 1-D style, diffusion sharing between differently sized transistors is not allowed, thus implying a significant area overhead when active areas with different sizes are required. This paper presents a new formulation of the transistor folding problem in the context of 1-D design style and a mathematical model that delivers area-optimal solutions. The mathematical model can be customized for different variants of the problem, considering flexible transistor sizes and multiple-height cells. An innovative feature of the method is that area optimality can be guaranteed without calculating the actual location of the transistors. The model can also be enhanced to deliver solutions with good routability properties.
Fri, 01 Nov 2013 00:00:00 GMThttp://hdl.handle.net/2117/272652013-11-01T00:00:00Z