Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Mike Gordon. HOL: A proof generating system for higher-order logic. InVLSI specification, Verification and Synthesis G. Birtwistle and P.A. Subrahmanyam (eds.), Kluwer Academic Publisers, 1988.
Robert S. Boyer and J. Strother Moore.A Computational Logic. Academic Press, 1979.
J.R. Büchi. On a decision method in rescricted second-order arithmetic. InProceedings International Congress on Logic, Methodology and Philosophy of Science, 1960, Stanford University Press, 1962, 1–12.
M.O. Rabin. Decidability of second-order theories and automata on infinite trees.Transactions American Mathematical Society, 141:1–35, 1969.
D.E. Muller. Infinite sequences and finite machines. InSwitching Circuit Theory and Logical Design: Proceedings Fourth Annual Symposium, New York, 1963. Institute of Electrical and Electronic Engineers, 3–16
Paul Loewenstein. The formal verification of state-machines using higher-order logic. InIEEE International Conference on Computer Design, 1989.
Paul Loewenstein and David Dill. Formal verification of cache systems using refinement relations. InIEEE International Conference on Computer Design, 228–233, 1990.
Paul Loewenstein and David L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic.Formal Methods in Systems Design, 1:355–383, 1992.
R. Milner. An algebraic definition of simulation between programs. InProceedings 2nd International Joint Conference on Artificial Intelligence, 1971.
Martín Abadi and Leslie Lamport. The existence of refinement mappings.Theoretical Computer Science, 82(2):253–284, May 1991.
Nils Klarlund and Fred B. Schneider. Verifying safety properties using non-deterministic infinitestate automata. Technical Report TR 89-1037, Cornell University Computer Science Department, 1989.
Mike Gordon. HOL: A machine oriented formulation of higher-order logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985.
Mike Fourman. Avoiding use of the axiom of choice. Private communication, 1990.
Bowern Alpern and Fred B. Schneider. Recognizing safety and liveness. Technical Report TR 86-727, Department of Computer Science, Cornel University, 1986.
Fred B. Schneider. Decomposing properties into safety and liveness using predicate logic. Technical Report TR 87-874, Department of Computer Science, Cornell University, 1987.
Dénes König. Sur les correspondances multivoques des ensembles.Fundamenta Mathematicae, 8:114–134, 1926.
T.F. Melham. Inductive relation definitions in HOL. InInternational Workshop on the HOL Theorem Proving System and its Applications. IEEE Computer Society Press, 1991.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Loewenstein, P. A formal theory of simulations between infinite automata. Form Method Syst Des 3, 117–149 (1993). https://doi.org/10.1007/BF01383986
Issue Date:
DOI: https://doi.org/10.1007/BF01383986