Using Asynchronous Büchi Automata for Efficient Automatic Verification of Concurrent Systems

  • D. Peled
  • W. Penczek
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


An Asynchronous Büchi Automaton is a collection of concurrently executing automata, able to perform operations that are shared between one or more of their concurrent components. These automata can be used to specify properties of distributed protocols. In this paper, an efficient method for verifying that a protocol satisfies its Asynchronous Büchi Automaton specification is presented. In order to alleviate a potential state space explosion while verifying a protocol, a state reduction technique is used. The construction results in a reduced state space that contains at least one representative sequence for each equivalence class of infinite sequences. This guarantees that the full state space contains an accepting execution if and only if the reduced state space contains one. This method can also be used to check for the emptyness of an Asynchronous Büchi Automaton. Thus, it can be used to check the validity of specification languages that can be translated into such automata, such as Thiagarajan’s TrPTL.


Verification State-space explosion Asynchronous Büchi Automata Partial order reductions. 


  1. [1]
    A.V. Aho, J.E. Hoperoft and J.D.Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley Publishing Company, 1974.Google Scholar
  2. [2]
    J. R. Büchi, On a decision method in restricted second order arithmetic, in E. Nagel et al. (eds.), Proceeding of the International Congress on Logic, Methodology and Philosophy of Science, Stanford, CA, Stanford University Press, 1960, 1–11.Google Scholar
  3. [3]
    E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal-logic specifications, ACM Transactions on Programming Languages and Systems, 8, 1986, 244–263.CrossRefzbMATHGoogle Scholar
  4. [4]
    R. Gerth, R. Kuiper, D. Peled, and W. Penczek, A Partial Order Approach to Branching Time Model Checking, Proc. of ISTCS’95, 1995, 330–339, Tel Aviv, Israel.CrossRefGoogle Scholar
  5. [5]
    P. Gastin, A. Petit, Asynchronous Automata for Infinite Traces, in W. Kuich (ed.), , 1992, LNCS 623, Springer-Verlag, 583–594.Google Scholar
  6. [6]
    P. Godefroid, P. Wolper, A Partial Approach to Model Checking, Proc. of LICS, 1991, 406–415.Google Scholar
  7. [7]
    G. J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall Software Series, 1992.Google Scholar
  8. [8]
    G. J. Holzmann, D. Peled, An Improvement in Formal Verification, Proc. of FORTE, 1994, 177–191.Google Scholar
  9. [9]
    S. Katz, D. Peled, Interleaving Set Temporal Logic, Theoretical Computer Science, Vol. 75, Number 3, 21–43, also appeared in proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, Vancouver, Canada, August 1987Google Scholar
  10. [10]
    M. Z. Kwiatkowska, Event Fairness and Non-Interleaving Concurrency, Formal Aspects of Computing 1, 1989, 213–228.CrossRefzbMATHGoogle Scholar
  11. [11]
    O. Lichtenstein, A. Pnueli, Checking that finite-state concurrent programs satisfy their linear specification, Proc. of 11th ACM POPL, 1984, 97–107.Google Scholar
  12. [12]
    A. Mazurkiewicz, Trace Theory, Advances in Petri Nets 1986, LNCS 255, Springer, 1987, 279–324.Google Scholar
  13. [13]
    A. Muscholl, On the Complementation of Büchi Asynchronous Cellular Automata, Proc. of ICALP’94, 1994, Springer-Verlag, LNCS, 141–129.Google Scholar
  14. [14]
    D. Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proc. of 6th international conference on Computer Aided Verification, Stanford, CA, 1994, LNCS 818, 377–390.Google Scholar
  15. [15]
    D. Peled and W. Penczek, Using Asynchronous Büchi Automata for Efficient Automatic Verification of Concurrent Systems, to appear in the Participant’s Proceedings of PSTV’95.Google Scholar
  16. [16]
    W. Penczek, Temporal Logics on Trace Systems: On automated verification, International Journal of Foundations of Computer Science, Vol. 4 No. 1, 1993, 31–67.MathSciNetCrossRefzbMATHGoogle Scholar
  17. [17]
    A. Pnueli, The Temporal Logic of Programs, Theoretical Computer Science 13, 1977, 1–20.Google Scholar
  18. [18]
    P.S. Thiagarajan, A Trace Based Extension of Linear Time Temporal Logic, Proc. of 9th Symposium on Logic in Computer Science, Paris, 1994, IEEE Press, 438–447.Google Scholar
  19. [19]
    W. Thomas, Automata on Infinite Objects, in J. Van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B, Elsvier, 1990, 133–191.Google Scholar
  20. [20]
    P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, Proc. of 24th IEEE symposium on foundation of computer science, Tuscan, 1983, 185–194.Google Scholar
  21. [21]
    A. Valmari, A Stubborn attack on state explosion, in E.M. Clarke, R.P. Kurshan (eds.), Proc. of CAV’90, DIMACS, Vol 3, 1991, 25–42.Google Scholar
  22. [22]
    A. Valmari, On-the-fly verification with stubborn sets, LNCS 697, 1993, 397–408.Google Scholar
  23. [23]
    W. Zielonka, Notes on finite asynchronous automata, R.A.I.R.O.-Informatique Théorique et Applications, 21, 1987, 99–135.MathSciNetzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • D. Peled
    • 1
  • W. Penczek
    • 2
  1. 1.AT&T BellMurray HillUSA
  2. 2.Technical University of EindhovenEindhovenThe Netherlands

Personalised recommendations