Lógica temporal métrica
La lógica temporal métrica (MTL) es un caso especial de lógica temporal . Es una extensión de la lógica temporal en la que los operadores temporales son reemplazados por versiones con restricciones de tiempo como hasta , siguiente , desde y operadores anteriores . Es una lógica de tiempo lineal que asume tanto la abstracción entrelazada como la del reloj ficticio. Se define sobre una semántica de tiempo entero débilmente monótona basada en puntos. Para MTL, la complejidad exacta de los problemas de satisfacibilidad es conocida e independiente de la interpretación basada en intervalos o en puntos, sincrónica (es decir, estrictamente monótona) o asincrónica (es decir, débilmente monótona): EXPSPACE-completo. [1]
MTL se ha descrito como un formalismo de especificación destacado para sistemas en tiempo real. [2] El MTL completo sobre infinitas palabras cronometradas es indecidible. [3]
La lógica temporal métrica completo se define de manera similar a la lógica temporal lineal , donde se añade un conjunto de número real no negativo a temporales operadores modales U y S . Formalmente, MTL se construye a partir de:
Cuando se omite el subíndice, es implícitamente igual a .
Tenga en cuenta que el siguiente operador N no se considera parte de la sintaxis MTL. En su lugar, se definirá a partir de otros operadores.
El fragmento pasado de la lógica temporal métrica , denotado como pasado-MTL, se define como la restricción de la lógica temporal métrica completa sin el operador hasta. De manera similar, el fragmento futuro de lógica temporal métrica , denotado como futuro-MTL, se define como la restricción de la lógica temporal métrica completa sin el operador since.