First-order logic with reachability for infinite-state systems

被引：4

作者：

D'Osualdo, Emanuele ^{[1
]}

Meyer, Roland ^{[1
]}

Zetzsche, Georg ^{[2
,3
]}

机构：

[1] Univ Kaiserslautern, Kaiserslautern, Germany

[2] CNRS, LSV, Paris, France

[3] Univ Paris Saclay, ENS Cachan, Paris, France

来源：

PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016) | 2016年

关键词：

first-order logic; reachability; decidability; valence automata; graph monoids; automatic structures; GRAPHS;

D O I：

10.1145/2933575.2934552

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

First-order logic with the reachability predicate (FO[R]) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable). This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FO[R] is decidable for the resulting transition systems.

引用

页码：457 / 466

页数：10

共 50 条

[31] First-order intensional logic
Fitting, M
ANNALS OF PURE AND APPLIED LOGIC, 2004, 127 (1-3) : 171 - 193
[32] The First-Order Logic of Hyperproperties
Finkbeiner, Bernd
Zimmermann, Martin
34TH SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2017), 2017, 66
[33] COMPUTING WITH FIRST-ORDER LOGIC
ABITEBOUL, S
VIANU, V
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1995, 50 (02) : 309 - 335
[34] A verification methodology for infinite-state message passing systems
Sprenger, C
Worytkiewicz, K
FIRST ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2003, : 255 - 264
[35] On first-order corrections to the LSW theory I: Infinite systems
Hönig A.
Niethammer B.
Otto F.
Journal of Statistical Physics, 2005, 119 (1-2) : 61 - 122
[36] A First-order Logic with Frames
Murali, Adithya
Pena, Lucas
Loeding, Christof
Madhusudan, P.
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2023, 45 (02):
[37] Indistinguishability and first-order logic
Jordan, Skip
Zeugmann, Thomas
THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, PROCEEDINGS, 2008, 4978 : 94 - 104
[38] Theorem-proving anonymity of infinite-state systems
Kawabe, Yoshinobu
Mano, Ken
Sakurada, Hideki
Tsukada, Yasuyuki
INFORMATION PROCESSING LETTERS, 2007, 101 (01) : 46 - 51
[39] From separation logic to first-order logic
Calcagno, C
Gardner, P
Hague, M
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2005, 3441 : 395 - 409
[40] From First-Order Logic to Assertional Logic
Zhou, Yi
ARTIFICIAL GENERAL INTELLIGENCE: 10TH INTERNATIONAL CONFERENCE, AGI 2017, 2017, 10414 : 87 - 97

← 1 2 3 4 5 →