Model checking for time division multiple access systems. - Marco Antonio Muñiz Rodríguez (2015)