Nondeterministic update of CTL models by preserving satisfaction through protections

Abstract

We present a recursive algorithm to update a Kripke model so as to satisfy a formula of the Computation-Tree Logic (CTL). Recursive algorithms for model update face a difficulty: deleting (adding) transitions from (to) a Kripke model to satisfy a universal (an existential) subformula may dissatisfy some existential (universal) subformulas. Our method employs protected models to overcome this difficulty. We demonstrate our algorithm with a classical example of automatic synthesis described by Emerson and Clarke in 1982. From a dummy model, where the accessibility relation is the identity relation, our algorithm can efficiently generate a model to satisfy a specification of mutual exclusion in a variant of CTL. Such a variant extends CTL with an operator that limits the out-degree of states. We compare our method with a generate-and-test algorithm and outline a proof of soundness and completeness for our method. © 2011 Springer-Verlag.