Unconditional Unrealizability Detection in Reactive Systems Modulo Theories





Publicado en

Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024)

Licencia Creative Commons


Linear Temporal Logic modulo theories (LTLT ) extends LTL by allowing atomic propositions to be literals from the theory T . Realizability of an LTLT specification φ is proven to be decidable by a Boolean abstraction that generates an equi-realizable LTL specification from φ. This abstraction method also opens the door for a more thoughtful analysis of LTLT specifications. In this work in progress, we address how to produce informative traces of LTLT specifications by finding strategies of the players such that certain desired or undesired goals are reached. In particularly, we show how to produce unconditional unrealizability witnesses for an uncontrollable environment. We present two approaches based on unrollings of formulae: the first one characterizes the problem using SMT-with-quantifiers; the second one Booleanizes the LTLT formula and then uses QBF solving. We show the latter is faster and provides more termination guarantees. To the best of our knowledge, this is the first such specification analysis over such an expressive fragment of the logic.


Acerca de Rodriguez, Andoni

Palabras clave

Reactive Systems, Reactive Synthesis, Realizability/unrealizability, LTL Modulo Theories, Trace Analysis, Strategy Search, QBF, QSMT, Boolean Abstractions
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX