Advertisement

Abstract

An alternative to the traditional Büchi Automata (BA), called Testing Automata (TA) was proposed by Hansen et al. [8,6] to improve the automata-theoretic approach to LTL model checking. In previous work [2], we proposed an improvement of this alternative approach called TGTA (Generalized Testing Automata). TGTA mixes features from both TA and TGBA (Generalized Büchi Automata), without the disadvantage of TA, which is the second pass of the emptiness check algorithm. We have shown that TGTA outperform TA, BA and TGBA for explicit and symbolic LTL model checking. However, TA and TGTA are less expressive than Büchi Automata since they are able to represent only stutter-invariant LTL properties (LTL ∖X) [13]. In this paper, we show how to extend Generalized Testing Automata (TGTA) to represent any LTL property. This allows to extend the model checking approach based on this new form of testing automata to check other kinds of properties and also other kinds of models (such as Timed models). Implementation and experimentation of this extended TGTA approach show that it is statistically more efficient than the Büchi Automata approaches (BA and TGBA), for the explicit model checking of LTL properties.

Keywords

Model Check Linear Temporal Logic Small Product Atomic Proposition Acceptance Condition 
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. 1.
    Ben Salem, A.E., Duret-Lutz, A., Kordon, F.: Generalized Büchi automata versus testing automata for model checking. In: Proc. of SUMo 2011, vol. 726, pp. 65–79. CEUR (2011)Google Scholar
  2. 2.
    Ben Salem, A.-E., Duret-Lutz, A., Kordon, F.: Model Checking Using Generalized Testing Automata. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) ToPNoC VI. LNCS, vol. 7400, pp. 94–122. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. 3.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized Büchi automata. In: Proc. of MASCOTS 2004, pp. 76–83. IEEE Computer Society Press (2004)Google Scholar
  5. 5.
    Etessami, K.: Stutter-invariant languages, ω-automata, and temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 236–248. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53–70. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulæ to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection of livelock properties. In: Proc. of FMICS 2002. ENTCS, vol. 66(2). Elsevier (2002)Google Scholar
  9. 9.
    Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Hugues, J., Thierry-Mieg, Y., Kordon, F., Pautet, L., Barrir, S., Vergnaud, T.: On the formal verification of middleware behavioral properties. In: Proc. of FMICS 2004. ENTCS, vol. 133, pp. 139–157. Elsevier (2004)Google Scholar
  11. 11.
    Kordon, F., et al.: Report on the model checking contest at petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) ToPNoC VI. LNCS, vol. 7400, pp. 169–196. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    MoVe/LRDE. The Spot home page: http://spot.lip6.fr (2014)
  13. 13.
    Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters 63(5), 243–246 (1995)CrossRefMathSciNetGoogle Scholar
  14. 14.
    Sebastiani, R., Tonetta, S.: “More deterministic” vs. “Smaller” Büchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Tauriainen, H.: Automata and Linear Temporal Logic: Translation with Transition-based Acceptance. PhD thesis, Helsinki University of Technology, Espoo, Finland (September 2006)Google Scholar
  16. 16.
    Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137–150. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  1. 1.LRDE, EPITALe Kremlin-Bic^etreFrance

Personalised recommendations