On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems

Steen Vester

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

280 Downloads (Pure)

Abstract

We study the complexity of the model-checking problem for the branching-time logic CTL ∗  and the alternating-time temporal logics ATL/ATL ∗  in one-counter processes and one-counter games respectively. The complexity is determined for all three logics when integer weights are input in unary (non-succinct) and binary (succinct) as well as when the input formula is fixed and is a parameter. Further, we show that deciding the winner in one-counter games with LTL objectives is 2ExpSpacecomplete for both succinct and non-succinct games. We show that all the problems considered stay in the same complexity classes when we add quantitative constraints that can compare the current value of the counter with a constant.
Original languageEnglish
Title of host publicationProceedings of the 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
EditorsBernd Finkbeiner, Geguang Pu, Lijun Zhang
PublisherSpringer
Publication date2015
Pages361-377
ISBN (Print)978-3-319-24952-0
ISBN (Electronic)978-3-319-24953-7
DOIs
Publication statusPublished - 2015
Event13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015) - Shanghai, China
Duration: 12 Oct 201515 Oct 2015
Conference number: 13
http://atva2015.ios.ac.cn/

Conference

Conference13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015)
Number13
CountryChina
CityShanghai
Period12/10/201515/10/2015
Internet address
SeriesLecture Notes in Computer Science
Volume9364
ISSN0302-9743

Cite this

Vester, S. (2015). On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems. In B. Finkbeiner, G. Pu, & L. Zhang (Eds.), Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 (pp. 361-377). Springer. Lecture Notes in Computer Science, Vol.. 9364 https://doi.org/10.1007/978-3-319-24953-7_27