Two Algorithms for Model Checking of Regular Linear Temporal Logic

Abstract

Este trabajo estudia el problema de ver si una fórmula es satisfacible—the satisfiability problem—y el problema de model checking para Regular Linear Temporal Logic (RLTL). En el contexto de la verificación de programas, el estudio de técnicas de verificación de sistemas reactivos—aquellos que interactúan con el entorno y responden a estímulos—ha ganado especial interés dentro de la comunidad científica. El model checking es una técnica automática muy poderosa para verificar la corrección de estos sistemas. Un model checker está típicamente compuesto por un lenguaje de descripción para modelar sistemas, un lenguaje de especificación para codificar propiedades y un método de verificación. Para verificar que un sistema satisface una propiedad, el usuario describe el modelo, afirma las hipótesis y el proceso de verificación descubre si dichas hipótesis son validas en el modelo. Una de las características más importantes del model checking es la capacidad de producir contraejemplos cuando una propiedad no se satisface en el sistema. El model checking está basado en lógica temporal, en la cuál el valor de verdad de una fórmula depende de la evolución del sistema. Linear Temporal Logic (LTL) es una lógica temporal que en la actualidad es ampliamente aceptada como formalismo para la especificación y verificación de sistemas concurrentes y sistemas reactivos. No todos los lenguajes ω-regulares pueden ser expresados por LTL y esta falta de expresividad suele aparecer en la práctica. Al mismo tiempo, algunos estudios señalan que las expresiones regulares, en combinación con LTL, son muy convenientes para escribir especificaciones formales. Regular Linear Temporal Logic (RLTL), ha sido propuesta como una extensión de LTL con constructores basados en expresiones regulares . RLTL extiende la expresividad de LTL a todos los lenguajes ω-regulares, tiene una base formal sólida y complejidad óptima para extensiones de LTL. En este trabajo presentamos dos nuevos enfoques al problema de ver si una formula es satisfacible (satisfiability problem) y al problema del model checking para RLTL. Por un lado, este trabajo extiende a Regular Linear Temporal Logic las ideas de bounded model checking—una técnica de verificación de propiedades temporales lineales basada en procedimientos SAT—desarrollada para Linear Temporal Logic. Como parte de este esfuerzo se presenta una traducción de expresiones RLTL a fórmulas SAT. Por el otro lado, este trabajo estudia el enfoque al model checking para RLTL basado en la teoría de autómatas—el cuál reduce este problema de verificación a la construcción de autómatas y problemas de decisión sobre autómatas. Se presenta una traducción de expresiones RLTL a strong alternating parity automata, junto con una traducción de los autómatas resultantes a non-deterministic Büchi automata. Además, introducimos la noción de stratified automata, la cuál nos permite realizar una traducción basada en ránkings mucho más eficiente. Los resultados experimentales obtenidos son muy alentadores. [ABSTRACT] This thesis studies the satisfiability and model checking problem for Regular Linear Temporal Logic RLTL). In the context of program verification, model checking is an automatic, powerful technique to verify the correctness of systems. In particular, the verification of reactive systems has gathered much research effort. Reactive systems are systems that interacts with their environments and respond to stimuli. A model checker is typically comprised by a description language for modeling systems, a specification language for encoding properties and a verification method. To verify that a system verifies a property,the user describes a model, asserts hypotheses, and the verification process discovers whether such hypotheses are valid on the model. One of the most important features of model checking is that counterexamples can be produced when a property fails to be satisfied in the system. Model checking is based on temporal logic, where the truth depends on the evolution of the system. Linear Temporal Logic (LTL) is a temporal logic that is now a widely accepted formalism for the specification and verification of concurrent and reactive systems. LTL cannot express all ω-regular properties and this lack of expressivity seems to surface in practice. At the same time, some studies point out that regular expressions are very convenient in addition to LTL in formal specifications. Regular Linear Temporal Logic (RLTL), a logic for the temporal frame, was proposed as an extension of LTL with constructs based on regular expressions. RLTL extends the expressive power of LTL to all ω-regular languages and has a formal foundation with well-studied complexity results. In this work, we provide two novel approaches to the satisfiability and model checking problems for RLTL. On the one hand, this work extends the ideas of bounded model checking—a verification technique for linear time properties based on propositional decision procedures (SAT)—developed for standard Linear Temporal Logic into Regular Linear Temporal Logic. As part of this eort, a translation from RLTL expressions into SAT formulas is presented. On the other hand, this work studies the automata-theoretic approach to model checking for RLTL—which reduces this verification problem to automata constructions and automata decision problems. A translation from RLTL expressions into strong alternating parity automata is presented along with a translation from the resulting automata into non-deterministic Büchi automata. We also introduce the notion of stratified automata, leading to a more efficient ranking translation with encouraging experimental results.