Taming past LTL and flat counter systems

被引：6

作者：

Demri, Stephane ^{[1
]}

Dhar, Amit Kumar ^{[2
]}

Sangnier, Arnaud ^{[2
]}

机构：

[1] CNRS, LSV, F-75700 Paris, France

[2] Univ Paris Diderot, LIAFA, Sorbonne Paris Cite, CNRS, Paris, France

来源：

INFORMATION AND COMPUTATION | 2015年 / 242卷

关键词：

Linear-time temporal logic; Stuttering; Model-checking; Counter system; Flatness; Complexity; System of equations; Small solution; Presburger arithmetic; TEMPORAL LOGIC; MODEL-CHECKING; AUTOMATA;

D O I：

10.1016/j.ic.2015.03.007

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that this problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. As far as past-time operators are concerned, their addition to LTL immediately leads to complications and hence an NP upper bound cannot be deduced by translating formulae into LTL and studying the problem only for this latter logic. We also provide other complexity results obtained by restricting further the class of flat counter systems. (C) 2015 Elsevier Inc. All rights reserved.

引用

页码：306 / 339

页数：34

共 39 条

[1] Baader Franz., 1991, Proceedings of the 12th International Joint Conference on Artificial Intelligence. Sydney, Australia, August 24-30, P452
[2] Boigelot B., 1998, THESIS U LIEGE
[3] BOUNDS ON POSITIVE INTEGRAL SOLUTIONS OF LINEAR DIOPHANTINE EQUATIONS
BOROSH, I
TREYBIG, LB
[J]. PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 1976, 55 (02) : 299 - 304
[4] Bozga M, 2014, LECT NOTES COMPUT SC, V8318, P242, DOI 10.1007/978-3-642-54013-4_14
[5] Bozga M, 2010, LECT NOTES COMPUT SC, V6174, P227, DOI 10.1007/978-3-642-14295-6_23
[6] Flat Parametric Counter Automata
Bozga, Marius
Iosif, Radu
Lakhnech, Yassine
[J]. FUNDAMENTA INFORMATICAE, 2009, 91 (02) : 275 - 303
[7] Clarke EM, 1999, MODEL CHECKING, P1
[8] Comon H, 1998, LECT NOTES COMPUT SC, V1427, P268, DOI 10.1007/BFb0028751
[9] Comon Hubert., 2000, Proceedings of CSL 2000, V1862 of LNCS, P262, DOI DOI 10.1007/3-540-44622-217
[10] Cooper D. C., 1972, Machine intelligence 7, P91

← 1 2 3 4 →