skip to main content
10.1145/2429069.2429079acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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 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
  • 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
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]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. buchi automata
  2. minimization
  3. simulation

Qualifiers

  • Research-article

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

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
  • (2019)Coinductive Algorithms for Büchi AutomataDevelopments in Language Theory10.1007/978-3-030-24886-4_15(206-220)Online publication date: 10-Jul-2019
  • (2018)Parity game reductionsActa Informatica10.1007/s00236-017-0301-x55:5(401-444)Online publication date: 1-Aug-2018
  • (2017)Forward Bisimulations for Nondeterministic Symbolic Finite AutomataProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_30(518-534)Online publication date: 22-Apr-2017
  • (2017)Minimization of Visibly Pushdown Automata Using Partial Max-SATProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_27(461-478)Online publication date: 22-Apr-2017
  • (2016)Reducing Nondeterministic Tree Automata by Adding TransitionsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.233.4233(33-51)Online publication date: 13-Dec-2016
  • (2016)Multi-Buffer Simulations for Trace Language InclusionElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.226.15226(213-227)Online publication date: 13-Sep-2016
  • (2016)Two-Buffer Simulation GamesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.220.3220(27-38)Online publication date: 31-Jul-2016
  • (2016)Compositional model checking of concurrent systems, with Petri netsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.204.3204(19-30)Online publication date: 2-Mar-2016
  • (2016)Organising LTL monitors over distributed systems with a global clockFormal Methods in System Design10.1007/s10703-016-0251-x49:1-2(109-158)Online publication date: 1-Oct-2016
  • (2016)Reduction of Nondeterministic Tree AutomataProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_46(717-735)Online publication date: 2-Apr-2016
  • 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