CTL update of Kripke models through protections

DOI10.1016/J.ARTINT.2014.02.005MaRDI QIDQ2453698zbMATH OpenOpenAlexFDO

Authors Miguel Carrillo, David A. Rosenblueth

Publication date 10 June 2014

Published in Artificial Intelligence (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.1016/j.artint.2014.02.005

zbMATH Keywords

automatic synthesisCTL model updatemodel checking

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Nondeterministic update of CTL models by preserving satisfaction through protections
• A method for CTL model update, representing Kripke structures as ``table systems
• CTL model update for system modifications
• AI 2005: Advances in Artificial Intelligence
• Minimisation of models satisfying CTL formulas

Cites work

• A method for CTL model update, representing Kripke structures as ``table systems
• CTL model update for system modifications
• Decision procedures and expressiveness in the temporal logic of branching time
• Enhancing model checking in verification by AI techniques
• Finding and fixing faults
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• Modeling and querying biomolecular interaction networks
• NASA formal methods. 4th international symposium, NFM 2012, Norfolk, VA, USA, April 3--5, 2012. Proceedings
• Nondeterministic update of CTL models by preserving satisfaction through protections
• On ACTL formulas having linear counterexamples
• Transactions on Computational Systems Biology VI
• Updating action domain descriptions
• Using branching time temporal logic to synthesize synchronization skeletons

Cited in

(6)

• Two AGM-style characterizations of model repair
• Foundations of tree-like local model updates
• Nondeterministic update of CTL models by preserving satisfaction through protections
• A method for CTL model update, representing Kripke structures as ``table systems
• AI 2005: Advances in Artificial Intelligence
• Minimisation of models satisfying CTL formulas

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: CTL update of Kripke models through protections

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2453698)