Advanced automata minimization

DOI10.1145/2429069.2429079MaRDI QIDQ2931784zbMATH OpenOpenAlexFDO

Authors Lorenzo Clemente, Richard M. Mayr

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.6624

zbMATH Keywords

Büchi automataminimizationsimulation

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45) Nonnumerical algorithms (68W05) Approximation algorithms (68W25)

Abstract: We present an efficient algorithm to reduce the size of nondeterministic Buchi word automata, while retaining their language. Additionally, we describe methods to solve PSPACE-complete automata problems like universality, equivalence and inclusion for much larger instances (1-3 orders of magnitude) than before. This can be used to scale up applications of automata in formal verification tools and decision procedures for logical theories. The algorithm is based on new transition pruning techniques. These use criteria based on combinations of backward and forward trace inclusions. Since these relations are themselves PSPACE-complete, we describe methods to compute good approximations of them in polynomial time. Extensive experiments show that the average-case complexity of our algorithm scales quadratically. The size reduction of the automata depends very much on the class of instances, but our algorithm consistently outperforms all previous techniques by a wide margin. We tested our algorithm on Buchi automata derived from LTL-formulae, many classes of random automata and automata derived from mutual exclusion protocols, and compared its performance to the well-known automata tool GOAL.

Recommendations

• Efficient reduction of nondeterministic automata with application to language inclusion testing
• Minimising deterministic Büchi automata precisely using SAT solving
• Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
• On complementing nondeterministic Büchi automata
• Minimizing Generalized Büchi Automata

Cited in

(23)

• Parity game reductions
• Multi-buffer simulations: decidability and complexity
• Büchi automata optimisations formalised in Isabelle/HOL
• New optimizations and heuristics for determinization of Büchi automata
• Minimization of visibly pushdown automata using partial Max-SAT
• Forward bisimulations for nondeterministic symbolic finite automata
• Automata with Extremal Minimality Conditions
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• Minimising deterministic Büchi automata precisely using SAT solving
• Learn with SAT to minimize Büchi automata
• Topological characterisation of multi-buffer simulation
• scientific article; zbMATH DE number 7438162 (Why is no real title available?)
• Multi-buffer simulations for trace language inclusion
• Coinductive algorithms for Büchi automata
• Improved Algorithms for the Automata-Based Approach to Model-Checking
• On the power of finite ambiguity in Büchi complementation
• Simulation relations and applications in formal methods
• Complementing Büchi Automata with Ranker
• Incremental dead state detection in logarithmic time
• Sky is not the limit. Tighter rank bounds for elevator automata in Büchi automata complementation
• Simulations in rank-based Büchi automata complementation
• Organising LTL monitors over distributed systems with a global clock
• Relations between equation automata and follow automata

This page was built for publication: Advanced automata minimization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931784)