SySLite (Syntax-Guided Past-time LTL Synthesizer & Enumerator)


SysLite makes use of decision and synthesis procedures (i.e., SAT, SMT, and SyGuS) to learn Pastime LTL formulas from a finite set of example traces. These example traces describe the intended and unintended behavior in terms of positive and negative traces that can come from various application domains (i.e, security policy logs, protocols, and execution of a system or design model, among others).

Tool Link