A formal theory of simulations between infinite automata

DOI10.1007/BF01383986zbMath0785.68081OpenAlexW3021628808MaRDI QIDQ1309253

Paul N. Loewenstein

Publication date: 20 December 1993

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01383986

zbMATH Keywords

HOL theorem provermodel of computationautomata-theoretic reasoninghigher-order logic theorem prover

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• HOL

Cites Work

• Unnamed Item
• Verification of a multiprocessor cache protocol using simulation relations and higher-order logic
• The existence of refinement mappings
• Recognizing safety and liveness
• Decidability of Second-Order Theories and Automata on Infinite Trees