Este estudio describe nuestra amplia experiencia en modelado formal y verificación exhaustiva de sistemas concurrentes, en particular algoritmos de exclusión mutua. La experiencia se centra en el algoritmo de exclusión mutua de Lycklama y Hadzilacos (LH). LH se basa en el tamaño reducido del estado compartido, contiene un mecanismo que intenta hacer cumplir un orden FCFS a los procesos que ingresan a su sección crítica, y encarna el algoritmo de exclusión mutua de Burns y Lamport (BL). La metodología de modelado se basa en autómatas temporizados y el verificador de modelos de la popular caja de herramientas Uppaal. La efectividad del enfoque de modelado y análisis se demuestra primero estudiando la solución de BL y recuperando todas sus propiedades, incluido, en general, su adelantamiento ilimitado, que es la cantidad no limitada de adelantamientos que un proceso puede sufrir antes de acceder a su sección crítica. Luego, el algoritmo LH se investiga en profundidad mostrando que cumple todas las propiedades de exclusión mutua cuando opera con memoria atómica. Sin embargo, como este estudio demuestra, LH no está libre de interbloqueos cuando se utiliza con memoria no atómica. Finalmente, se propone una solución de exclusión mutua de última generación, que se basa en una versión simplificada de LH para procesos, que se utiliza como unidad de arbitraje en una organización de árbol de torneo (TT). Este estudio documenta que el algoritmo basado en TT de LH satisface todas las propiedades de exclusión mutua, con un adelantamiento lineal, tanto utilizando memoria atómica como no atómica.