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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence 112(1-2), 57–104 (1999)
Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. In: Priami, C., Plotkin, G.D. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 68–94. Springer, Heidelberg (2006)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 241–266 (1982)
Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. JCSS 30(1), 1–24 (1985)
Zhang, Y., Ding, Y.: CTL model update for system modifications. Journal of Artificial Intelligence Research 31, 113–155 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carrillo, M., Rosenblueth, D.A. (2011). Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)