Equivalence between model-checking flat counter systems and Presburger arithmetic.
Saved in:
| Title: | Equivalence between model-checking flat counter systems and Presburger arithmetic. |
|---|---|
| Authors: | Demri, Stéphane1, Dhar, Amit Kumar2 amitdhar@iiita.ac.in, Sangnier, Arnaud3 |
| Source: | Theoretical Computer Science. Jul2018, Vol. 735, p2-23. 22p. |
| Subjects: | Counters (Computer science), Digital counters, Constraint satisfaction, Arithmetic, Information technology |
| Abstract: | We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment. [ABSTRACT FROM AUTHOR] |
| Copyright of Theoretical Computer Science is the property of Elsevier B.V. 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: 129922693 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Equivalence between model-checking flat counter systems and Presburger arithmetic. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Demri%2C+Stéphane%22">Demri, Stéphane</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Dhar%2C+Amit+Kumar%22">Dhar, Amit Kumar</searchLink><relatesTo>2</relatesTo><i> amitdhar@iiita.ac.in</i><br /><searchLink fieldCode="AR" term="%22Sangnier%2C+Arnaud%22">Sangnier, Arnaud</searchLink><relatesTo>3</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Theoretical+Computer+Science%22">Theoretical Computer Science</searchLink>. Jul2018, Vol. 735, p2-23. 22p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Counters+%28Computer+science%29%22">Counters (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Digital+counters%22">Digital counters</searchLink><br /><searchLink fieldCode="DE" term="%22Constraint+satisfaction%22">Constraint satisfaction</searchLink><br /><searchLink fieldCode="DE" term="%22Arithmetic%22">Arithmetic</searchLink><br /><searchLink fieldCode="DE" term="%22Information+technology%22">Information technology</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: We show that model-checking flat counter systems with the branching-time temporal logic CTL* extended with arithmetical constraints on counter values has the same worst-case complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with strong restrictions: the logical language uses only the temporal operator EF and no arithmetical constraints, and the guards on the transitions are made of linear constraints. This work complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL, for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Theoretical Computer Science is the property of Elsevier B.V. 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=129922693 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1016/j.tcs.2017.07.007 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 22 StartPage: 2 Subjects: – SubjectFull: Counters (Computer science) Type: general – SubjectFull: Digital counters Type: general – SubjectFull: Constraint satisfaction Type: general – SubjectFull: Arithmetic Type: general – SubjectFull: Information technology Type: general Titles: – TitleFull: Equivalence between model-checking flat counter systems and Presburger arithmetic. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Demri, Stéphane – PersonEntity: Name: NameFull: Dhar, Amit Kumar – PersonEntity: Name: NameFull: Sangnier, Arnaud IsPartOfRelationships: – BibEntity: Dates: – D: 29 M: 07 Text: Jul2018 Type: published Y: 2018 Identifiers: – Type: issn-print Value: 03043975 Numbering: – Type: volume Value: 735 Titles: – TitleFull: Theoretical Computer Science Type: main |
| ResultId | 1 |
