Dissertação

Linear Temporal Logic: Separation and Translation EVALUATED

Lógica temporal linear com as modalidades Since e Until tem o mesmo poder expressivo, sobre ordens lineares completas, que um fragmento de primeira-ordem conhecido como FOMLO. Também se sabe que uma lógica temporal linear, assumindo algumas propriedades básicas, tem a mesma expressividade que FOMLO se e só se tem uma propriedade, chamada separação, que qualquer fórmula é equivalente a uma combinação Booleana de fórmulas tal que cada uma delas apenas considera o passado, presente ou futuro. Neste texto apresenta-se algoritmos simples e as suas implementações para fazer esta separação da lógica temporal linear com Since e Until, sobre ordens discretas e completas, e tradução de FOMLO para esta mesma lógica.
Lógica Temporal, LTL, FOMLO, Separação, Tradução, Completude Expressiva

Novembro 3, 2017, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

João Filipe Quintas dos Santos Rasga

Departamento de Matemática (DM)

Professor Auxiliar