Page 1

Displaying 1 – 14 of 14

Showing per page

Object oriented institutions to specify symbolic computation systems

César Domínguez, Laureano Lambán, Julio Rubio (2007)

RAIRO - Theoretical Informatics and Applications

The specification of the data structures used in EAT, a software system for symbolic computation in algebraic topology, is based on an operation that defines a link among different specification frameworks like hidden algebras and coalgebras. In this paper, this operation is extended using the notion of institution, giving rise to three institution encodings. These morphisms define a commutative diagram which shows three possible views of the same construction, placing it in an equational algebraic...

On characteristic formulae for Event-Recording Automata

Omer Landry Nguena Timo, Pierre-Alain Reynier (2013)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that...

On Distributive Fixed-Point Expressions

Helmut Seidl, Damian Niwiński (2010)

RAIRO - Theoretical Informatics and Applications

For every fixed-point expression e of alternation-depth r, we construct a new fixed-point expression e' of alternation-depth 2 and size 𝒪 ( r · | e | ) . Expression e' is equivalent to e whenever operators are distributive and the underlying complete lattice has a co-continuous least upper bound. We alternation-depth but also w.r.t. the increase in size of the resulting expression.

On global induction mechanisms in a μ -calculus with explicit approximations

Christoph Sprenger, Mads Dam (2003)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

We investigate a Gentzen-style proof system for the first-order μ -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...

On global induction mechanisms in a μ-calculus with explicit approximations

Christoph Sprenger, Mads Dam (2010)

RAIRO - Theoretical Informatics and Applications

We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...

On the Decidability of the Equivalence Problem for Monadic Recursive Programs

Vladimir A. Zakharov (2010)

RAIRO - Theoretical Informatics and Applications

We present a uniform and easy-to-use technique for deciding the equivalence problem for deterministic monadic linear recursive programs. The key idea is to reduce this problem to the well-known group-theoretic problems by revealing an algebraic nature of program computations. We show that the equivalence problem for monadic linear recursive programs over finite and fixed alphabets of basic functions and logical conditions is decidable in polynomial time for the semantics based on the free monoids...

Currently displaying 1 – 14 of 14

Page 1