publication . Article . Book . Conference object . Part of book or chapter of book . 2006

symbolic implementation of alternating automata

Bloem, R.; Cimatti, A.; Ingo Pill; Roveri, M.; Semprini, S.;
Restricted
  • Published: 01 Jan 2006 Journal: International Journal of Foundations of Computer Science, volume 18, pages 727-743 (issn: 0129-0541, eissn: 1793-6373, Copyright policy)
  • Publisher: World Scientific Pub Co Pte Lt
Abstract
<jats:p> This paper addresses the challenges of symbolic model checking and language emptiness checking where the specification is given as an alternating Büchi automaton. </jats:p><jats:p> We introduce a novel version of Miyano and Hayashi's construction that allows us to directly convert an alternating automaton to a polynomially-sized symbolic structure. We thus avoid building an exponentially-sized explicit representation of the corresponding nondeterministic automaton. </jats:p><jats:p> For one-weak automata, Gastin and Oddoux' construction produces smaller automata than Miyano and Hayashi's construction. We present a (symbolic) hybrid approach that combine...
Subjects
free text keywords: Computer Science (miscellaneous), Deterministic automaton, Timed automaton, Discrete mathematics, Automaton, Nondeterministic finite automaton, Theoretical computer science, Nondeterministic algorithm, Symbolic trajectory evaluation, Mathematics, Büchi automaton, Model checking, Continuous spatial automaton, Quantum finite automata, Automata theory, Mobile automaton, ω-automaton, Algorithm
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue