Automata over finite or infinite words or binary decision diagrams (BDDs) are ubiquitous in modern computer science, providing robust foundations for applications in automated reasoning, verification, information processing, etc. Applications based on these models usually largely benefit when the handled automata or BDDs are small, reducing memory requirements and improving the runtime of their processing. Recently, compact representations of automata based on extensions of the basic models started appearing, often in an ad hoc manner relevant for particular applications, with many basic questions unanswered and their full potential unexplored. One goal of the project is to fill the gap by designing novel, practically relevant, concise kinds of automata and algorithms for their efficient manipulation, and applications based on these automata. The second is to reduce the size of manipulated BDDs by combining them with approximative reasoning. By achieving these goals, the project aims to push the applicability and scalability of automata- and BDD-based tools to a new level.

Keywords
formal languages;finite automata;automata over infinite words;omega-automata;Emerson-Lei automata;TELA;binary decision diagrams;BDD;partial BDD;approximation;complementation

26-22640S

English

Lengál Ondřej, doc. Ing., Ph.D. - principal person responsible

Department of Intelligent Systems
- responsible department (24.3.2025 - not assigned)
Department of Intelligent Systems
- co-beneficiary (24.3.2025 - 31.12.2028)
Faculty of Informatics MU
- beneficiary (24.3.2025 - 31.12.2028)

Responsibility: Lengál Ondřej, doc. Ing., Ph.D.