¿Cuáles son las propiedades prácticamente computables de los sistemas de transición etiquetados?

Encontré que los sistemas de transición etiquetados son un buen modelo para mi aplicación, es decir, hay un documento sobre modelos de casos de uso con LTS. La pregunta es, ¿qué se puede probar fácilmente sobre los LTS? Me gustaría reutilizar las soluciones existentes para ver si son útiles para mi aplicación. Me gustaría saber qué propiedades de los LTS (y los casos de uso) se pueden probar fácilmente de forma automática, por lo que puedo decidir si existe una contraparte práctica del problema para los casos de uso.

Las fórmulas de la lógica de Hennessy-Milner son muy fáciles de probar sobre los sistemas de transición etiquetados. Sin embargo, esta lógica es lo suficientemente inexpresiva (no hay forma de establecer propiedades de caminos infinitos) que probablemente desee considerar alguna extensión, como la lógica temporal lineal. LTL tiene un problema decidible, pero completo para PSPACE.

El verificador de modelos SPIN es una herramienta ampliamente utilizada para verificar propiedades de LTL de modelos.

Otras dos herramientas, para complementar la sugerida por Neel, son muCRL y mCRL2 . Ambos conjuntos de herramientas tienen una amplia gama de herramientas para definir LTS en varios niveles de abstracción. La visualización del espacio de estado y las herramientas de verificación de modelos también están disponibles. La lógica subyacente es el cálculo modal modal proposicional , que es mucho más expresivo que LTL, pero aún así decidible. Otras herramientas útiles le permiten realizar una bisimulación de módulo de reducción de espacio de estado para obtener la representación más pequeña de su sistema.

$\mathit{NP}\cap \mathit{co\text{-}NP}$

Las propiedades de CTL se pueden verificar en tiempo lineal (ver Clarke et al ).

Hace mucho tiempo, solía trabajar en una empresa donde muchos colegas usaban Rulebase para verificar diseños de circuitos integrados. El lenguaje de propiedad es PSL , está estandarizado por IEEE y es una especie de CTL con esteroides.

En un curso conocí a Isabelle , una "asistente de pruebas genéricas". Admite programación funcional (total) (cercana a ML) y lógica de orden superior. Puede definirse (o buscar) lenguajes para LTS y LTL y probar teoremas sobre ellos. No sé si esto califica como fácil, pero ciertamente funciona.

Si su fondo es CTL interpretado sobre estructuras de Kripke y busca algo similar interpretado sobre LTS, entonces ACTL (CTL basado en acciones) podría ser interesante.

En 1990, R. De Nicola y F. Vaandrager introdujeron ACTL como un CTL basado en acción (Lógicas basadas en acción versus estado para sistemas de transición , Semántica de sistemas de procesos concurrentes (1990), págs. 407-419). Se ha estudiado más en 1993 (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: un marco basado en la acción para verificar las propiedades lógicas y de comportamiento de los sistemas concurrentes , redes de computadoras y sistemas ISDN, Vol. 25, No. 7., pp. 761-778.) Y más recientemente en 2008 (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - Una lógica de árbol de cómputo basada en la acción con un operador a menos , Information Sciences, 178 (6) , pp. 1542-1557.)

La idea principal de ACTL (que no debe confundirse con un subconjunto de CTL con el mismo acrónimo) es tener operadores similares y algoritmos similares para la verificación de modelos como los de CTL. Además, los operadores se definen mediante expresiones de punto fijo análogas a las utilizadas para CTL. La complejidad (no estoy seguro acerca de la expresividad) de ACTL está en algún lugar entre HML y el cálculo modal μ proposicional.