Advertisement

Alaska

Antichains for Logic, Automata and Symbolic Kripke Structures Analysis
  • Martin De Wulf
  • Laurent Doyen
  • Nicolas Maquet
  • Jean-Francois Raskin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

ALASKA is a verification tool that implements new algorithms based on antichains [5, 7, 6] to efficiently solve the emptiness problem for both alternating finite automata (AFW) and alternating Büchi automata (ABW). Using the well-known translation from LTL to alternating automata, the tool can decide the satisfiability and validity problems for LTL over finite or infinite words. Moreover, ALASKA can solve the model-checking problem for ABW, LTL, AFW and finite-word LTL over symbolic (BDD-encoded) Kripke structures.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bloem, R., Cimatti, A., Pill, I., Roveri, M., Semprini, S.: Symbolic implementation of alternating automata. In: Ibarra, O.H., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol. 4094, pp. 208–218. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model checker. STTT 2(4), 410–425 (2000)CrossRefzbMATHGoogle Scholar
  3. 3.
    Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: CAV 1994. LNCS, vol. 818, pp. 415–427. Springer, Heidelberg (1994)Google Scholar
  4. 4.
    Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    De Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: Alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63–77. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Doyen, L., Raskin, J.-F.: Improved algorithms for the automata-based approach to model-checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 451–465. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus. In: LICS, pp. 267–278 (1986)Google Scholar
  9. 9.
    Fritz, C.: Constructing Büchi automata from LTL using simulation relations for alternating Büchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 191–205. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Heljanko, K., Junttila, T.A., Keinänen, M., Lange, M., Latvala, T.: Bounded model checking for weak alternating büchi automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 95–108. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Löding, C., Thomas, W.: Alternating automata and logics over infinite words. In: IFIP TCS, pp. 521–535 (2000)Google Scholar
  14. 14.
    Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. In: CAAP, pp. 195–210 (1984)Google Scholar
  15. 15.
    Muller, D., Saoudi, A., Schnupp, P.: Alternating automata. The weak monadic theory of the tree, and its complexity. In: Knott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 275–283. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  16. 16.
    Rozier, K., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Ruys, T., Holzmann, G.: Advanced Spin tutorial. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 304–305. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 350–363. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: Goal extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 346–350. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: 8th Banff Higher Order Workshop. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1995)Google Scholar
  22. 22.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332–344. IEEE Computer Society Press, Los Alamitos (1986)Google Scholar
  23. 23.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Martin De Wulf
    • 1
  • Laurent Doyen
    • 2
  • Nicolas Maquet
    • 1
  • Jean-Francois Raskin
    • 1
  1. 1.Université Libre de Bruxelles (ULB)Belgium
  2. 2.École Polytechnique Fédérale de Lausanne (EPFL)Switzerland

Personalised recommendations