Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(7)
Context Free Language
Finite Automata
Finite State Machine
Formal Language
Coq Proof Assistant
Machine Model
Real Time
Subscribe
Academic
Publications
Simulating Finite Eilenberg Machines with a Reactive Engine
Simulating Finite Eilenberg Machines with a Reactive Engine,10.1016/j.entcs.2011.02.019,Electronic Notes in Theoretical Computer Science,Benoît Razet
Edit
Simulating Finite Eilenberg Machines with a Reactive Engine
(
Citations: 2
)
BibTex

RIS

RefWorks
Download
Benoît Razet
Eilenberg machines have been introduced in 1974 in the field of
formal language
theory. They are
finite automata
for which the alphabet is interpreted by mathematical relations over an abstract set. They generalize many finite state machines. We consider in the present work the subclass of finite Eilenberg machines for which we provide an executable complete simulator. This program is specified using the Coq proof assistant. The correctness of the algorithm is also proved formally and mechanically verified using Coq. Using its extraction mechanism, the
Coq proof assistant
allows to translate the specification into an executable OCaml program. The algorithm and specification are inspired from the reactive engine of Gérard Huet. The finite Eilenberg machines model includes deterministic and nondeterministic automata (DFA and NFA) but also realtime transducers. As an example, we present a pushdown automaton (PDA) recognizing ambiguous λterms is shown to be a finite Eilenberg machine. Then the reactive engine simulating the pushdown automaton provides a complete recognizer for this particular contextfree language.
Journal:
Electronic Notes in Theoretical Computer Science  ENTCS
, vol. 229, no. 5, pp. 119134, 2011
DOI:
10.1016/j.entcs.2011.02.019
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.sciencedirect.com
)
Citation Context
(2)
...Ce d´eveloppement est pr´esent´e en [
8
]...
Gerard Huet
.
Automates, machines, moteurs reactifs
...Benoˆõt Razet showed in [
17
] a formal proof of correctness and completeness of the simulation of a finite machine by the above reactive engine...
Unknown.
Computing with Relational Machines
Sort by:
Citations
(2)
Automates, machines, moteurs reactifs
Gerard Huet
Published in 2008.
Computing with Relational Machines
Unknown
Published in 2008.