Grafo de alcanzabilidad, detección de deadlock y livelock, árbol de Karp-Miller (aceleración ω) para la finitud, simulación temporizada con transiciones exponenciales, visualización DOT/PNG, pruebas unitarias.
Académique 2025 → 2026
Biblioteca de redes de Petri
Demostrar que un sistema concurrente no se bloquea, en un grafo, no con un test que pasa.
- Rol
- Proyecto en pareja, Modelos y Especificaciones (Máster 2)
- Contexto
- Université Marie & Louis Pasteur
- Estado
- Terminado
- Python
- Tests automatisés