Abstract
In the game theoretic approach to the synthesis of reactive systems, specifications are often given in linear time logic (LTL). Computing a winning strategy to an infinite game whose winning condition is the set of LTL properties is the main step in obtaining an implementation. We present a practical hybrid algorithm-a combination of symbolic and explicit algorithm-for the computation of winning strategies for unrestricted LTL games that we have successfully applied to synthesize reactive systems with up to 1011 states. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Sohail, S., Somenzi, F., & Ravi, K. (2008). A hybrid algorithm for LTL games. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4905 LNCS, pp. 309–323). https://doi.org/10.1007/978-3-540-78163-9_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
