06076922

a

06076922 Latte, Markus Lange, Martin Branching time? pruning time! Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26--29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 393-407 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-31365-3_31

Summary: The full branching time logic {\sc ctl}* is a well-known specification logic for reactive systems. Its satisfiability and model checking problems are well understood. However, it is still lacking a satisfactory sound and complete axiomatisation. The only proof system known for {\sc ctl}* is Reynolds' which comes with an intricate and long completeness proof and, most of all, uses rules that do not possess the subformula property. In this paper we consider a large fragment of {\sc ctl}* which is characterised by disallowing certain nestings of temporal operators inside universal path quantifiers. This subsumes {\sc ctl}$^{ + }$ for instance. We present infinite satisfiability games for this fragment. Winning strategies for one of the players represent infinite tree models for satisfiable formulas. These can be pruned into finite trees using fixpoint strengthening and some simple combinatorial machinery such that the results represent proofs in a Hilbert-style axiom system for this fragment. Completeness of this axiomatisation is a simple consequence of soundness of the satisfiability games.