Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Maude Object-Oriented Action Tool

MAIDL, André Murbach; CARVILHE, Claudio; MUSICANTE, Martin A. Maude Object-Oriented Action Tool. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2008.

Tilings induced by a class of cubic Rauzy fractals

We study aperiodic and periodic tilings induced by the Rauzy fractal and its subtiles associated with beta-substitutions related to the polynomial x3-ax2-bx-1 for a≥b≥1. In particular, we compute the corresponding boundary graphs, describing the adjacencies in the tilings. These graphs are a valuable tool for more advanced studies of the topological properties of the Rauzy fractals. As an example, we show that the Rauzy fractals are not homeomorphic to a closed disc as soon as a≤2b-4. The methods presented in this paper may be used to obtain similar results for other classes of substitutions.© 2012 Elsevier B.V. All rights reserved.

A class of cubic Rauzy fractals

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Two ways to common knowledge

It is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems.