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
Sobre
Download foto HD

Sobre

Short Bio (EN):

Alexandre Madeira é um membro do HASLab - INESC TEC que está  a desenvolver o projecto de pós-doutoramento  "dynamic logics for every season" suportado por uma bolsa individual BPD FCT (SFRH /BPD/103004/2014). O projecto é acolhido no HASLab - INESC TEC e no centro CIDMA sob orientação científica de Luís S. Barbosa (Dep. Informática, Univ. Minho) e Manuel A. Martins (Dep. Matemática da Univ. Aveiro).   O Alexandre é ainda o Investigador Responsável do projecto R&D da FCT "DaLí: Dynamic logics for cyber-physical systems: towards contract based design".   Interesses de Investigação:   - Fundamentos Matemáticos para a Engenharia de Software   - Métodos Lógicos e Algébricos para o Sesenvolvimento de Software   - Geração Paramétrica de Lógicas Modais/Hibridas/Dinamicas   - Algebra de Processos    

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Alexandre Castro Madeira
  • Cluster

    Informática
  • Desde

    01 novembro 2011
002
Publicações

2020

Introducing Synchrony in Fuzzy Automata

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

Publicação
Electronic Notes in Theoretical Computer Science

Abstract

2020

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

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

Publicação
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

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

Publicação
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

Autores
Benevides, MRF; Madeira, A;

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract

2019

Taming Hierarchical Connectors

Autores
Proença, J; Madeira, A;

Publicação
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.

Teses
supervisionadas

2018

Contracts on-demand

Autor
Leandro Rafael Moreira Gomes

Instituição
UM

2016

Contracts on-demand

Autor
Leandro Rafael Moreira Gomes

Instituição
UM

2015

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

Autor
Yoan David Ribeiro

Instituição
UM