publication . Conference object . 2005

Efficient LTL compilation for SAT-based model checking

R. Armoni; S. Egorov; R. Fraer; D. Korchemny; M.Y. Vardi;
Restricted
  • Published: 22 Dec 2005
  • Publisher: IEEE
Abstract
This work describes an algorithm of automata construction for LTL safety properties, suitable for bounded model checking. Existing automata construction methods are tailored to BDD-based symbolic model checking. The novelty of our approach is that we construct deterministic automata, unlike the standard approach, which constructs nondeterministic automata. We show that the proposed method has significant advantages for bounded model checking over traditional methods.
Subjects
arXiv: Computer Science::Formal Languages and Automata TheoryNonlinear Sciences::Cellular Automata and Lattice Gases
ACM Computing Classification System: TheoryofComputation_COMPUTATIONBYABSTRACTDEVICESTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Bounded function, Automaton, Model checking, Abstraction model checking, Automata construction, Theoretical computer science, Automata theory, Novelty, Symbolic trajectory evaluation, Computer science
Related Organizations
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue