Homomorphic Reduction of Coordination Analysis

  • R. P. Kurshan
Part of the The IMA Volumes in Mathematics and its Applications book series (IMA, volume 73)


Automata-theoretic verification is based upon the language containment test
$${\cal L}({P_0} \otimes {P_1} \otimes \ldots \otimes {P_k}) \subset {\cal L}(T)$$
where the Pi’s are automata which together model a system with its fairness constraints, ⊗ is a parallel composition for automata and T defines a specification. The complexity of that test typically grows exponentially with k. This growth, often called “state explosion”, has been a major impediment to computer-aided verification, and many heuristics which are successful in special cases, have been developed to combat it. We describe here a general reduction methodology which subsumes many of these heuristics. It is based upon two transformations: decomposition of T into “local” properties T1 ,…, Tn such that ) ∩L(Tj) ⊂ L(Tj), and localization of each test L(⊗Pi) ⊂ L(Tj) to a small (tractible) test.


Model Check Boolean Algebra Formal Verification Acceptance Condition Simple Decomposition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    H. R. Anderson and G. Winskel. Compositional Checking of Satisfaction. Formal Methods in Syst. Design 1, pages 323–354, (1992).CrossRefGoogle Scholar
  2. [2]
    J. R. Büchi. On a Decision Method in Restricted Second-Order Arithmetic. In Methodology and Philosophy of Science, Proceedings, 1960 Stanford Intern. Congr., pages 1–11, Stanford, Calif., 1962. Stanford Univ. Press.Google Scholar
  3. [3]
    Y. Choueka. Theories of Automata on ω-Tapes: A Simplified Approach. J. Comp. Sys. Sci. 8, pages 117–141, (1974).MathSciNetzbMATHCrossRefGoogle Scholar
  4. [4]
    E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A Unified Approach for Showing Language Containment and Equivalence Between Various Types of ω-Automata. Information Processing Letters 46, pages 301–308, (1993).MathSciNetzbMATHCrossRefGoogle Scholar
  5. [5]
    E. A. Emerson and C. L. Lei. Modalities for model checking: Branching time strikes back. In Proc. Symp. Princ. Prog. Langs. (POPL), pages 84–96. ACM, 1985.Google Scholar
  6. [6]
    M. R. Garey and D. S. Johnson. Computers and Intractability. Freeman, 1979.Google Scholar
  7. [7]
    A. Ginsburg. Algebraic Theory of Automata. Academic Press, New York, 1968.Google Scholar
  8. [8]
    S. Graf and B. Steffen. Compositional Minimization of Finite State Systems. Lecture Notes in Computer Science (LNCS) 531, pages 186–196, (1991).CrossRefGoogle Scholar
  9. [9]
    A. Grasselli and F. Luccio. A Method for Minimizing the Number of Internal States in Incompletely Specified Sequential Networks. IEEE Trans. EC-14, pages 350–359, (1965).Google Scholar
  10. [10]
    D. Gries. Describing an Algorithm by Hopcroft. Acta Inf. 2, pages 97–109, (1973).MathSciNetzbMATHCrossRefGoogle Scholar
  11. [11]
    O. Grumberg and D. E. Long. Model Checking and Modular Verification. In Proc. CONCUR’91, volume 527 of Lecture Notes in Computer Science. Springer Verlag, 1991.Google Scholar
  12. [12]
    G. D. Hachtel, J.-K. Rho, F. Somenzi, and R. Jacoby. Exact and heuristic algorithms for the minimization of incompletelyspecified state machines. In Proc. Eur. Conf. Design Automat, pages 184–191, 1991.CrossRefGoogle Scholar
  13. [13]
    P. Halmos. Lectures on Boolean Algebras. Springer-Verlag, 1974.Google Scholar
  14. [14]
    Z. Har’El and R. P. Kurshan. Software for Analytical Development of Communications Protocol. AT&T Tech. J. 69, pages 45–59, (1990).Google Scholar
  15. [15]
    R. Hojati, V. Singhal, and R. K. Brayton. Edge-Street/Edge-Rabin Automata Environment for Formal Verification Using Language Containment, unpublished, 1994.Google Scholar
  16. [16]
    J. E. Hopcroft. An n log n algorithm for minimizingthe states in a finite automaton. In Paz Kohavi, editor, Theory of Machines and Computations, pages 189–196. Academic Press, 1971.Google Scholar
  17. [17]
    D. Kozen. Lower Bounds for Natural Proof Systems. Proc 18th Symp. Found. Comput. Sci. (FOCS), pages 254 – 266, (1977).Google Scholar
  18. [18]
    D. Kozen. Results on the Propositional Mu-Calculus. Theoretical Computer Science, pages 333–354, (1983).Google Scholar
  19. [19]
    R. P. Kurshan. Complementing Deterministic Büchi Automata in Polynomial Time. J. Comp. Sys. Sci. 35, pages 59–71, (1987).MathSciNetzbMATHCrossRefGoogle Scholar
  20. [20]
    R. P. Kurshan. Reducibility in Analysis of Coordination. LNCIS 103, pages 19–39, (1987).MathSciNetGoogle Scholar
  21. [21]
    R. P. Kurshan. Analysis of Discrete Event Coordination. Lec. Notes in Comput. Sci. (LNCS) 430, pages 414–453, (1990).Google Scholar
  22. [22]
    R. P. Kurshan and L. Lamport. Formal Verification that a 64-Bit Multiplier Multiplies Correctly. Led. Notes Comput. Sci. (LNCS) 697, pages 166–179, 1993.Google Scholar
  23. [23]
    R. P. Kurshan and K. L. McMillan. A Structural Induction Theorem for Processes. Proc. Conf. Princ. Distrib. Comput. (PODC), pages 239–247, (1989).Google Scholar
  24. [24]
    R. P. Kurshan and K. L. McMillan. Analysis of Digital Circuits Through Symbolic Reduction. IEEE Trans. CAD 10, pages 1356–1371, (1991).Google Scholar
  25. [25]
    D. E. Long. Model Checking, Abstraction, and Compositional Verification. PhD thesis, CMU, 1993.Google Scholar
  26. [26]
    Z. Manna and A. Pnueli. Specification and Verification of Concurrent Programs ∀-Automata. In Proc. 14th Symp. Princ. Prog. Lang. (POPL), pages 1–12. ACM, 1987.Google Scholar
  27. [27]
    R. McNaughton. Testing and Generating Infinite Sequences by a Finite Automaton. Inf. Control 9, pages 521–530, (1966).MathSciNetzbMATHCrossRefGoogle Scholar
  28. [28]
    D. E. Muller. Infinite Sequences and Finite Machines. Proc. IEEE Symp. Switch. Cir. Thy. Logic Design 4, pages 3–16, (1963).Google Scholar
  29. [29]
    M. C. Paull and S. H. Unger. Minimizing the Number of States in Incompletely Specified Sequential Switching Functions. IRE Trans. EC-8, pages 356–367, (1959).Google Scholar
  30. [30]
    M. O. Rabin. Automata on Infinite Objects and Church’s Problem. Reg. Conf. Ser. Math. 13, (1972).Google Scholar
  31. [31]
    S. Safra. On the complexity of ω-automata. In Proc. 29th Found. Comput. Sci. (FOCS), pages 319–327, 1988.Google Scholar
  32. [32]
    R. Sikorski. Boolean Algebras. Springer-Verlag, 1969.Google Scholar
  33. [33]
    L. Staiger. Finite-State ω-Languages. J. Comput. Syst. Sci. 27, pages 434–448, (1983).MathSciNetzbMATHCrossRefGoogle Scholar
  34. [34]
    C. Stirling and D. Walker. Local Model Checking in the Modal μ-Calculus. Theoretical Comput. Sci. 86, pages 161–177, (1991).MathSciNetGoogle Scholar
  35. [35]
    R. S. Streett. Propositional Dynamic Logic of Loopingand Converse is Elementary Decidable. Inf. Control 54, pages 121–141, (1982).MathSciNetzbMATHCrossRefGoogle Scholar
  36. [36]
    S. H. Unger. Asynchronous Sequential Switching Circuits. John wiley, 1969. (Reprinted by Krieger).Google Scholar
  37. [37]
    B. Vergauwen and J. Lewi. A Linear Local Model Checking Algorithm for CTL. Lecture Notes in Computer Science (LNCS) 715, pages 447–461, (1993).MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag New York, Inc. 1995

Authors and Affiliations

  • R. P. Kurshan
    • 1
  1. 1.AT&T Bell LaboratoriesUSA

Personalised recommendations