PV1 ⊧ FOADA: First Order Alternating Data Automatachecks whether the given automaton is empty

Application domain/field

• Automata theory
• Emptiness checking

Type of tool

Model checker/emptiness checker

Expected input

First Order Alternating Data Automata

Format:

Own format (.foada file)

Expected output

Yes or no (whether the First Order Alternating Data Automata is empty)

Internals

Tool for emptiness checking for First Order Alternating Data Automata Uses Z3, JavaSMT