Abstract
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 [27], but is significantly richer in terms of expressivity. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Ehlers, R. (2012). ACTL ∩ LTL synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 39–54). https://doi.org/10.1007/978-3-642-31424-7_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
