Computing Simulations over Tree Automata

(Efficient Techniques for Reducing Tree Automata)
  • Parosh A. Abdulla
  • Ahmed Bouajjani
  • Lukáš Holík
  • Lisa Kaati
  • Tomáš Vojnar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)


We address the problem of computing simulation relations over tree automata. In particular, we consider downward and upward simulations on tree automata, which are, loosely speaking, analogous to forward and backward relations over word automata. We provide simple and efficient algorithms for computing these relations based on a reduction to the problem of computing simulations on labelled transition systems. Furthermore, we show that downward and upward relations can be combined to get relations compatible with the tree language equivalence, which can subsequently be used for an efficient size reduction of nondeterministic tree automata. This is of a very high interest, for instance, for symbolic verification methods such as regular model checking, which use tree automata to represent infinite sets of reachable configurations. We provide experimental results showing the efficiency of our algorithms on examples of tree automata taken from regular model checking computations.


Model Check Computing Simulation Transition Rule Label Transition System Kripke Structure 
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.


  1. 1.
    Abdulla, P., Bouajjani, A., Holík, L., Kaati, L., Vojnar, T.: Computing Simulations over Tree Automata. Technical report, FIT-TR-2007-001, FIT, Brno University of Technology, Czech Republic (2007)Google Scholar
  2. 2.
    Abdulla, P., Högberg, J., Kaati, L.: Bisimulation Minimization of Tree Automata. In: H. Ibarra, O., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol. 4094, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Abdulla, P., Jonsson, B., Mahata, P., d’Orso, J.: Regular Tree Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Abdulla, P., Legay, A., d’Orso, J., Rezine, A.: Tree Regular Model Checking: A Simulation-based Approach. The Journal of Logic and Algebraic Programming 69(1-2), 93–121 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking. In: ENTCS, vol. 149(1), pp. 37–48. Elsevier, Amsterdam (2006)Google Scholar
  6. 6.
    Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Bouajjani, A., Touili, T.: Extrapolating Tree Transformations. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Bouajjani, A., Touili, T.: Reachability Analysis of Process Rewrite Systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, Springer, Heidelberg (2003)Google Scholar
  9. 9.
    Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (1997), Available on:
  10. 10.
    Henzinger, M., Henzinger, T., Kopke, P.: Computing simulations on finite and infinite graphs. In: Proc. of FOCS 1995, IEEE, Los Alamitos (1995)Google Scholar
  11. 11.
    Maletti, A., Högberg, J., May, J.: Backward and forward bisimulation minimisation of tree automata. In: Holub, J., Žďárek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 109–121. Springer, Heidelberg (2007)Google Scholar
  12. 12.
    Klarlund, N., Møller, A.: MONA Version 1.4 User Manual, BRICS, Department of Computer Science, University of Aarhus, Denmark (2001)Google Scholar
  13. 13.
    Paige, R., Tarjan, R.: Three Partition Refinement Algorithms. SIAM Journal on Computing 16, 973–989 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Ranzato, F., Tapparo, F.: A New Efficient Simulation Equivalence Algorithm. In: Proc. of LICS 2007, IEEE CS, Los Alamitos (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Parosh A. Abdulla
    • 1
  • Ahmed Bouajjani
    • 2
  • Lukáš Holík
    • 3
  • Lisa Kaati
    • 1
  • Tomáš Vojnar
    • 3
  1. 1.University of UppsalaSweden
  2. 2.LIAFA, University Paris 7France
  3. 3.FITBrno University of TechnologyCzech Republic

Personalised recommendations