Advertisement
Published in:
2011 | OriginalPaper | Chapter
Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections
Authors : Miguel Carrillo, David A. Rosenblueth
Published in: Automated Technology for Verification and Analysis
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
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.