×

A hybrid algorithm for LTL games. (English) Zbl 1138.68459

Logozzo, Francesco (ed.) et al., Verification, model checking, and abstract interpretation. 9th international conference, VMCAI 2008, San Francisco, USA, January 7–9, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78162-2/pbk). Lecture Notes in Computer Science 4905, 309-323 (2008).
Summary: 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 \(10^{11}\) states.
For the entire collection see [Zbl 1134.68006].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
03D05 Automata and formal grammars in connection with logical questions
91A80 Applications of game theory
PDFBibTeX XMLCite
Full Text: DOI