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

I am a PhD student at MAP-i doctoral program, held by Universities of Minho, Aveiro and Porto and researcher at HASLab, Univeristy of Minho.

I did both my bachelor and master degrees in Mathematics, in University of Aveiro.

My current research topic, and my goal for the PhD, lies in building a systematic process of generating dynamic logic, by developing a general theory of such logics. This approach favouring a contract-based design method for software speciï¬�cation, and the development of an algebraic structure to model the space of programs and the corresponding domains of behaviours. My goal for the PhD is to provide also a generic theory to support the logics generated by this process, as well as to discuss how to capture more complex computing paradigms, such as quantum algorithms and hybrid systems.

Interest
Topics
Details

Details

  • Name

    Leandro Rafael Gomes
  • Since

    15th April 2016
  • Nationality

    Portugal
  • Contacts

    +351253604440
    leandro.r.gomes@inesctec.pt
002
Publications

2020

Introducing Synchrony in Fuzzy Automata

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

Publication
Electronic Notes in Theoretical Computer Science

Abstract

2020

On the Construction of Multi-valued Concurrent Dynamic Logics

Authors
Gomes, L;

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

Abstract
Dynamic logic is a powerful framework for reasoning about imperative programs. An extension with a concurrent operator, called concurrent propositional dynamic logic (CPDL) [20], was introduced to formalise programs running in parallel. In a different direction, other authors proposed a systematic method for generating multi-valued propositional dynamic logics to reason about weighted programs [15]. This paper presents the first step of combining these two frameworks to introduce uncertainty in concurrent computations. In the proposed framework, a weight is assigned to each branch of the parallel execution, resulting in a (possible) asymmetric parallelism, inherent to the fuzzy programming paradigm [2, 23]. By adopting such an approach, a family of logics is obtained, called multi-valued concurrent propositional dynamic logics ), parametric on an action lattice specifying a notion of “weight” assigned to program execution. Additionally, the validity of some axioms of CPDL is discussed in the new family of generated logics. © 2020, Springer Nature Switzerland AG.

2019

Generalising KAT to Verify Weighted Computations

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

Publication
SCIENTIFIC ANNALS OF COMPUTER SCIENCE

Abstract
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M (n, A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.

2019

Logics for Petri Nets with Propagating Failures

Authors
Gomes, L; Madeira, A; Benevides, MRF;

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

Abstract
Petri nets play a central role in the formal modelling of a wide range of complex systems and scenarios. Their ability to handle with both concurrency and resource awareness justifies their spread in the current formal development practices. On the logic side, Dynamic Logics are widely accepted as the de facto formalisms to reason about computational systems. However, as usual, the application to new situations raises new challenges and issues. The ubiquity of failures in the execution of current systems, interpreted in these models as triggered events that are not followed by the corresponding transition, entails not only the adjustment of these structures to deal with this reality, but also the introduction of new logics adequate to this emerging phenomenon. This paper contributes to this challenge by exploring a combination of two previous works of the authors, namely the Propositional Dynamic Logic for Petri Nets [1] and a parametric construction of multi-valued dynamic logics presented in [13]. This exercise results in a new family of Dynamic Logics for Petri Nets suitable to deal with firing failures. © 2019, IFIP International Federation for Information Processing.

2019

On the Generation of Equational Dynamic Logics for Weighted Imperative Programs

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

Publication
Formal Methods and Software Engineering - Lecture Notes in Computer Science

Abstract