Abstract
Model checking is a new techology developed to ensure the correctness of concurrent systems. In this paper we consider one of the algorithms included in this techology, an algorithm for constructing Büchi automaton from a given LTL formula. This algorithm uses an alternating automaton as an intermediate model while translating the LTL formula to a generalized Büchi automaton. We represent data structures and data manipulations with BDD to increase algorithm effectiveness. The algorithm is compared on time and resulting Büchi automaton size with well known LTL to Büchi realizations (SPIN, LTL2BA), and it shows its effectiveness for wide class of LTL formulas. © 2011 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Shoshmina, I. V., & Belyaev, A. B. (2011). Symbolic algorithm for generation Büchi automata from LTL formulas. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6873 LNCS, pp. 98–109). https://doi.org/10.1007/978-3-642-23178-0_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
