Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Efficient detection of vacuity in ACTL formulas

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 1254))

Included in the following conference series:

Abstract

Prepositional logic formulas containing implications can suffer from antecedent failure, in which the formula is true trivially because the pre-condition of the implication is not satisfiable. In other words, the post-condition of the implication does not affect the truth value of the formula. We call this a vacuous pass, and extend the definition of vacuity to cover other kinds of trivial passes in temporal logic. We define w-ACTL, a subset of CTL and show by construction that for every w-ACTL formulaϕ there is a formula w(ϕ), such that: bothϕ and w(ϕ) are true in some model M iffϕ passes vacuously. A useful side-effect of w(ϕ) is that if false, any counter-example is also a non-trivial witness of the original formulaϕ.

Similar content being viewed by others

Keywords

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.

References

  1. D. Beatty and R. Bryant, “Formally verifying a microprocessor using a simulation methodology”, Design Automation Conference '94, pp. 596–602.

    Google Scholar 

  2. I. Beer, S. Ben-David, C. Eisner, A. Landver, “RuleBase: an Industry-Oriented Formal Verification Tool”, in Proc. 33rd Design Automation Conference 1996, pp. 655–660.

    Google Scholar 

  3. E.M. Clarke and E.A. Emerson, “Design and synthesis of synchronization skeletons using Branching Time Temporal Logic”, in Proc. Workshop on Logics of Programs, Lecture Notes in Computer Science, Vol. 131 (Springer, Berlin, 1981) pp. 52–71.

    Google Scholar 

  4. E.M. Clark and E.A. Emerson, “Characterizing Properties of Parallel Programs as Fixed-point”, in Seventh International Colloquium on Automata, Languages, and Programming, Volume 85 of LNCS, 1981.

    Google Scholar 

  5. E. Clarke, O. Grumberg, K. McMillan, X. Zhao, “Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking”, Design Automation Conference 1995, pp. 427–432.

    Google Scholar 

  6. O. Grumberg and D. Long, “Model checking and modular verification.” In J.C.M. Baeten and J.F. Groote, editors, Proccedings of CONCUR '91: 2nd International Conference on Concurrency Theory, Volume 527 of LNCS, 1991.

    Google Scholar 

  7. R. Hojati, R.K. Brayton and R.P. Kurshan, “BDD-based debugging of designs using language containment and fair CTL.” CAV '93, pp. 41–58.

    Google Scholar 

  8. R. Kurshan, “Analysis of Discrete Event Coordination,” LNCS 1990.

    Google Scholar 

  9. D. Long, “Model Checking, Abstraction and Compositional Verification”, Ph.D. Thesis, CMU, 1993.

    Google Scholar 

  10. K.L. McMillan, “Symbolic Model Checking”, Kluwer Academic Publishers, 1993.

    Google Scholar 

  11. B. Plessier and C. Pixley, “Formal Verification of a Commercial Serial Bus Interface”, International Phoenix Conference on Computers and Communications, 1995, pp. 378–382.

    Google Scholar 

  12. G. Shurek, O. Grumberg, “The Computer-Aided Modular Framework —Motivation, Solutions and Evaluation Criteria”, Workshop on Computer Aided Verification, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Haifa Research Laboratory, IBM Science and Technology, Matam, Haifa, Israel

    Ilan Beer, Shoham Ben-David, Cindy Eisner & Yoav Rodeh

Authors
  1. Ilan Beer

    You can also search for this author inPubMed Google Scholar

  2. Shoham Ben-David

    You can also search for this author inPubMed Google Scholar

  3. Cindy Eisner

    You can also search for this author inPubMed Google Scholar

  4. Yoav Rodeh

    You can also search for this author inPubMed Google Scholar

Editor information

Orna Grumberg

Rights and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beer, I., Ben-David, S., Eisner, C., Rodeh, Y. (1997). Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_28

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp