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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Complementable Normal Form of Parametrized Automata

  • Franziska Alber,
  • Philipp Rümmer

摘要

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.