MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Labelled superposition for PLTL

Suda, Martin and Weidenbach, Christoph

January 2012, 42 pages.

Status: available - back from printing

This paper introduces a new decision procedure for PLTL based on labelled superposition. Its main idea is to treat temporal formulas as infi nite sets of purely propositional clauses over an extended signature. These in finite sets are then represented by finite sets of labelled propositional clauses. The new representation enables the replacement of the complex temporal resolution rule, suggested by existing resolution calculi for PLTL, by a fi ne-grained repetition check of fi nitely saturated labelled clause sets followed by a simple inference. The completeness argument is based on the standard model building idea from superposition. It inherently justifi es ordering restrictions, redundancy elimination and eff ective partial model building. The latter can be directly used to eff ectively generate counterexamples of non-valid PLTL conjectures out of saturated labelled clause sets in a straightforward way.

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Suda, Martin and Weidenbach, Christoph},
  TITLE = {Labelled superposition for {PLTL}},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2012-RG1-001},
  MONTH = {January},
  YEAR = {2012},
  ISSN = {0946-011X},