Paper Info
Title
Resolution-Based Model Construction for PLTL
Abstract
With tableaux-based reasoning approaches or model checking techniques for propositional linear-time temporal logics, PLTL, it is easily possible to construct counter examples for formulae that are not valid. In contrast, only the information that a formula is satisfiable is usually available in resolution-based inference systems. In this paper we present a resolution-based approach for constructing models for satisfiable PLTL formulae. Our approach is based on using the standard model construction for sets of propositional clauses saturated under ordered resolution in the different time points of a temporal model. The temporal model construction procedure is also designed in such a way that it can be easily implemented in existing theorem rovers for PLTL.
Year
DOI
Venue
2009
10.1109/TIME.2009.11
TIME
Keywords
Field
DocType
satisfiable pltl formula,resolution-based model construction,model checking technique,standard model construction,resolution-based inference system,tableaux-based reasoning approach,temporal model,resolution-based approach,propositional clause,propositional linear-time temporal logic,temporal model construction procedure,satisfiability,standard model,temporal logic,data mining,calculus,formal verification,resolution,logic,computational modeling,bismuth,manganese,model checking,silicon,computer science,construction industry
Model checking,Inference,Computer science,Algorithm,Theoretical computer science,Construction industry,Counterexample,Temporal logic
Conference
Citations 
PageRank 
References 
5
0.42
9
Authors
2
Name
Order
Citations
PageRank
Michel Ludwig11137.67
Ullrich Hustadt2100766.68