Unconditional Unrealizability Detection in Reactive Systems Modulo Theories

Abstract

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.