Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Publicações

Publicações por HASLab

2024

Paraconsistency for the Working Software Engineer (Extended Abstract)

Autores
Barbosa, LS;

Publicação
Software Engineering and Formal Methods - 22nd International Conference, SEFM 2024, Aveiro, Portugal, November 6-8, 2024, Proceedings

Abstract
Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. This lecture summarises recent joint work with Juliana Cunha, Alexandre Madeira and Ana Cruz on a variant of transition systems endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values. Such structures are called paraconsistent transition systems, the qualifier stressing a connection to paraconsistent logic, a logic taking inconsistent information as potentially informative. A coalgebraic perspective on this family of structures is also discussed. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

2024

Secure two-party computation via measurement-based quantum computing

Autores
Rahmani, Z; Pinto, AHMN; Barbosa, LMDCS;

Publicação
QUANTUM INFORMATION PROCESSING

Abstract
Secure multiparty computation (SMC) provides collaboration among multiple parties, ensuring the confidentiality of their private information. However, classical SMC implementations encounter significant security and efficiency challenges. Resorting to the entangled Greenberger-Horne-Zeilinger (GHZ) state, we propose a quantum-based two-party protocol to compute binary Boolean functions, with the help of a third party. We exploit a technique in which a random Z-phase rotation on the GHZ state is performed to achieve higher security. The security and complexity analyses demonstrate the feasibility and improved security of our scheme compared to other SMC Boolean function computation methods. Additionally, we implemented the proposed protocol on the IBM QisKit and found consistent outcomes that validate the protocol's correctness.

2024

Trainability issues in quantum policy gradients

Autores
Sequeira, A; Santos, LP; Barbosa, LS;

Publicação
MACHINE LEARNING-SCIENCE AND TECHNOLOGY

Abstract
This research explores the trainability of Parameterized Quantum Circuit-based policies in Reinforcement Learning, an area that has recently seen a surge in empirical exploration. While some studies suggest improved sample complexity using quantum gradient estimation, the efficient trainability of these policies remains an open question. Our findings reveal significant challenges, including standard Barren Plateaus with exponentially small gradients and gradient explosion. These phenomena depend on the type of basis-state partitioning and the mapping of these partitions onto actions. For a polynomial number of actions, a trainable window can be ensured with a polynomial number of measurements if a contiguous-like partitioning of basis-states is employed. These results are empirically validated in a multi-armed bandit environment.

2024

The Blocklace: A Universal, Byzantine Fault-Tolerant, Conflict-free Replicated Data Type

Autores
Almeida, PS; Shapiro, E;

Publicação
CoRR

Abstract

2024

A Framework for Consistency Models in Distributed Systems

Autores
Almeida, PS;

Publicação
CoRR

Abstract

2024

Validating multiple variants of an automotive light system with Alloy 6

Autores
Cunha, A; Macedo, N; Liu, C;

Publicação
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER

Abstract
This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.

  • 8
  • 256