[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

A resolution calculus for the branching-time temporal logic CTL

Published: 06 March 2014 Publication History

Abstract

The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the translation of formulae to a normal form and the application of a number of resolution rules. We use indices in the normal form to represent particular paths and the application of the resolution rules is restricted dependent on an ordering and selection function to reduce the search space. We show that the translation preserves satisfiability, the calculus is sound, complete, and terminating, and consider the complexity of the calculus.

Supplementary Material

a10-zhang-apndx.pdf (zhang.zip)
Supplemental movie, appendix, image and software files for, A resolution calculus for the branching-time temporal logic CTL

References

[1]
P. Abate and R. Goré. 2003. The Tableaux Work Bench. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'03). Lecture Notes in Computer Science, vol. 2796, Springer-Verlag, Berlin, 230--236.
[2]
P. Abate, R. Goré, and F. Widmann. 2007. One-pass Tableaux for computation tree logic. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07). Lecture Notes in Computer Science, vol. 4790, Springer-Verlag, Berlin, 32--46.
[3]
L. Afanasiev, M. Franceschet, M. Marx, and M. De Rijke. 2004. CTL model checking for processing simple XPath queries. In Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME'04). 117--124.
[4]
P. C. Attie. 2003. On the implementation complexity of specifications of concurrent programs. In Proceedings of the 17th International Conference on Distributed Computing (DISC'03). Lecture Notes in Computer Science, vol. 2848, Springer-Verlag, Berlin, 151--165.
[5]
L. Bachmair and H. Ganzinger. 2001. Resolution theorem proving. In Handbook of Automated Reasoning. vol. 1, Elsevier, 19--99.
[6]
A. Basso and A. Bolotov. 2007. Towards GCM re-configuration extending specification by norms. In Making Grids Work: Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments. 17--29.
[7]
M. Ben-Ari, Z. Manna, and A. Pnueli. 1981. The temporal logic of branching time. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'81). ACM Press, 164--176.
[8]
A. Bolotov. 2000. Clausal resolution for branching-time temporal logic. Ph.D. dissertation, Manchester Metropolitan University.
[9]
A. Bolotov and C. Dixon. 2000. Resolution for branching time temporal logics: Applying the temporal resolution rule. In Proceedings of the 7th International Workshop on Temporal Representation and Reasoning (TIME'00). 163--172.
[10]
A. Bolotov and M. Fisher. 1999. A clausal resolution method for CTL branching-time temporal logic. J. Exp. Theor. Artif. Intell. 11, 1, 77--93.
[11]
A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. NuSMV 2: An OpenSource tool for symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02). Lecture Notes in Computer Science, vol. 2404, Springer-Verlag, Berlin, 359--364.
[12]
E. M. Clarke and E. A. Emerson. 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science, vol. 131, Springer-Verlag, Berlin, 52--71.
[13]
E. M. Clarke, E. A. Emerson, and A. P. Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2, 244--263.
[14]
E. M. Clarke, O. Grumberg, and D. A. Peled. 2000. Model Checking. MIT Press.
[15]
C. Dixon. 1998. Temporal resolution using a breadth-first search algorithm. Ann. Math. Artif. Intell. 22, 1--2, 87--115.
[16]
C. Dixon, M. Fisher, and A. Bolotov. 2002. Clausal resolution in a logic of rational agency. Artif. Intell. 139, 1, 47--89.
[17]
E. A. Emerson. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, Elsevier, Chapter 16, 996--1072.
[18]
E. A. Emerson and J. Y. Halpern. 1982. Decision procedures and expressiveness in the temporal logic of branching time. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC'82). ACM Press, 169--180.
[19]
E. A. Emerson and J. Y. Halpern. 1985. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30, 1, 1--24.
[20]
E. A. Emerson and J. Y. Halpern. 1986. “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. J. ACM 33, 1, 151--178.
[21]
E. A. Emerson and C. S. Jutla. 1988. Complexity of tree automata and modal logics of programs. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science (FOCS'88). 328--337.
[22]
M. C. Fernández Gago. 2004. Efficient control of temporal reasoning. Ph.D. dissertation, University of Liverpool.
[23]
M. Fisher, C. Dixon, and M. Peim. 2001. Clausal temporal resolution. ACM Trans. Comput. Logic 2, 1, 12--56.
[24]
T. French, J. Mccabe-Dansted, and M. Reynolds. 2007. A temporal logic of robustness. In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07). Lecture Notes in Computer Science, vol. 4720, Springer-Verlag, Berlin, 193--205.
[25]
O. Friedmann and M. Lange. 2009. A solver for modal fixpoint logics. Electron. Notes Theor. Comput. Sci. 262, 99--111.
[26]
R. Goré, J. Thomson, and F. Widmann. 2011. An experimental comparison of theorem provers for CTL. In Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME'11). 49--56.
[27]
M. Huth and M. Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
[28]
Z. Manna and A. Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer.
[29]
W. Marrero. 2005. Using BDDs to decide CTL. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05). Lecture Notes in Computer Science, vol. 3440, Springer-Verlag, Berlin, 222--236.
[30]
J. McCabe-Dansted. 2008. A tableau for RoBCTL. In Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA'08). Lecture Notes in Computer Science, vol. 5293, Springer-Verlag, Berlin, 298--310.
[31]
J. McCabe-Dansted and C. Dixon. 2010. CTL-like fragments of a temporal logic of robustness. In Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10). 11--18.
[32]
V. R. Pratt. 1980. A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20, 2, 231--254.
[33]
M. Reynolds. 2011. A tableau-based decision procedure for CTL*. Formal Aspects Comput. 23, 6, 1--41.
[34]
J. A. Robinson. 1965. Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227--234. S. Schwendimann. 1998. A new one-pass tableau calculus for PLTL. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98). Lecture Notes in Computer Science, vol. 1397, Springer-Verlag, Berlin, 277--291.
[35]
M. Vardi and L. Stockmeyer. 1985. Improved upper and lower bounds for modal logics of programs. In Proceedings of the 17th Annual ACM Symposium on Theory of Computing (STOC'85). ACM Press, 240--251.
[36]
M. Y. Vardi and P. Wolper. 1986. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32, 2, 183--221.
[37]
C. Weidenbach, R. A. Schmidt, T. Hillenbrand, R. Rusev, and D. Topic. 2007. System description: Spass version 3.0. In Proceedings of the 21st International Conference on Automated Deduction (CADE-21). Lecture Notes in Computer Science, vol. 4603, Springer-Verlag, Berlin, 514--520.
[38]
L. Zhang. 2010. Clausal reasoning for branching-time logics. Ph.D. dissertation, University of Liverpool.
[39]
L. Zhang, U. Hustadt, and C. Dixon. 2009a. A refined resolution calculus for CTL. In Proceedings of the 22nd International Conference on Automated Deduction (CADE-22). Lecture Notes in Computer Science, vol. 5663, Springer-Verlag, Berlin, 245--260.
[40]
L. Zhang, U. Hustadt, and C. Dixon. 2009b. CTL-RP: A computational tree logic resolution prover. AI Commun. 23, 2--3, 111--136.

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic
ACM Transactions on Computational Logic  Volume 15, Issue 1
February 2014
279 pages
ISSN:1529-3785
EISSN:1557-945X
DOI:10.1145/2590829
Issue’s Table of Contents
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 March 2014
Accepted: 01 September 2013
Revised: 01 May 2013
Received: 01 October 2012
Published in TOCL Volume 15, Issue 1

Check for updates

Author Tags

  1. Temporal logic
  2. automated theorem proving
  3. resolution

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)71
  • Downloads (Last 6 weeks)11
