ACTL ∩ LTL Synthesis
Rüdiger Ehlers
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.
24rd International Conference on Computer Aided Verification (CAV 2012).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.