Displaying 741 – 760 of 2186

Showing per page

Formally certified floating-point filters for homogeneous geometric predicates

Guillaume Melquiond, Sylvain Pion (2007)

RAIRO - Theoretical Informatics and Applications

Floating-point arithmetic provides a fast but inexact way of computing geometric predicates. In order for these predicates to be exact, it is important to rule out all the numerical situations where floating-point computations could lead to wrong results. Taking into account all the potential problems is a tedious work to do by hand. We study in this paper a floating-point implementation of a filter for the orientation-2 predicate, and how a formal and partially automatized verification of this...

Formulation of Cell Petri Nets

Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama (2013)

Formalized Mathematics

Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended...

Free group languages : rational versus recognizable

Pedro V. Silva (2004)

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

We provide alternative proofs and algorithms for results proved by Sénizergues on rational and recognizable free group languages. We consider two different approaches to the basic problem of deciding recognizability for rational free group languages following two fully independent paths: the symmetrification method (using techniques inspired by the study of inverse automata and inverse monoids) and the right stabilizer method (a general approach generalizable to other classes of groups). Several...

Free group languages: Rational versus recognizable

Pedro V. Silva (2010)

RAIRO - Theoretical Informatics and Applications

We provide alternative proofs and algorithms for results proved by Sénizergues on rational and recognizable free group languages. We consider two different approaches to the basic problem of deciding recognizability for rational free group languages following two fully independent paths: the symmetrification method (using techniques inspired by the study of inverse automata and inverse monoids) and the right stabilizer method (a general approach generalizable to other classes of groups). Several...

Free Term Algebras

Grzegorz Bancerek (2012)

Formalized Mathematics

We interoduce a new characterization of algebras of normal forms of term rewriting systems [35] as algerbras of term free in itself (any function from free generators into the algebra generates endomorphism of the algebra). Introduced algebras are free in classes of algebras satisfying some sets of equalities. Their universes are subsets of all terms and the denotations of operation symbols are partially identical with the operations of construction of terms. These algebras are compiler algebras...

From Bi-ideals to Periodicity

Jānis Buls, Aivars Lorencs (2008)

RAIRO - Theoretical Informatics and Applications

The necessary and sufficient conditions are extracted for periodicity of bi-ideals. They cover infinitely and finitely generated bi-ideals.

From indexed grammars to generating functions

Jared Adams, Eric Freden, Marni Mishna (2013)

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

We extend the DSV method of computing the growth series of an unambiguous context-free language to the larger class of indexed languages. We illustrate the technique with numerous examples.

FSM encoding for BDD representations

Wilsin Gosti, Tiziano Villa, Alex Saldanha, Alberto Sangiovanni-Vincentelli (2007)

International Journal of Applied Mathematics and Computer Science

We address the problem of encoding the state variables of a finite state machine such that the BDD representing the next state function and the output function has the minimum number of nodes. We present an exact algorithm to solve this problem when only the present state variables are encoded. We provide results on MCNC benchmark circuits.

FSP and FLTL framework for specification and verification of middle-agents

Amelia Bădică, Costin Bădică (2011)

International Journal of Applied Mathematics and Computer Science

Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers....

Full approximability of a class of problems over power sets.

Giorgio Ausiello, Alberto Marchetti-Spaccamela, Marco Protasi (1981)

Qüestiió

In this paper results concerning structural and approximability properties of the subclass of NP-Complete Optimization Problems, defined over a lattice are considered. First, various approaches to the concept of Fully Polynomial Approximation Scheme are presented with application to several known problems in the class of NP-Complete Optimization Problems.Secondly, a characterization of full Approximability for the class of Max Subset Problems is introduced.

Function operators spanning the arithmetical and the polynomial hierarchy

Armin Hemmerling (2010)

RAIRO - Theoretical Informatics and Applications

A modified version of the classical µ-operator as well as the first value operator and the operator of inverting unary functions, applied in combination with the composition of functions and starting from the primitive recursive functions, generate all arithmetically representable functions. Moreover, the nesting levels of these operators are closely related to the stratification of the arithmetical hierarchy. The same is shown for some further function operators known from computability and complexity theory....

Currently displaying 741 – 760 of 2186