Pruebas cíclicas abstractas

Los sistemas de pruebas cíclicas abstractas permiten derivaciones que son grafos finitos en contraste con los árboles de derivación convencionales. La solidez de tales pruebas se asegura imponiendo una condición de solidez sobre las derivaciones. La condición más común es la condición de traza global (GTC), una condición sobre los caminos infinitos a través del grafo de derivación. Para dar un tratamiento uniforme de tales sistemas de pruebas cíclicas, Brotherston propuso una noción abstracta de traza. Extendemos el enfoque de Brotherston a una interpretación teórica de categorías de derivaciones cíclicas, avanzando el marco de dos maneras: primero, introducimos álgebras de activación que permiten una formalización más natural de las condiciones de traza en los sistemas de pruebas cíclicas existentes. Segundo, tener en cuenta la composición de la información de traza nos permite derivar resultados novedosos sobre pruebas cíclicas, como la introducción de una condición de traza al estilo de Ramsey. Además, conectamos nuestra noción de traza con la teoría de autómatas y demostramos que verificar la GTC para pruebas cíclicas abstractas con ciertas condiciones de traza es PSPACE-completo.