A formal theory of simulations between infinite automata
| Autor: | Paul N. Loewenstein |
|---|---|
| Rok vydání: | 1993 |
| Předmět: |
Theoretical computer science
Computer science Theory Nonlinear Sciences::Cellular Automata and Lattice Gases Theoretical Computer Science Automaton Automated theorem proving Range (mathematics) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Hardware and Architecture Formal verification Computer Science::Formal Languages and Automata Theory Software Abstraction (linguistics) |
| Zdroj: | Formal Methods in System Design. 3:117-149 |
| ISSN: | 1572-8102 0925-9856 |
| DOI: | 10.1007/bf01383986 |
| Popis: | Automata are suitable for modeling a wide range of sequential and concurrent hardware. They can be used at many levels of abstraction, from top-level specifications to register transfer descriptions suitable for input to synthesis tools. This paper covers approaches for relating one automaton with another using simulations and transformations on automata. The entire theory is mechanically derived in, and intended for use in a higher-order logic theorem prover. Because automaton-based models can be used at multiple abstraction levels, much of the formal verification of sequential and concurrent designs can be performed by composing and relating automata. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink