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

2019

On interval dynamic logic: Introducing quasi-action lattices

Autores
Santiago, R; Bedregal, B; Madeira, A; Martins, MA;

Publicação
SCIENCE OF COMPUTER PROGRAMMING

Abstract
In this paper we discuss the incompatibility between the notions of validity and impreciseness in the context of Dynamic Logics. To achieve that we consider the Lukasiewicz action lattice and its interval counterpart, we show how some validities fail in the context of intervals. In order to capture the properties of action lattices that remain valid for intervals we propose a new structure called Quasi-action Lattices which generalizes action lattices and is able to model both: The Lukasiewicz action lattice, L, and its interval counterpart, (sic). The notion of graded satisfaction relation is extended to quasi-action lattices. We demonstrate that, in the case of intervals, the relation of graded satisfaction is correct (cf. Theorem 3) with respect to the graded satisfaction relation on the Lukasiewicz action lattice. Although this theorem guarantees that satisfiability is preserved on intervals, we show that validity is not. We propose, then, to weaken the notion of validity on action lattices to designated validity on quasi-action lattices. In this context, Theorem 4 guarantees that the dynamic formula which are valid with respect to L will be designated valid with respect to (sic).

2019

Epistemic Logics with Structured Knowledge

Autores
Madeira, A; Martins, MA; Benevides, MRF;

Publicação
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Abstract
Multi-agent Dynamic Epistemic Logic, as a suitable modal logic to reason about knowledge evolving systems, has emerged in a number of contexts and scenarios. The agents knowledge in this logic is simply characterised by valuations of propositions. This paper discusses the adoption of other richer structures to make these representations, as graphs, algebras or even epistemic models. This method of building epistemic logics over richer structures is called "Epistemisation". On this view a parametric method to build such Epistemic Logics with Public Announcements is introduced. Moreover, a parametric notion of bisimulation is presented, and the modal invariance of the proposed logics, with respect to this relation, are proved. Some interesting application horizons opened with this construction are stated.

2019

A Hybrid Dynamic Logic for Event/Data-Based Systems

Autores
Hennicker, R; Madeira, A; Knapp, A;

Publicação
Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings

Abstract
We propose (formula presented) -logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs where e is an event and (formula presented) a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that (formula presented) -logic is powerful enough to characterise the semantics of an operational specification by a single (formula presented) -sentence. Thus the whole development process can rely on (formula presented) -logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition. © The Author(s) 2019.

2019

A Hybrid Dynamic Logic for Event/Data-based Systems

Autores
Hennicker, R; Madeira, A; Knapp, A;

Publicação
CoRR

Abstract

2019

d'Artagnan: A Trusted NoSQL Database on Untrusted Clouds

Autores
Pontes, R; Maia, F; Vilaça, R; Machado, N;

Publicação
38th Symposium on Reliable Distributed Systems, SRDS 2019, Lyon, France, October 1-4, 2019

Abstract
Privacy sensitive applications that store confidential information such as personal identifiable data or medical records have strict security concerns. These concerns hinder the adoption of the cloud. With cloud providers under the constant threat of malicious attacks, a single successful breach is sufficient to exploit any valuable information and disclose sensitive data. Existing privacy-aware databases mitigate some of these concerns, but sill leak critical information that can potently compromise the entire system's security. This paper proposes d'Artagnan, the first privacy-aware multi-cloud NoSQL database framework that renders database leaks worthless. The framework stores data as encrypted secrets in multiple clouds such that i) a single data breach cannot break the database's confidentiality and ii) queries are processed on the server-side without leaking any sensitive information. d'Artagnan is evaluated with industry-standard benchmark on market-leading cloud providers. © 2019 IEEE.

2019

Electrocardiogram Beat-Classification Based on a ResNet Network

Autores
Brito, C; Machado, A; Sousa, A;

Publicação
MEDINFO 2019: HEALTH AND WELLBEING E-NETWORKS FOR ALL

Abstract
When dealing with electrocardiography (ECG) the main focus relies on the classification of the heart's electric activity and deep learning has been proving its value over the years classifying the heartbeats, exhibiting great performance when doing so. Following these assumptions, we propose a deep learning model based on a ResNet architecture with convolutional ID layers to classes the beats into one of the 4 classes: normal, atrial premature contraction, premature ventricular contraction and others. Experimental results with MIT-BIH Arrhythmia Database confirmed that the model is able to perform well, obtaining an accuracy of 96% when using stochastic gradient descent (SGD) and 83% when using adaptive moment estimation (Adam), SGD also obtained F1-scores over 90% for the four classes proposed. A larger dataset was created and tested as unforeseen data for the trained model, proving that new tests should be done to improve the accuracy of it.

  • 83
  • 259