ACTL ∩ LTL Synthesis
We study the synthesis problem for specifications of the common fragment of ACTL (computation tree logic with only universal path quantification) and LTL (linear-time temporal logic). Key to this setting is a novel construction for translating properties from LTL to very-weak automata, whenever possible. Such automata are structurally simple and thus amenable to optimizations as well as symbolic implementations. Based on this novel construction, we describe a synthesis approach that inherits the efficiency of generalized reactivity(1) synthesis, but is significantly richer in terms of expressivity.
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.