Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by HASLab

2021

Quantum Tree-Based Planning

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

Publication
IEEE ACCESS

Abstract
Reinforcement Learning is at the core of a recent revolution in Artificial Intelligence. Simultaneously, we are witnessing the emergence of a new field: Quantum Machine Learning. In the context of these two major developments, this work addresses the interplay between Quantum Computing and Reinforcement Learning. Learning by interaction is possible in the quantum setting using the concept of oraculization of environments. The paper extends previous oracular instances to address more general stochastic environments. In this setting, we developed a novel quantum algorithm for near-optimal decision-making based on the Reinforcement Learning paradigm known as Sparse Sampling. The proposed algorithm exhibits a quadratic speedup compared to its classical counterpart. To the best of the authors' knowledge, this is the first quantum planning algorithm exhibiting a time complexity independent of the number of states of the environment, which makes it suitable for large state space environments, where planning is otherwise intractable.

2021

A semantics and a logic for Fuzzy Arden Syntax

Authors
Gomes, L; Madeira, A; Barbosa, LS;

Publication
SOFT COMPUTING

Abstract
Fuzzy programming languages, such as the Fuzzy Arden Syntax (FAS), are used to describe behaviours which evolve in a fuzzy way and thus cannot be characterized neither by a Boolean outcome nor by a probability distribution. This paper introduces a semantics for FAS, focusing on the weighted parallel interpretation of its conditional statement. The proposed construction is based on the notion of a fuzzy multirelation which associates with each state in a program a fuzzy set of weighted possible evolutions. The latter is parametric on a residuated lattice which models the underlying semantic 'truth space'. Finally, a family of dynamic logics, equally parametric on the residuated lattice, is introduced to reason about FAS programs.

2021

Quantum Bayesian Decision-Making

Authors
de Oliveira, M; Barbosa, LS;

Publication
FOUNDATIONS OF SCIENCE

Abstract
As a compact representation of joint probability distributions over a dependence graph of random variables, and a tool for modelling and reasoning in the presence of uncertainty, Bayesian networks are of great importance for artificial intelligence to combine domain knowledge, capture causal relationships, or learn from incomplete datasets. Known as a NP-hard problem in a classical setting, Bayesian inference pops up as a class of algorithms worth to explore in a quantum framework. This paper explores such a research direction and improves on previous proposals by a judicious use of the utility function in an entangled configuration. It proposes a completely quantum mechanical decision-making process with a proven computational advantage. A prototype implementation in Qiskit (a Python-based program development kit for the IBM Q machine) is discussed as a proof-of-concept.

2021

The High-Assurance ROS Framework

Authors
Santos, A; Cunha, A; Macedo, N;

Publication
2021 IEEE/ACM 3RD INTERNATIONAL WORKSHOP ON ROBOTICS SOFTWARE ENGINEERING (ROSE 2021)

Abstract
This tool paper presents the High-Assurance ROS (HAROS) framework. HAROS is a framework for the analysis and quality improvement of robotics software developed using the popular Robot Operating System (ROS). It builds on a static analysis foundation to automatically extract models from the source code. Such models are later used to enable other sorts of analyses, such as Model Checking, Runtime Verification, and Property-based Testing. It has been applied to multiple real-world examples, helping developers find and correct various issues.

2021

Observational interpretations of hybrid dynamic logic with binders and silent transitions

Authors
Hennicker, R; Knapp, A; Madeira, A;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
We extend hybrid dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations: The first one relies on observational abstraction from the ordinary model class of a specification Sp by considering its closure under weak bisimulation. The second one uses an observational satisfaction relation for the axioms of the specification Sp, which relaxes the interpretation of state variables and the satisfaction of modal formulae by abstracting from silent transitions. We establish a formal relationship between both approaches and show that they are equivalent under mild conditions. For the proof we instantiate the previously introduced concept of a behaviour-abstractor framework to the case of dynamic logic with binders and silent transitions. As a particular outcome we provide an invariance theorem and show the Hennessy-Milner property for weakly bisimilar labelled transition systems and observational satisfaction. In the second part of the paper we integrate our results in a development methodology for reactive systems leading to two versions of observational refinement. We provide conditions under which both kinds of refinement are semantically equivalent, involving implementation constructors for relabelling, hiding, and parallel composition.

2021

Observational interpretations of hybrid dynamic logic with binders and silent transitions

Authors
Hennicker, R; Knapp, A; Madeira, A;

Publication
J. Log. Algebraic Methods Program.

Abstract

  • 45
  • 251