Reflects downloads up to 11 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2022)Computing Sufficient and Necessary Conditions in CTL: A Forgetting ApproachInformation Sciences10.1016/j.ins.2022.10.124616(474-504)Online publication date: Nov-2022
  • (2021)Theorem Proving Using Clausal Resolution: From Past to PresentReachability Problems10.1007/978-3-030-89716-1_2(19-27)Online publication date: 25-Oct-2021
  • (2020)Security-Minded Verification of Space Systems2020 IEEE Aerospace Conference10.1109/AERO47225.2020.9172563(1-13)Online publication date: Mar-2020
  • (2020)Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via TranslationsJournal of Automated Reasoning10.1007/s10817-020-09541-464:8(1553-1610)Online publication date: 19-Feb-2020
  • (2019)Sublogics of a branching time logic of robustnessInformation and Computation10.1016/j.ic.2019.02.003Online publication date: Mar-2019
  • (2018)Temporal logic of common knowledge and its resolution-based proof methodJournal of Intelligent & Fuzzy Systems10.3233/JIFS-17988(1-16)Online publication date: 21-Aug-2018
  • (2017)To be fair, use bundlesAnnals of Mathematics and Artificial Intelligence10.1007/s10472-017-9546-x80:3-4(317-364)Online publication date: 1-Aug-2017
  • (2015)Declarative Programming with Temporal Constraints, in the Language CGThe Scientific World Journal10.1155/2015/5408542015:1Online publication date: 29-Mar-2015
  • (2015)Global Caching for the Flat Coalgebraic µ-CalculusProceedings of the 2015 22nd International Symposium on Temporal Representation and Reasoning (TIME)10.1109/TIME.2015.15(121-130)Online publication date: 23-Sep-2015
  • (2015)Ordered Resolution for Coalition LogicProceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - Volume 932310.1007/978-3-319-24312-2_12(169-184)Online publication date: 21-Sep-2015

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media