A tableau-based decision procedure for CTL*.
Saved in:
| Title: | A tableau-based decision procedure for CTL*. |
|---|---|
| Authors: | Reynolds, Mark1 mark@csse.uwa.edu.au |
| Source: | Formal Aspects of Computing. Nov2011, Vol. 23 Issue 6, p739-779. 41p. |
| Subjects: | Computer software termination, Computing platforms, Subroutines (Computer programs), Reasoning, Ring networks |
| Abstract: | We present a sound, complete and implementable tableau method for deciding satisfiability of formulas in the propositional version of computation tree logic CTL*. This is the first such tableau. CTL* is an exceptionally important temporal logic with applications from hardware design to agent reasoning, but there is no easily automated reasoning approach to CTL*. The tableau here is a traditional tree-shaped or top-down style tableau, and affords the possibility of reasonably quick decisions on the satisfiability of medium-sized formulas and construction of small models for them. A straightforward subroutine is given for determining when looping allows successful branch termination, but much needed further development is left as future work. In particular, a more general repetition prevention mechanism is needed to speed up the task of tableau construction. [ABSTRACT FROM AUTHOR] |
| Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 67056546 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: A tableau-based decision procedure for CTL*. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Reynolds%2C+Mark%22">Reynolds, Mark</searchLink><relatesTo>1</relatesTo><i> mark@csse.uwa.edu.au</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Formal+Aspects+of+Computing%22">Formal Aspects of Computing</searchLink>. Nov2011, Vol. 23 Issue 6, p739-779. 41p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Computer+software+termination%22">Computer software termination</searchLink><br /><searchLink fieldCode="DE" term="%22Computing+platforms%22">Computing platforms</searchLink><br /><searchLink fieldCode="DE" term="%22Subroutines+%28Computer+programs%29%22">Subroutines (Computer programs)</searchLink><br /><searchLink fieldCode="DE" term="%22Reasoning%22">Reasoning</searchLink><br /><searchLink fieldCode="DE" term="%22Ring+networks%22">Ring networks</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: We present a sound, complete and implementable tableau method for deciding satisfiability of formulas in the propositional version of computation tree logic CTL*. This is the first such tableau. CTL* is an exceptionally important temporal logic with applications from hardware design to agent reasoning, but there is no easily automated reasoning approach to CTL*. The tableau here is a traditional tree-shaped or top-down style tableau, and affords the possibility of reasonably quick decisions on the satisfiability of medium-sized formulas and construction of small models for them. A straightforward subroutine is given for determining when looping allows successful branch termination, but much needed further development is left as future work. In particular, a more general repetition prevention mechanism is needed to speed up the task of tableau construction. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=67056546 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s00165-011-0193-4 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 41 StartPage: 739 Subjects: – SubjectFull: Computer software termination Type: general – SubjectFull: Computing platforms Type: general – SubjectFull: Subroutines (Computer programs) Type: general – SubjectFull: Reasoning Type: general – SubjectFull: Ring networks Type: general Titles: – TitleFull: A tableau-based decision procedure for CTL*. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Reynolds, Mark IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 11 Text: Nov2011 Type: published Y: 2011 Identifiers: – Type: issn-print Value: 09345043 Numbering: – Type: volume Value: 23 – Type: issue Value: 6 Titles: – TitleFull: Formal Aspects of Computing Type: main |
| ResultId | 1 |
