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
About
Download Photo HD

About

Alexandre is a member  HASLab INESC TEC currently developing the postdoc project "dynamic logics for every season" supported by the FCT (Portuguese Foundation for Science and technology) with the individual grant SFRH /BPD/103004/2014. The project is hosted in HASLab INESC TEC and CIDMA over the scientific supervision of Luís S. Barbosa (Informatics Dep. of Univ. Minho) and Manuel A. Martins(Mathematics Dep. of Univ. Aveiro).

Alexandre is also coordinating the FCT R&D project DaLí: Dynamic logics for cyber-physical systems: towards contract based design.

Research interest:

- Mathematical Foundations of Software Engineering

- Algebraic and logical methods for software development

- Parametric generation of Modal/Hybrid/Dynamic Logics

- Process Algebra 

Interest
Topics
Details

Details

002
Publications

2020

Introducing Synchrony in Fuzzy Automata

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

Publication
Electronic Notes in Theoretical Computer Science

Abstract

2020

Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions

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

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
We extend dynamic logic with binders (for state variables) by distinguishing between observable and silent transitions. This differentiation gives rise to two kinds of observational interpretations of the logic: abstractor and behavioural specifications. Abstractor specifications relax the standard model class semantics of a specification by considering its closure under weak bisimulation. Behavioural specifications, however, rely on a behavioural satisfaction relation which relaxes the interpretation of state variables and the satisfaction of modal formulas and by abstracting from silent transitions. A formal relation between abstractor and behavioural specifications is provided which shows that both coincide semantically 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. © 2020, Springer Nature Switzerland AG.

2020

A Fuzzy Modal Logic for Fuzzy Transition Systems

Authors
Jain, M; Madeira, A; Martins, MA;

Publication
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Abstract
This paper intends to contribute with a new fuzzy modal logic to model and reason about transition systems involving uncertainty in behaviours. Our formalism supports fuzziness at transitions and on the proposition symbols assignment levels. Against of other approaches in the literature, our bisimulation and bisimilarity notions generalise the analogous standard notions of classic modal logic and of process algebras. Moreover, the outcome of our logic is also fuzzy, with the semantic interpretation of connectives supported by the Godel algebra.

2020

DaLi - Dynamic Logic, new trends and applications

Authors
Benevides, MRF; Madeira, A;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract

2019

Taming Hierarchical Connectors

Authors
Proença, J; Madeira, A;

Publication
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
Building and maintaining complex systems requires good software engineering practices, including code modularity and reuse. The same applies in the context of coordination of complex component-based systems. This paper investigates how to verify properties of complex coordination patterns built hierarchically, i.e., built from composing blocks that are in turn built from smaller blocks. Most existing approaches to verify properties flatten these hierarchical models before the verification process, losing the hierarchical structure. We propose an approach to verify hierarchical models using containers as actions; more concretely, containers interacting with their neighbours. We present a dynamic modal logic tailored for hierarchical connectors, using Reo and Petri Nets to illustrate our approach. We realise our approach via a prototype implementation available online to verify hierarchical Reo connectors, encoding connectors and formulas into mCRL2 specifications and formulas. © 2019, IFIP International Federation for Information Processing.

Supervised
thesis

2018

Contracts on-demand

Author
Leandro Rafael Moreira Gomes

Institution
UM

2016

Contracts on-demand

Author
Leandro Rafael Moreira Gomes

Institution
UM

2015

Validação do IEC 61131-3 Programmable Logical Controllers em KeyMaera

Author
Yoan David Ribeiro

Institution
UM