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 July 2012
Contact Data Privacy Policy Imprint
Home People Publications
More