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
Publications

Publications by Alexandre Castro Madeira

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 - 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

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

Publication
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.

2018

Verification for Everyone? An Overview of Dynamic Logic

Authors
Madeira, A;

Publication
Molecular Logic and Computational Synthetic Biology - First International Symposium, MLCSB 2018, Santiago, Chile, December 17-18, 2018, Revised Selected Papers

Abstract
This note, reporting the homonym keynote presented in the International Symposium on Molecular Logic and Computational Synthetic Biology 2018, traces an informal roadmap on Dynamic Logic (DL) field, focusing on its versatility and resilience to be adjusted and adopted in a wide class of application domains and computational paradigms. The exposition argues the room for developments on tagging DL to the analysis of synthetic biologic domain. © 2019, Springer Nature Switzerland AG.

2020

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

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

Publication
DYNAMIC LOGIC: NEW TRENDS AND APPLICATIONS, DALI 2019

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 phi and [alpha]phi 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

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

  • 7
  • 12