ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals
http://hdl.handle.net/2117/3092
Fri, 12 Feb 2016 23:11:50 GMT2016-02-12T23:11:50ZReasoning about policy behavior in logic-based trust management systems: Some complexity results and an operational framework
http://hdl.handle.net/2117/82625
Reasoning about policy behavior in logic-based trust management systems: Some complexity results and an operational framework
Pasarella Sánchez, Ana Edelmira; Lobo, Jorge
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 Hilbert-style 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.
Fri, 05 Feb 2016 12:38:45 GMThttp://hdl.handle.net/2117/826252016-02-05T12:38:45ZPasarella Sánchez, Ana EdelmiraLobo, JorgeIn 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 Hilbert-style 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.A cost-benefit analysis of continuous assessment
http://hdl.handle.net/2117/82536
A cost-benefit analysis of continuous assessment
Duch Brown, Amalia; Gabarró Vallès, Joaquim; Petit Silvestre, Jordi; Blesa Aguilera, Maria Josep; Serna Iglesias, María José
The first course on programming is fundamental in the Facultat d’Informàtica de Barcelona. After a major redesign of the Programming-1 course in 2006 to give it a more practical flavor, an increasing number of measures have been undertaken over the years to try to increase its pass rate while maintaining a fixed quality level. These measures, that can be roughly summarized as an important increase in assessment, imply an increase in the workload of both students and instructors that does not always correspond to the increase of pass rate they provide. In this paper, and within the context of this course, we analyze quantitatively the amount of work required from faculty to implement the series of measures and we conclude that, within this course, continuous assessment is expensive and has reached its limit.
Thu, 04 Feb 2016 09:49:32 GMThttp://hdl.handle.net/2117/825362016-02-04T09:49:32ZDuch Brown, AmaliaGabarró Vallès, JoaquimPetit Silvestre, JordiBlesa Aguilera, Maria JosepSerna Iglesias, María JoséThe first course on programming is fundamental in the Facultat d’Informàtica de Barcelona. After a major redesign of the Programming-1 course in 2006 to give it a more practical flavor, an increasing number of measures have been undertaken over the years to try to increase its pass rate while maintaining a fixed quality level. These measures, that can be roughly summarized as an important increase in assessment, imply an increase in the workload of both students and instructors that does not always correspond to the increase of pass rate they provide. In this paper, and within the context of this course, we analyze quantitatively the amount of work required from faculty to implement the series of measures and we conclude that, within this course, continuous assessment is expensive and has reached its limit.RTL synthesis: From logic synthesis to automatic pipelining
http://hdl.handle.net/2117/82027
RTL synthesis: From logic synthesis to automatic pipelining
Cortadella Fortuny, Jordi; Galceran Oms, Marc; Kishinevsky, Mike; Sapatnekar, Sachin S.
Design automation has been one of the main propellers of the semiconductor industry with logic synthesis being one of the core technologies in this field. This article reviews the evolution of logic synthesis until the advent of techniques for automatic pipelining based on elastic timing, either synchronous or asynchronous. The emergence of these techniques can enable a productive interaction with tools that can do microarchitectural exploration of complex designs.
Tue, 26 Jan 2016 10:28:37 GMThttp://hdl.handle.net/2117/820272016-01-26T10:28:37ZCortadella Fortuny, JordiGalceran Oms, MarcKishinevsky, MikeSapatnekar, Sachin S.Design automation has been one of the main propellers of the semiconductor industry with logic synthesis being one of the core technologies in this field. This article reviews the evolution of logic synthesis until the advent of techniques for automatic pipelining based on elastic timing, either synchronous or asynchronous. The emergence of these techniques can enable a productive interaction with tools that can do microarchitectural exploration of complex designs.The robustness of periodic orchestrations in uncertain evolving environments
http://hdl.handle.net/2117/82017
The robustness of periodic orchestrations in uncertain evolving environments
Castro Rabal, Jorge; Gabarró Vallès, Joaquim; Serna Iglesias, María José; Stewart, Alan
A framework for assessing the robustness of long-duration repetitive orchestrations in uncertain evolving environments is proposed. The model assumes that service-based evaluation environments are stable over short time-frames only; over longer periods service-based environments evolve as demand fluctuates and contention for shared resources varies.
The behaviour of a short-duration orchestration E in a stable environment is assessed by an uncertainty profile U and a corresponding zero-sum angel-daemon game Gamma (U).
Here the angel-daemon approach is extended to assess evolving environments by means of a subfamily of stochastic games. These games are called strategy oblivious because their transition probabilities are strategy independent. It is shown that the value of a strategy oblivious stochastic game is well defined and that it can be computed by solving a linear system. Finally, the proposed stochastic framework is used to assess the evolution of the Gabrmn IT system.
Tue, 26 Jan 2016 08:45:30 GMThttp://hdl.handle.net/2117/820172016-01-26T08:45:30ZCastro Rabal, JorgeGabarró Vallès, JoaquimSerna Iglesias, María JoséStewart, AlanA framework for assessing the robustness of long-duration repetitive orchestrations in uncertain evolving environments is proposed. The model assumes that service-based evaluation environments are stable over short time-frames only; over longer periods service-based environments evolve as demand fluctuates and contention for shared resources varies.
The behaviour of a short-duration orchestration E in a stable environment is assessed by an uncertainty profile U and a corresponding zero-sum angel-daemon game Gamma (U).
Here the angel-daemon approach is extended to assess evolving environments by means of a subfamily of stochastic games. These games are called strategy oblivious because their transition probabilities are strategy independent. It is shown that the value of a strategy oblivious stochastic game is well defined and that it can be computed by solving a linear system. Finally, the proposed stochastic framework is used to assess the evolution of the Gabrmn IT system.A MOOC on approaches to machine translation
http://hdl.handle.net/2117/81278
A MOOC on approaches to machine translation
Ruiz Costa-Jussà, Marta; Formiga, Lluís; Torrillas Tostado, Oriol; Petit Silvestre, Jordi; Rodríguez Fonollosa, José Adrián
This paper describes the design, development, and analysis of a MOOC entitled “Approaches to Machine Translation: Rule-based, statistical and hybrid”, and provides lessons learned and conclusions to be taken into account in the future. The course was developed within the Canvas platform, used by recognized European universities. It contains video-lectures, quizzes, and laboratory assignments. Evaluation was through on-line quizzes, programming assignments assessed by means of a specific code evaluation, and peer-to-peer strategies. This MOOC allowed people from various fields to be introduced to the theory and practice of Machine Translation. It also enabled us to internationally publicize various tools developed at the Universitat Politècnica de Catalunya.
Tue, 12 Jan 2016 13:04:11 GMThttp://hdl.handle.net/2117/812782016-01-12T13:04:11ZRuiz Costa-Jussà, MartaFormiga, LluísTorrillas Tostado, OriolPetit Silvestre, JordiRodríguez Fonollosa, José AdriánThis paper describes the design, development, and analysis of a MOOC entitled “Approaches to Machine Translation: Rule-based, statistical and hybrid”, and provides lessons learned and conclusions to be taken into account in the future. The course was developed within the Canvas platform, used by recognized European universities. It contains video-lectures, quizzes, and laboratory assignments. Evaluation was through on-line quizzes, programming assignments assessed by means of a specific code evaluation, and peer-to-peer strategies. This MOOC allowed people from various fields to be introduced to the theory and practice of Machine Translation. It also enabled us to internationally publicize various tools developed at the Universitat Politècnica de Catalunya.Modelling service-oriented computing with temporal symbolic graph transformation systems
http://hdl.handle.net/2117/81101
Modelling service-oriented computing with temporal symbolic graph transformation systems
Mylonakis Pascual, Nicolás; Orejas Valdés, Fernando; Fiadeiro, José
In this paper, we present a novel semantics for an essential aspect of service-oriented computing: the mechanism through which systems evolve through a symbiosis of state transformations and run-time service discovery and binding.
The semantics is based on a new notion of temporal symbolic graph-transformation systems:
in temporal symbolic graphs, interfaces can be specified using temporal logic, and service-level agreements can be specified in that logic's propositional fragment.
An important advantage of our framework is that it can be supported by tools that implement temporal symbolic graph transformations, which would also provide a means of animating service-oriented systems evolution.
We illustrate our semantics with a simple trip-booking service.
Thu, 07 Jan 2016 12:16:21 GMThttp://hdl.handle.net/2117/811012016-01-07T12:16:21ZMylonakis Pascual, NicolásOrejas Valdés, FernandoFiadeiro, JoséIn this paper, we present a novel semantics for an essential aspect of service-oriented computing: the mechanism through which systems evolve through a symbiosis of state transformations and run-time service discovery and binding.
The semantics is based on a new notion of temporal symbolic graph-transformation systems:
in temporal symbolic graphs, interfaces can be specified using temporal logic, and service-level agreements can be specified in that logic's propositional fragment.
An important advantage of our framework is that it can be supported by tools that implement temporal symbolic graph transformations, which would also provide a means of animating service-oriented systems evolution.
We illustrate our semantics with a simple trip-booking service.Entailment among probabilistic implications
http://hdl.handle.net/2117/79017
Entailment among probabilistic implications
Atserias, Albert; Balcázar Navarro, José Luis
We study a natural variant of the implicational fragment of propositional logic. Its formulas are pairs of conjunctions of positive literals, related together by an implicational-like connective, the semantics of this sort of implication is defined in terms of a threshold on a conditional probability of the consequent, given the antecedent: we are dealing with what the data analysis community calls confidence of partial implications or association rules. Existing studies of redundancy among these partial implications have characterized so far only entailment from one premise and entailment from two premises. By exploiting a previously noted alternative view of this entailment in terms of linear programming duality, we characterize exactly the cases of entailment from arbitrary numbers of premises. As a result, we obtain decision algorithms of better complexity, additionally, for each potential case of entailment, we identify a critical confidence threshold and show that it is, actually, intrinsic to each set of premises and antecedent of the conclusion.
Wed, 11 Nov 2015 12:38:12 GMThttp://hdl.handle.net/2117/790172015-11-11T12:38:12ZAtserias, AlbertBalcázar Navarro, José LuisWe study a natural variant of the implicational fragment of propositional logic. Its formulas are pairs of conjunctions of positive literals, related together by an implicational-like connective, the semantics of this sort of implication is defined in terms of a threshold on a conditional probability of the consequent, given the antecedent: we are dealing with what the data analysis community calls confidence of partial implications or association rules. Existing studies of redundancy among these partial implications have characterized so far only entailment from one premise and entailment from two premises. By exploiting a previously noted alternative view of this entailment in terms of linear programming duality, we characterize exactly the cases of entailment from arbitrary numbers of premises. As a result, we obtain decision algorithms of better complexity, additionally, for each potential case of entailment, we identify a critical confidence threshold and show that it is, actually, intrinsic to each set of premises and antecedent of the conclusion.SafeRazor: Metastability-robust adaptive clocking in resilient circuits
http://hdl.handle.net/2117/78809
SafeRazor: Metastability-robust adaptive clocking in resilient circuits
Cannizzaro, Marco; Beer, Salomon; Cortadella Fortuny, Jordi; Ginosar, Ran; Lavagno, Luciano
Razor-based circuits can run faster or at a lower voltage than those designed to work at the worst case corner. However, all known implementations are prone to failures due to the non-deterministic timing behavior introduced by metastability, even in the case where sufficient time is left for resolution. This paper analyzes the causes why Razor-based circuits fail and proposes a new scheme combining the Razor principle with stoppable clocks in a GALS setting. This scheme avoids any timing failure due to metastability and does not require any checkpointing or pipeline restarting logic, other than the usual auxiliary latch to store valid data. The experiments show how the Razor principle can be extended to any generic logic circuit, and not just to microprocessors with sophisticated pipeline flush/recovery mechanisms. In this way, the performance/power benefits of Razor can be adopted without the complex architectural changes required by the various Razor schemes in the literature.
Thu, 05 Nov 2015 09:20:57 GMThttp://hdl.handle.net/2117/788092015-11-05T09:20:57ZCannizzaro, MarcoBeer, SalomonCortadella Fortuny, JordiGinosar, RanLavagno, LucianoRazor-based circuits can run faster or at a lower voltage than those designed to work at the worst case corner. However, all known implementations are prone to failures due to the non-deterministic timing behavior introduced by metastability, even in the case where sufficient time is left for resolution. This paper analyzes the causes why Razor-based circuits fail and proposes a new scheme combining the Razor principle with stoppable clocks in a GALS setting. This scheme avoids any timing failure due to metastability and does not require any checkpointing or pipeline restarting logic, other than the usual auxiliary latch to store valid data. The experiments show how the Razor principle can be extended to any generic logic circuit, and not just to microprocessors with sophisticated pipeline flush/recovery mechanisms. In this way, the performance/power benefits of Razor can be adopted without the complex architectural changes required by the various Razor schemes in the literature.High evolutionary turnover of satellite families in Caenorhabditis
http://hdl.handle.net/2117/78807
High evolutionary turnover of satellite families in Caenorhabditis
Subirana Torrent, Juan A.; Albà, M. Mar; Messeguer Peypoch, Xavier
Background: The high density of tandem repeat sequences (satellites) in nematode genomes and the availability of genome sequences from several species in the group offer a unique opportunity to better understand the evolutionary dynamics and the functional role of these sequences. We take advantage of the previously developed SATFIND program to study the satellites in four Caenorhabditis species and investigate these questions.; Methods: The identification and comparison of satellites is carried out in three steps. First we find all the satellites present in each species with the SATFIND program. Each satellite is defined by its length, number of repeats, and repeat sequence. Only satellites with at least ten repeats are considered. In the second step we build satellite families with a newly developed alignment program. Satellite families are defined by a consensus sequence and the number of satellites in the family. Finally we compare the consensus sequence of satellite families in different species.; Results: We give a catalog of individual satellites in each species. We have also identified satellite families with a related sequence and compare them in different species. We analyze the turnover of satellites: they increased in size through duplications of fragments of 100-300 bases. It appears that in many cases they have undergone an explosive expansion. In C. elegans we have identified a subset of large satellites that have strong affinity for the centromere protein CENP-A. We have also compared our results with those obtained from other species, including one nematode and three mammals.; Conclusions: Most satellite families found in Caenorhabditis are species-specific; in particular those with long repeats. A subset of these satellites may facilitate the formation of kinetochores in mitosis. Other satellite families in C. elegans are either related to Helitron transposons or to meiotic pairing centers.
Thu, 05 Nov 2015 09:02:56 GMThttp://hdl.handle.net/2117/788072015-11-05T09:02:56ZSubirana Torrent, Juan A.Albà, M. MarMesseguer Peypoch, XavierBackground: The high density of tandem repeat sequences (satellites) in nematode genomes and the availability of genome sequences from several species in the group offer a unique opportunity to better understand the evolutionary dynamics and the functional role of these sequences. We take advantage of the previously developed SATFIND program to study the satellites in four Caenorhabditis species and investigate these questions.; Methods: The identification and comparison of satellites is carried out in three steps. First we find all the satellites present in each species with the SATFIND program. Each satellite is defined by its length, number of repeats, and repeat sequence. Only satellites with at least ten repeats are considered. In the second step we build satellite families with a newly developed alignment program. Satellite families are defined by a consensus sequence and the number of satellites in the family. Finally we compare the consensus sequence of satellite families in different species.; Results: We give a catalog of individual satellites in each species. We have also identified satellite families with a related sequence and compare them in different species. We analyze the turnover of satellites: they increased in size through duplications of fragments of 100-300 bases. It appears that in many cases they have undergone an explosive expansion. In C. elegans we have identified a subset of large satellites that have strong affinity for the centromere protein CENP-A. We have also compared our results with those obtained from other species, including one nematode and three mammals.; Conclusions: Most satellite families found in Caenorhabditis are species-specific; in particular those with long repeats. A subset of these satellites may facilitate the formation of kinetochores in mitosis. Other satellite families in C. elegans are either related to Helitron transposons or to meiotic pairing centers.FrogCOL and FrogMIS: new decentralized algorithms for finding large independent sets in graphs
http://hdl.handle.net/2117/77894
FrogCOL and FrogMIS: new decentralized algorithms for finding large independent sets in graphs
Blum, Christian; Calvo, Borja; Blesa Aguilera, Maria Josep
Finding large (and generally maximal) independent sets of vertices in a given graph is a fundamental problem in distributed computing. Applications include, for example, facility location and backbone formation in wireless ad hoc networks. In this paper, we study a decentralized (or distributed) algorithm inspired by the calling behavior of male Japanese tree frogs, originally introduced for the graph-coloring problem, for its potential usefulness in the context of finding large independent sets. Moreover, we adapt this algorithm to directly produce maximal independent sets without the necessity of first producing a graph-coloring solution. Both algorithms are compared to a wide range of decentralized algorithms from the literature on a diverse set of benchmark instances for the maximal independent set problem. The results show that both algorithms compare very favorably to their competitors.
Mon, 19 Oct 2015 14:33:02 GMThttp://hdl.handle.net/2117/778942015-10-19T14:33:02ZBlum, ChristianCalvo, BorjaBlesa Aguilera, Maria JosepFinding large (and generally maximal) independent sets of vertices in a given graph is a fundamental problem in distributed computing. Applications include, for example, facility location and backbone formation in wireless ad hoc networks. In this paper, we study a decentralized (or distributed) algorithm inspired by the calling behavior of male Japanese tree frogs, originally introduced for the graph-coloring problem, for its potential usefulness in the context of finding large independent sets. Moreover, we adapt this algorithm to directly produce maximal independent sets without the necessity of first producing a graph-coloring solution. Both algorithms are compared to a wide range of decentralized algorithms from the literature on a diverse set of benchmark instances for the maximal independent set problem. The results show that both algorithms compare very favorably to their competitors.