Complementable Normal Form of Parametrized Automata
摘要
Parametrized automata (PA) are an extension of two existing kinds of automata, symbolic automata and variable automata. In PA, transitions are labeled with formulas that may contain variables. PA are a powerful tool for modeling systems over infinite alphabets, but complementation of PA has been proven to be challenging: not every PA has a complement, and complementation in general may be non-computable. This paper presents a new notion of normal form for PA, called complementable normal form (CFPA). CFPA is sufficiently expressive to completely characterize the class of PA that can be complemented. We show that all Boolean operations (including complementation) can be computed efficiently on CFPA, and key problems such as the universality and non-emptiness problem are decidable for CFPA. Based on CFPA, we propose a new method for complementing PA.