skip to main content
research-article

Advanced automata minimization

Published: 23 January 2013 Publication History

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.

References

[1]
RABIT tool: www.languageinclusion.org/doku.php?id=tools.
[2]
L. Clemente and R. Mayr. Advanced Automata Minimization. Tech. Rep. EDI-INF-RR-1414, U. of Edinburgh (2012), arXiv:1210.6624 http://www.inf.ed.ac.uk/publications/report/1414.html.
[3]
P. Abdulla, Y.-F. Chen, L. Clemente, L. Holik, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation Subsumption in Ramsey-Based Buchi Automata Universality and Inclusion Testing. In T. Touili, B. Cook, and P. Jackson, editors, Computer Aided Verification, volume 6174 of LNCS, pages 132--147, 2010. ISBN 978-3-642-14294-9. 14. URL http://dx.doi.org/10.1007/978-3-642-14295-6 14.
[4]
P. Abdulla, Y.-F. Chen, L. Clemente, L. Holik, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based Buchi Automata Inclusion Testing. In J.-P. Katoen and B. Konig, editors, International Conference on Concurrency Theory, volume 6901 of LNCS, pages 187--202, Sept. 2011.
[5]
P. A. Abdulla, Y.-F. Chen, L. Hol1k, and T. Vojnar. Mediating for reduction (on minimizing alternating Buchi automata). In FSTTCS, volume 4 of LIPIcs, pages 1--12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2009.
[6]
P. A. Abdulla, Y.-F. Chen, L. Holik, R. Mayr, and T. Vojnar. When Simulation Meets Antichains. In Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of LNCS, 2010. URL http://hal.inria.fr/inria-00460294/en/.
[7]
D. Bustan and O. Grumberg. Simulation-based minimization. ACM Trans. Comput. Logic, 4:181--206, April 2003. ISSN 1529-3785. URL http://doi.acm.org/10.1145/635499.635502.
[8]
L. Clemente. Buchi Automata Can Have Smaller Quotients. In L. Aceto, M. Henzinger, and J. Sgall, editors, ICALP, volume 6756 of LNCS, pages 258--270. 2011. ISBN 978-3-642-22011-1. 20. URL http://arxiv.org/pdf/1102.3285.
[9]
L. Clemente. Generalized Simulation Relations with Applications in Automata Theory. PhD thesis, University of Edinburgh, 2012.
[10]
D. L. Dill, A. J. Hu, and H. Wont-Toi. Checking for Language Inclusion Using Simulation Preorders. In Computer Aided Verification, volume 575 of LNCS. Springer-Verlag, 1991. 25. URL http://dx.doi.org/10.1007/3-540-55179-4 25.
[11]
L. Doyen and J.-F. Raskin. Antichains Algorithms for Finite Automata. In Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of LNCS, pages 2--22. Springer-Verlag, 2010.
[12]
K. Etessami. A Hierarchy of Polynomial-Time Computable Simulations for Automata. In International Conference on Concurrency Theory, volume 2421 of LNCS, pages 131--144. Springer-Verlag, 2002. 10. URL http://dx.doi.org/10.1007/3-540-45694-5 10.
[13]
K. Etessami and G. Holzmann. Optimizing Buchi Automata. In International Conference on Concurrency Theory, volume 1877 of LNCS, pages 153--168. Springer-Verlag, 2000.
[14]
K. Etessami, T. Wilke, and R. A. Schuller. Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata. SIAM J. Comput., 34(5):1159--1175, 2005. URL http://epubs.siam.org/sam-bin/dbq/article/42067.
[15]
S. Fogarty and M. Vardi. Complementation and Size-Change Termination. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of LNCS, pages 16--30. 2009. 2. URL http://dx.doi.org/10.1007/978-3-642-00768-2 2.
[16]
S. Fogarty and M. Y. Vardi. Efficient Buchi Universality Checking. In Tools and Algorithms for the Construction and Analysis of Systems, pages 205--220, 2010.
[17]
S. Fogarty, O. Kupferman, M. Y. Vardi, and T. Wilke. Unifying Buchi Complementation Constructions. In M. Bezem, editor, Computer Science Logic, volume 12 of LIPIcs, pages 248--263. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2011.
[18]
P. Gastin and D. Oddoux. Fast LTL to Buchi automata translation. In CAV, volume 2102 of LNCS, pages 53--65. Springer, 2001.
[19]
S. Gurumurthy, R. Bloem, and F. Somenzi. Fair simulation minimization. In CAV, volume 2404 of LNCS, pages 610--624. Springer, 2002.
[20]
M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In Foundations of Computer Science, FOCS '95, Washington, DC, USA, 1995. IEEE Computer Society. ISBN 0-8186-7183-1. URL http://portal.acm.org/citation.cfm?id=796255.
[21]
T. A. Henzinger, O. Kupferman, and S. K. Rajamani. Fair Simulation. Information and Computation, 173: 64--81, 2002. URL http://dx.doi.org/10.1006/inco.2001.3085.
[22]
G. Holzmann. The SPIN Model Checker. Addison Wesley, 2004.
[23]
T. Jiang and B. Ravikumar. Minimal NFA Problems are Hard. In J. Albert, B. Monien, and M. Artalejo, editors, ICALP, volume 510 of LNCS, pages 629--640. 1991. 169.
[24]
S. Juvekar and N. Piterman. Minimizing Generalized Buchi Automata. In Computer Aided Verification, volume 4414 of LNCS, pages 45--58. Springer-Verlag, 2006. 7. URL http://dx.doi.org/10.1007/11817963 7.
[25]
O. Kupferman and M. Vardi. Verification of Fair Transition Systems. In Computer Aided Verification, volume 1102 of LNCS, pages 372--382. Springer-Verlag, 1996. URL http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.9654.
[26]
C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. POPL '01, pages 81--92, 2001.
[27]
J. Leroux and G. Point. TaPAS: The Talence Presburger Arithmetic Suite. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of LNCS. Springer, 2009.
[28]
I. Niven. Mathematics of Choice. The Mathematical Association of America, 1965.
[29]
N. Piterman. From nondeterministic Buchi and Streett automata to deterministic parity automata. In LICS, pages 255--264. IEEE, 2006.
[30]
R. Sebastiani and S. Tonetta. More deterministic vs. smaller Buchi automata for efficient LTL model checking. In Correct Hardware Design and Verification Methods, volume 2860 of LNCS, 2003.
[31]
A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Buchi automata with applications to temporal logic. Theor. Comput. Sci., 49:217--237, Jan. 1987. ISSN 0304-3975. 3975(87)90008-9. URL http://dx.doi.org/10.1016/0304-3975(87)90008-9.
[32]
F. Somenzi and R. Bloem. Efficient Buchi Automata from LTL Formulae. In Computer Aided Verification, volume 1855 of LNCS, pages 248--263. Springer-Verlag, 2000. 21. URL http://dx.doi.org/10.1007/10722167_21.
[33]
D. Tabakov and M. Vardi. Model Checking Buchi Specifications. In LATA, volume Report 35/07. Research Group on Mathematical Linguistics, Universitat Rovira i Virgili, Tarragona, 2007.
[34]
Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai,W.-C. Chan, and C.-J. Luo. GOAL extended: Towards a research tool for omega automata and temporal logic. In C. Ramakrishnan and J. Rehof, editors, Tools and Algo- rithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 346--350. 2008. ISBN 978-3-540-78799-0. URL http://dx.doi.org/10.1007/978-3-540-78800-3 26.
[35]
Y.-K. Tsay, M.-H. Tsai, J.-S. Chang, and Y.-W. Chang. Buchi store: An open repository of Buchi automata. In P. Abdulla and K. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of LNCS, pages 262--266. 2011. ISBN 978-3-642-19834-2. URL http://dx.doi.org/10.1007/978-3-642-19835-9 23.10.1007/978-3-642-19835-9 23.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. buchi automata
  2. minimization
  3. simulation

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)33
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Symbolic Automata: Omega-Regularity Modulo TheoriesProceedings of the ACM on Programming Languages10.1145/37048389:POPL(33-66)Online publication date: 9-Jan-2025
  • (2023)On the power of finite ambiguity in Büchi complementationInformation and Computation10.1016/j.ic.2023.105032292(105032)Online publication date: Jun-2023
  • (2023)Incremental Dead State Detection in Logarithmic TimeComputer Aided Verification10.1007/978-3-031-37703-7_12(241-264)Online publication date: 17-Jul-2023
  • (2022)Genetic and Chemical Diversity of Commercial Japanese ValerianChemical and Pharmaceutical Bulletin10.1248/cpb.c22-0010570:12(840-847)Online publication date: 1-Dec-2022
  • (2022)Simulation Relations and Applications in Formal MethodsPrinciples of Systems Design10.1007/978-3-031-22337-2_13(272-291)Online publication date: 29-Dec-2022
  • (2022)Complementing Büchi Automata with RankerComputer Aided Verification10.1007/978-3-031-13188-2_10(188-201)Online publication date: 6-Aug-2022
  • (2022)Sky Is Not the LimitTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-99527-0_7(118-136)Online publication date: 30-Mar-2022
  • (2020)Language Inclusion for Finite Prime Event StructuresVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_15(314-336)Online publication date: 2020
  • (2019)Approximate reduction of finite automata for high-speed network intrusion detectionInternational Journal on Software Tools for Technology Transfer10.1007/s10009-019-00520-8Online publication date: 24-May-2019
  • (2019)Simulations in Rank-Based Büchi Automata ComplementationProgramming Languages and Systems10.1007/978-3-030-34175-6_23(447-467)Online publication date: 18-Nov-2019
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media