Skip navigation
Skip navigation

Blocking and Other Enhancements for Bottom-Up Model Generation Methods

Baumgartner, Peter; Schmidt, Renate A.

Description

Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several ways of enhancing the paradigm of bottom-up model generation, with the two main contributions being a new range-restriction transformation and generalized blocking techniques. The range-restriction transformation refines existing transformations to...[Show more]

dc.contributor.authorBaumgartner, Peter
dc.contributor.authorSchmidt, Renate A.
dc.date.accessioned2019-03-04T00:37:41Z
dc.date.available2019-03-04T00:37:41Z
dc.identifier.issn0168-7433
dc.identifier.urihttp://hdl.handle.net/1885/156809
dc.description.abstractModel generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several ways of enhancing the paradigm of bottom-up model generation, with the two main contributions being a new range-restriction transformation and generalized blocking techniques. The range-restriction transformation refines existing transformations to range-restricted clauses by carefully limiting the creation of domain terms. The blocking techniques are based on simple transformations of the input set together with standard equality reasoning and redundancy elimination techniques, and allow for finding small, finite models. All possible combinations of the introduced techniques and a classical range-restriction technique were tested on the clausal problems of the TPTP Version 6.0.0 with an implementation based on the SPASS theorem prover using a hyperresolution-like refinement. Unrestricted domain blocking gave best results for satisfiable problems, showing that it is an indispensable technique for bottom-up model generation methods, that yields good results in combination with both new and classical range-restricting transformations. Limiting the creation of terms during the inference process by using the new range-restricting transformation has paid off, especially when using it together with a shifting transformation. The experimental results also show that classical range restriction with unrestricted blocking provides a useful complementary method. Overall, the results show bottom-up model generation methods are good for disproving theorems and generating models for satisfiable problems, but less efficient for unsatisfiable problems.
dc.description.sponsorshipFinancial support through research Grants EP/F068530/1 and EP/H043748/1 of the UK Engineering and Physical Sciences Research Council (EPSRC) is gratefully acknowledged.
dc.format55 pages
dc.format.mimetypeapplication/pdf
dc.language.isoen_AU
dc.publisherSpringer Netherlands
dc.rights© The Author(s) 2019. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
dc.sourceJournal of Automated Reasoning
dc.subjectAutomated reasoning
dc.subjectModel generation
dc.subjectBlocking
dc.subjectFirst-order logic
dc.subjectBernays–Schönfinkel class
dc.titleBlocking and Other Enhancements for Bottom-Up Model Generation Methods
dc.typeJournal article
local.description.notesImported from Springer Nature
dcterms.dateAccepted2019-02-05
dc.date.issued2019-03-01
local.publisher.urlhttps://link.springer.com/
local.type.statusPublished Version
local.contributor.affiliationBaumgartner, Peter, CSIRO/Data61 and The Australian National University
local.contributor.affiliationSchmidt, Renate A., School of Computer Science, The University of Manchester
local.identifier.essn1573-0670
local.bibliographicCitation.startpage1
local.bibliographicCitation.lastpage55
local.identifier.doi10.1007/s10817-019-09515-1
dc.date.updated2019-03-03T09:06:28Z
dcterms.accessRightsOpen Access
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01 Portal P and Veraar M Stochastic maximal regularity 2019.pdf3.35 MBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator