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 Leandro Rafael Gomes

2017

On Kleene Algebras for Weighted Computation

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

Publicação
FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2017

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 actions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in a not necessary bivalent truth space, namely graded Kleene algebra with tests (GKAT) and Heyting Kleene algebra with tests (HKAT). On these contexts, in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [10], we discuss the encoding of a graded PHL in HKAT and of its while-free fragment in GKAT.

2019

Generalising KAT to Verify Weighted Computations

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

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

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

Publicação
Fundamentals of Software Engineering - 8th International Conference, FSEN 2019, Tehran, Iran, May 1-3, 2019, Revised Selected Papers

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

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

Publicação
Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings

Abstract
Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter. © 2019, Springer Nature Switzerland AG.

2020

Introducing Synchrony in Fuzzy Automata

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

Publicação
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Abstract
This paper introduces a sort of automata and associated languages, often arising in modelling natural phenomena, in which both vagueness and simultaneity are taken as first class citizens. This requires a fuzzy semantics assigned to transitions and a precise notion of a synchronous product to enforce the simultaneous occurrence of actions. The expected relationships between automata and languages are revisited in this setting; in particular it is shown that any subset of a fuzzy synchronous language with the suitable signature forms a synchronous Kleene algebra.

2020

On the Construction of Multi-valued Concurrent Dynamic Logics

Autores
Gomes, L;

Publicação
DYNAMIC LOGIC: NEW TRENDS AND APPLICATIONS, DALI 2019

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 (GCDL(A)), parametric on an action lattice A 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.

  • 1
  • 2