Learning Models from Temporal-Logic Properties via Explanations. - Miguel Carrillo; David A. Rosenblueth (ExaCt, 2007)

Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections. - Miguel Carrillo; David A. Rosenblueth (ATVA, 2011)

"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis. - Gustavo Arellano; Julián Argil; Eugenio Azpeitia; Mariana Benítez; Miguel Carrillo; Pedro Arturo Góngora; David A. Rosenblueth; Elena R. Álvarez-Buylla (BMC Bioinform., 2011)

Inference of Boolean Networks from Gene Interaction Graphs Using a SAT Solver. - David A. Rosenblueth; Stalin Muñoz; Miguel Carrillo; Eugenio Azpeitia (AlCoB, 2014)

CTL update of Kripke models through protections. - Miguel Carrillo; David A. Rosenblueth (Artif. Intell., 2014)

Actualización de modelos para lógica de árboles de cómputo mediante protecciones - Miguel Carrillo Barajas (2015)

Model-to-Model Transformations for Efficient Time-domain Verification of Concurrent Models by NuSMV Modules. - Miguel Carrillo; Vladimir Estivill-Castro; David A. Rosenblueth (MODELSWARD, 2020)

Verification and Simulation of Time-Domain Properties for Models of Behaviour. - Miguel Carrillo; Vladimir Estivill-Castro; David A. Rosenblueth (MODELSWARD (Revised Selected Papers), 2020)

LLFSMs to TLA+: A Model-to-Text Transformation of Executable Models Enabling Specification and Verification of Multi-Threaded and Concurrent Systems. - Vladimir Estivill-Castro; Miguel Carrillo; David A. Rosenblueth (MODELSWARD, 2025)

Efficient Modelling with Logic-Labelled Finite-State Machines of IEC 61499 Function Blocks: Simulation, Execution and Verification. - Vladimir Estivill-Castro; Miguel Carrillo; David A. Rosenblueth (MODELSWARD, 2025)