2012 | OriginalPaper | Chapter
Branching Time? Pruning Time!
Authors : Markus Latte, Martin Lange
Published in: Automated Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
The full branching time logic
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
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
ctl*
which is characterised by disallowing certain nestings of temporal operators inside universal path quantifiers. This subsumes
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.