Lógica Temporal e Modal na Computação

As lógicas temporal e modal estendem a lógica clássica com operadores para tempo e possibilidade, fornecendo linguagens precisas para especificar como um programa ou sistema reativo deve se comportar ao longo de toda a sua execução.

Definition

A lógica temporal aumenta a lógica proposicional ou de primeira ordem com operadores que descrevem quando as propriedades se mantêm ao longo de uma computação, como sempre, eventualmente e até que; a lógica modal generaliza isso com operadores para necessidade e possibilidade sobre uma estrutura de estados e transições.

Scope

Este tópico abrange lógicas temporais de tempo linear e tempo ramificado, como LTL e CTL, lógicas modais, incluindo lógica dinâmica e o cálculo-mu modal, a expressão de propriedades de segurança e vivacidade, e os problemas algorítmicos de verificação de modelo (model checking) e satisfatibilidade que tornam essas lógicas centrais para a verificação automatizada.

Core questions

• Como uma lógica pode expressar que algo bom eventualmente acontece ou que algo ruim nunca acontece?
• Qual é a diferença entre raciocinar sobre uma única execução e sobre todos os futuros possíveis?
• Como a verificação de que um sistema satisfaz uma propriedade temporal é tornada algorítmica?
• Quais lógicas temporais equilibram o poder expressivo com a verificação eficiente?

Key theories

Lógica temporal para especificação de programas

Pnueli demonstrou que a lógica temporal captura a correção de programas reativos e concorrentes, expressando propriedades sobre suas execuções, fornecendo uma linguagem uniforme para requisitos de segurança e vivacidade.

Verificação de modelo (model checking) de lógica de tempo ramificado

Clarke e Emerson introduziram a lógica da árvore de computação (computation tree logic) e um algoritmo para verificá-la automaticamente contra um modelo de estado finito, fundando o campo da verificação de modelo.

Clinical relevance

As lógicas temporais são as linguagens de especificação de verificadores de modelo (model checkers) usados rotineiramente para verificar projetos de hardware, protocolos de comunicação e software concorrente, detectando impasses (deadlocks) e violações de segurança e vivacidade antes da implantação; esta tecnologia rendeu aos seus criadores o Prêmio Turing e é padrão no design de chips.

History

Pnueli propôs a lógica temporal para raciocinar sobre programas em 1977, e Clarke e Emerson, com Queille e Sifakis independentemente, desenvolveram a verificação de modelo (model checking) por volta de 1981. A abordagem foi ampliada para sistemas industriais através de métodos simbólicos no início dos anos 1990, e seus criadores receberam o Prêmio Turing pela técnica.

Key figures

• Amir Pnueli
• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis

Seminal works

• clarkeEmerson1981
• huthRyan2004

Frequently asked questions

Qual é a diferença entre lógica de tempo linear e de tempo ramificado?

Lógicas de tempo linear, como LTL, descrevem propriedades de um único caminho de execução, possivelmente infinito. Lógicas de tempo ramificado, como CTL, quantificam sobre a árvore de todos os futuros possíveis a partir de cada estado, permitindo afirmar que ao longo de algum caminho ou ao longo de todos os caminhos uma propriedade se mantém. Elas possuem diferentes poderes expressivos e algoritmos de verificação.

Como a verificação de modelo (model checking) usa essas lógicas?

Um sistema é representado como um modelo de estado finito e uma propriedade desejada como uma fórmula de lógica temporal. Um verificador de modelo explora exaustivamente os estados para determinar se a fórmula se mantém e, se falhar, produz um traço de contraexemplo, tornando a verificação tanto automática quanto diagnóstica.