A Step Up in Expressiveness of Decidable Fixpoint Logics

Michael Benedikt; Pierre Bourhis; Michael Vanden Boom

doi:10.1145/2933575.2933592

A Step Up in Expressiveness of Decidable Fixpoint Logics

Michael Benedikt
, Pierre Bourhis
, Michael Vanden Boom

University of Oxford
Université de Lille

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Guardedness restrictions are one of the principal means to obtain decidable logics - - operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.

Original language	English
Title of host publication	Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	817-826
Number of pages	10
ISBN (Electronic)	9781450343916
DOIs	https://doi.org/10.1145/2933575.2933592
Publication status	Published - 5 Jul 2016
Externally published	Yes
Event	31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States Duration: 5 Jul 2016 → 8 Jul 2016

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Volume	05-08-July-2016
ISSN (Print)	1043-6871

Conference

Conference	31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
Country/Territory	United States
City	New York
Period	5/07/16 → 8/07/16

Access to Document

10.1145/2933575.2933592

Cite this

Benedikt, M., Bourhis, P., & Boom, M. V. (2016). A Step Up in Expressiveness of Decidable Fixpoint Logics. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016 (pp. 817-826). (Proceedings - Symposium on Logic in Computer Science; Vol. 05-08-July-2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/2933575.2933592

@inproceedings{7282744135554fd5832e49c5c90603bd,

title = "A Step Up in Expressiveness of Decidable Fixpoint Logics",

abstract = "Guardedness restrictions are one of the principal means to obtain decidable logics - - operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.",

author = "Michael Benedikt and Pierre Bourhis and Boom, \{Michael Vanden\}",

note = "Publisher Copyright: {\textcopyright} 2016 ACM.; 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 ; Conference date: 05-07-2016 Through 08-07-2016",

year = "2016",

month = jul,

day = "5",

doi = "10.1145/2933575.2933592",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "817--826",

booktitle = "Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016",

}

Benedikt, M, Bourhis, P & Boom, MV 2016, A Step Up in Expressiveness of Decidable Fixpoint Logics. in Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016. Proceedings - Symposium on Logic in Computer Science, vol. 05-08-July-2016, Institute of Electrical and Electronics Engineers Inc., pp. 817-826, 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, United States, 5/07/16. https://doi.org/10.1145/2933575.2933592

A Step Up in Expressiveness of Decidable Fixpoint Logics. / Benedikt, Michael; Bourhis, Pierre; Boom, Michael Vanden.
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016. Institute of Electrical and Electronics Engineers Inc., 2016. p. 817-826 (Proceedings - Symposium on Logic in Computer Science; Vol. 05-08-July-2016).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A Step Up in Expressiveness of Decidable Fixpoint Logics

AU - Benedikt, Michael

AU - Bourhis, Pierre

AU - Boom, Michael Vanden

PY - 2016/7/5

Y1 - 2016/7/5

N2 - Guardedness restrictions are one of the principal means to obtain decidable logics - - operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.

AB - Guardedness restrictions are one of the principal means to obtain decidable logics - - operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.

U2 - 10.1145/2933575.2933592

DO - 10.1145/2933575.2933592

M3 - Conference contribution

AN - SCOPUS:84994683519

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 817

EP - 826

BT - Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016

Y2 - 5 July 2016 through 8 July 2016

ER -

A Step Up in Expressiveness of Decidable Fixpoint Logics

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this