La lógica temporal de intervalos (también lógica de intervalos ) es una lógica temporal para representar el razonamiento lógico proposicional y de primer orden sobre períodos de tiempo que es capaz de manejar tanto la composición secuencial como la paralela. En lugar de tratar con secuencias infinitas de estados, la lógica temporal de intervalos trata con secuencias finitas.
Las lógicas temporales de intervalo encuentran aplicación en informática , inteligencia artificial y lingüística . La lógica temporal de intervalos de primer orden se desarrolló inicialmente en la década de 1980 para la especificación y verificación de protocolos de hardware . La lógica temporal de intervalos ( ITL ) es una forma específica de lógica temporal , desarrollada originalmente por Ben Moszkowski para su tesis en la Universidad de Stanford . [1] Es útil en la descripción formal de hardware y software.para sistemas basados en computadora. Hay herramientas disponibles para ayudar en este proceso. Tempura proporciona un marco ITL ejecutable . La composicionalidad es un tema importante y una consideración en el diseño de ITL.
Los derivados notables de la lógica temporal de intervalos son la lógica de intervalos gráficos, la lógica de intervalos con signo y la lógica de intervalos futuros .