Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Labelled superposition for PLTL

Suda, Martin and Weidenbach, Christoph

MPI-I-2012-RG1-001. January 2012, 42 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2012-RG1-001.pdf MPI-I-2012-RG1-001.pdf 420 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
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},