Artículo:
Towards an Efficient Implementation of Tableaux for Reactive Safety Specifications

Fecha

2023-09-12

Editor

Sistedes

Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)

Licencia Creative Commons

Resumen

In this article, we take the first steps to implement a tableau method for deciding realizability of specifications expressed in a safety fragment of linear temporal logic. This tableau method also allows us to extract (i.e., synthesize) a correct system in the case the specification is realizable. In particular, we explain here how to efficiently implement a new normal form called terse normal form, which is crucial to the development of such tableau method.

Descripción

Acerca de Alonso, Ander

Palabras clave

Temporal Logic, Realizability, Safety Specifications, Tableaux
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX