Un Formalismo de Reescritura de Marcos Modales Dinámicos con Restricción de Viabilidad y Descenso Estructural

Este trabajo desarrolla un formalismo de reescritura estructural para marcos modales dinámicos, concebido como un DSL de segundo orden orientado al meta‑control de sistemas concurrentes. En lugar de modelar la evolución de estados, el sistema SCA/Operium actúa directamente sobre la relación de accesibilidad de un marco de Kripke, entendida como espacio de posibilidad mutable. La semántica estática impone un Axioma de Compensación Estructural que garantiza la no‑inflación del grafo mediante un presupuesto algebraico estricto, mientras que la semántica denotacional se formula como un DMTS gobernado por trazas de Mazurkiewicz. Se demuestra la terminación estructural del sistema, la corrección semántica del mecanismo de reescritura y la completitud respecto a transformaciones contractivas sobre marcos modales. El resultado es una lógica dinámica tipada capaz de modelar mutaciones de posibilidad en sistemas concurrentes de manera segura, determinista y computacionalmente tractable.