P. A. Abdulla, Y. Chen, L. Holík, R. Mayr, and T. Vojnar, When Simulation Meets Antichains, Proc. TACAS, pp.158-174, 2010.
DOI : 10.1007/978-3-642-12002-2_14
URL : https://hal.archives-ouvertes.fr/inria-00460294

A. V. Aho, J. E. Hopcroft, and J. D. Ullman, The Design and Analysis of Computer Algorithms, 1974.

A. Aiken and B. R. Murphy, Implementing regular tree expressions, FPCA, pp.427-447, 1991.
DOI : 10.1007/3540543961_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3766

J. C. Baeten, J. A. Bergstra, and J. W. Klop, Decidability of bisimulation equivalence for processes generating context-free languages
DOI : 10.1007/3-540-17945-3_5

F. Bartels, On generalized coinduction and probabilistic specification formats, 2004.

F. Bonchi and D. Pous, Web appendix for this paper, 2012.

A. Bouajjani, P. Habermehl, and T. Vojnar, Abstract Regular Model Checking, Proc. CAV, 2004.
DOI : 10.1007/978-3-540-27813-9_29
URL : https://hal.archives-ouvertes.fr/hal-00159512

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

J. A. Brzozowski, Canonical regular expressions and minimal state graphs for definite events, Mathematical Theory of Automata, pp.529-561, 1962.

S. Christensen, H. Hüttel, and C. Stirling, Bisimulation Equivalence Is Decidable for All Context-Free Processes, Information and Computation, vol.121, issue.2, pp.143-148, 1995.
DOI : 10.1006/inco.1995.1129

J. Fernandez, L. Mounier, C. Jard, and T. Jron, On-the-fly verification of finite transition systems, Formal Methods in System Design, vol.2, issue.23, pp.251-273, 1992.
DOI : 10.1007/BF00121127
URL : https://hal.archives-ouvertes.fr/inria-00074812

M. R. Henzinger, T. A. Henzinger, and P. W. Kopke, Computing simulations on finite and infinite graphs, Proceedings of IEEE 36th Annual Foundations of Computer Science, pp.453-462, 1995.
DOI : 10.1109/SFCS.1995.492576

Y. Hirshfeld, M. Jerrum, and F. Moller, A polynomial algorithm for deciding bisimilarity of normed context-free processes, Theoretical Computer Science, vol.158, issue.1-2, pp.143-159, 1996.
DOI : 10.1016/0304-3975(95)00064-X

J. E. Hopcroft, AN n log n ALGORITHM FOR MINIMIZING STATES IN A FINITE AUTOMATON, Proc. International Symposium of Theory of Machines and Computations, pp.189-196, 1971.
DOI : 10.1016/B978-0-12-417750-5.50022-1

J. E. Hopcroft and R. M. Karp, A linear algorithm for testing equivalence of finite automata, 1971.

J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages and Computation, 1979.

H. Hosoya, J. Vouillon, and B. C. Pierce, Regular expression types for XML, ACM Transactions on Programming Languages and Systems, vol.27, issue.1, pp.46-90, 2005.
DOI : 10.1145/1053468.1053470
URL : https://hal.archives-ouvertes.fr/hal-00009271

D. Lee and M. Yannakakis, Online minimization of transition systems (extended abstract), Proceedings of the twenty-fourth annual ACM symposium on Theory of computing , STOC '92, pp.264-274, 1992.
DOI : 10.1145/129712.129738

O. Lengál, J. Simácek, and T. Vojnar, VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata, TACAS, pp.79-94, 2012.
DOI : 10.1007/978-3-642-28756-5_7

M. Lenisa, From Set-theoretic Coinduction to Coalgebraic Coinduction: some results, some problems, Electronic Notes in Theoretical Computer Science, vol.19, pp.2-22, 1999.
DOI : 10.1016/S1571-0661(05)80265-8

D. Lucanu and G. Rosu, Circular Coinduction with Special Contexts, Proc. ICFEM, pp.639-659, 2009.
DOI : 10.1007/978-3-642-10373-5_33

A. Meyer and L. J. Stockmeyer, Word problems requiring exponential time, Proc. STOC, pp.1-9, 1973.

R. Milner, Communication and Concurrency, 1989.

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, II, Information and Computation, vol.100, issue.1, pp.1-77, 1992.
DOI : 10.1016/0890-5401(92)90009-5

D. Pous, Complete Lattices and Up-To Techniques, Proc. APLAS, pp.351-366, 2007.
DOI : 10.1007/978-3-540-76637-7_24
URL : https://hal.archives-ouvertes.fr/ensl-00155308

J. Rutten, Automata and coinduction (an exercise in coalgebra), Proc. CONCUR, pp.194-218, 1998.
DOI : 10.1007/BFb0055624

D. Sangiorgi, On the bisimulation proof method, Mathematical Structures in Computer Science, vol.8, issue.5, pp.447-479, 1998.
DOI : 10.1017/S0960129598002527

D. Sangiorgi, Introduction to Bisimulation and Coinduction, 2011.
DOI : 10.1017/CBO9780511777110
URL : https://hal.archives-ouvertes.fr/hal-00907026

A. Silva, F. Bonchi, M. Bonsangue, and J. Rutten, Generalizing the powerset construction, coalgebraically, Proc. FSTTCS of LIPIcs Leibniz-Zentrum fuer Informatik, pp.272-283, 2010.

D. Tabakov and M. Vardi, Experimental Evaluation of Classical Automata Constructions, Proc. LPAR, pp.396-411, 2005.
DOI : 10.1007/11591191_28

D. Turi and G. D. Plotkin, Towards a mathematical operational semantics, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp.280-291, 1997.
DOI : 10.1109/LICS.1997.614955

M. D. Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, Antichains: A New Algorithm for Checking Universality of Finite Automata, Proc. CAV, pp.17-30, 2006.
DOI : 10.1007/11817963_5