{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article14592","name":"Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment","abstract":"We define a class of Separation Logic [Ishtiaq and O'Hearn, 2001; J.C. Reynolds, 2002] formulae, whose entailment problem given formulae \u03d5, \u03c8\u2081, \u2026, \u03c8_n, is every model of \u03d5 a model of some \u03c8_i? is 2-EXPTIME-complete. The formulae in this class are existentially quantified separating conjunctions involving predicate atoms, interpreted by the least sets of store-heap structures that satisfy a set of inductive rules, which is also part of the input to the entailment problem. Previous work [Iosif et al., 2013; Jens Katelaan et al., 2019; Jens Pagel and Florian Zuleger, 2020] consider established sets of rules, meaning that every existentially quantified variable in a rule must eventually be bound to an allocated location, i.e. from the domain of the heap. In particular, this guarantees that each structure has treewidth bounded by the size of the largest rule in the set. In contrast, here we show that establishment, although sufficient for decidability (alongside two other natural conditions), is not necessary, by providing a condition, called equational restrictedness, which applies syntactically to (dis-)equalities. The entailment problem is more general in this case, because equationally restricted rules define richer classes of structures, of unbounded treewidth. In this paper we show that \r\n(1) every established set of rules can be converted into an equationally restricted one and \r\n(2) the entailment problem is 2-EXPTIME-complete in the latter case, thus matching the complexity of entailments for established sets of rules [Jens Katelaan et al., 2019; Jens Pagel and Florian Zuleger, 2020].","keywords":["Separation logic","Induction definitions","Inductive theorem proving","Entailments","Complexity"],"author":[{"@type":"Person","name":"Echenim, Mnacho","givenName":"Mnacho","familyName":"Echenim","affiliation":"Universit\u00e9 Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France"},{"@type":"Person","name":"Iosif, Radu","givenName":"Radu","familyName":"Iosif","affiliation":"Universit\u00e9 Grenoble Alpes, CNRS, VERIMAG, F-38000 Grenoble, France"},{"@type":"Person","name":"Peltier, Nicolas","givenName":"Nicolas","familyName":"Peltier","affiliation":"Universit\u00e9 Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France"}],"position":20,"pageStart":"20:1","pageEnd":"20:18","dateCreated":"2021-01-13","datePublished":"2021-01-13","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Echenim, Mnacho","givenName":"Mnacho","familyName":"Echenim","affiliation":"Universit\u00e9 Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France"},{"@type":"Person","name":"Iosif, Radu","givenName":"Radu","familyName":"Iosif","affiliation":"Universit\u00e9 Grenoble Alpes, CNRS, VERIMAG, F-38000 Grenoble, France"},{"@type":"Person","name":"Peltier, Nicolas","givenName":"Nicolas","familyName":"Peltier","affiliation":"Universit\u00e9 Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France"}],"copyrightYear":"2021","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.20","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","citation":["https:\/\/easychair.org\/publications\/paper\/DdNg","http:\/\/arxiv.org\/abs\/2002.01202","https:\/\/easychair.org\/publications\/paper\/VTGk"],"isPartOf":{"@type":"PublicationVolume","@id":"#volume6386","volumeNumber":183,"name":"29th EACSL Annual Conference on Computer Science Logic (CSL 2021)","dateCreated":"2021-01-13","datePublished":"2021-01-13","editor":[{"@type":"Person","name":"Baier, Christel","givenName":"Christel","familyName":"Baier","email":"mailto:christel.baier@tu-dresden.de","sameAs":"https:\/\/orcid.org\/0000-0002-5321-9343","affiliation":"Technische Universit\u00e4t Dresden, Germany"},{"@type":"Person","name":"Goubault-Larrecq, Jean","givenName":"Jean","familyName":"Goubault-Larrecq","email":"mailto:goubault@lsv.fr","sameAs":"https:\/\/orcid.org\/0000-0001-5879-3304","affiliation":"ENS Paris-Saclay, France"}],"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article14592","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6386"}}}