@misc(trppptool,
 url          = "http://www.csc.liv.ac.uk/~konev/software/trp++/",
)
@misc(paperwebpage,
 url          = "http://www.schuppan.de/viktor/qapl13/",
)
@inproceedings(RArmoniLFixAFlaisherOGrumbergNPitermanATiemeyerMVardi-CAV-2003,
 author       = "R. Armoni and L. Fix and A. Flaisher and O. Grumberg and N. Piterman and A. Tiemeyer and M. Vardi",
 year         = "2003",
 title        = "Enhanced Vacuity Detection in Linear Temporal Logic",
 editor       = "W. Hunt Jr. and F. Somenzi",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "2725",
 publisher    = "Springer",
 pages        = "368--380",
 doi          = "10.1007/978-3-540-45069-6\_35",
)
@article(AAwadRGoreZHouJThomsonMWeidlich-InformationSystems-2012,
 author       = "A. Awad and R. Gor{\'e} and Z. Hou and J. Thomson and M. Weidlich",
 year         = "2012",
 title        = "An iterative approach to synthesize business process templates from compliance rules",
 journal      = "Inf. Syst.",
 volume       = "37",
 number       = "8",
 pages        = "714--736",
 doi          = "10.1016/j.is.2012.05.001",
)
@inproceedings(RBakkerFDikkerFTempelmanPWognum-IJCAI-1993,
 author       = "R. Bakker and F. Dikker and F. Tempelman and P. Wognum",
 year         = "1993",
 title        = "Diagnosing and Solving Over-Determined Constraint Satisfaction Problems",
 booktitle    = "IJCAI",
 pages        = "276--281",
 url          = "http://ijcai.org/Past",
)
@inproceedings(IBeerSBenDavidHChocklerAOrniRTrefler-CAV-2009,
 author       = "I. Beer and S. Ben-David and H. Chockler and A. Orni and R. Trefler",
 year         = "2009",
 title        = "Explaining Counterexamples Using Causality",
 editor       = "A. Bouajjani and O. Maler",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "5643",
 publisher    = "Springer",
 pages        = "94--108",
 doi          = "10.1007/978-3-642-02658-4\_11",
)
@article(IBeerSBenDavidCEisnerYRodeh-FMSD-2001,
 author       = "I. Beer and S. Ben-David and C. Eisner and Y. Rodeh",
 year         = "2001",
 title        = "Efficient Detection of Vacuity in Temporal Model Checking",
 journal      = "FMSD",
 volume       = "18",
 number       = "2",
 pages        = "141--163",
 doi          = "10.1023/A:1008779610539",
)
@article(ABehdennaCDixonMFisher-IntelligentComputingAndCybernetics-2009,
 author       = "A. Behdenna and C. Dixon and M. Fisher",
 year         = "2009",
 title        = "Deductive Verification of Simple Foraging Robotic Behaviours",
 journal      = "Int. J. of Intelligent Comput. and Cybernetics",
 volume       = "2",
 number       = "4",
 pages        = "604--643",
 doi          = "10.1108/17563780911005818",
)
@misc(run,
 author       = "A. Biere and T. Jussila",
 title        = "Benchmark Tool Run",
 url          = "http://fmv.jku.at/run/",
)
@inproceedings(RBloemSGallerBJobstmannNPitermanAPnueliMWeiglhofer-COCV-2007,
 author       = "R. Bloem and S. Galler and B. Jobstmann and N. Piterman and A. Pnueli and M. Weiglhofer",
 year         = "2007",
 title        = "Specify, Compile, Run: Hardware from {PSL}",
 editor       = "S. Glesner and J. Knoop and R. Drechsler",
 booktitle    = "COCV",
 series       = "ENTCS",
 volume       = "190(4)",
 publisher    = "Elsevier",
 pages        = "3--16",
 doi          = "10.1016/j.entcs.2007.09.004",
)
@inproceedings(AChiappiniACimattiLMacchiORebolloMRoveriASusiSTonettaBVittorini-ICSE-2010,
 author       = "A. Chiappini and A. Cimatti and L. Macchi and O. Rebollo and M. Roveri and A. Susi and S. Tonetta and B. Vittorini",
 year         = "2010",
 title        = "Formalization and validation of a subset of the European Train Control System",
 editor       = "J. Kramer and J. Bishop and P. Devanbu and S. Uchitel",
 booktitle    = "ICSE (2)",
 publisher    = "ACM",
 pages        = "109--118",
 doi          = "10.1145/1810295.1810312",
)
@inproceedings(EClarkeMTalupurHVeithDWang-SAT-2003,
 author       = "E. Clarke and M. Talupur and H. Veith and D. Wang",
 year         = "2003",
 title        = "{SAT} Based Predicate Abstraction for Hardware Verification",
 editor       = "E. Giunchiglia and A. Tacchella",
 booktitle    = "SAT",
 series       = "LNCS",
 volume       = "2919",
 publisher    = "Springer",
 pages        = "78--92",
 doi          = "10.1007/978-3-540-24605-3\_7",
)
@phdthesis(CDixon-PhDThesis-1995,
 author       = "C. Dixon",
 year         = "1995",
 title        = "Strategies for Temporal Resolution",
 school       = "Department of Computer Science, University of Manchester",
 url          = "ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-95-12-1.ps.Z",
)
@inproceedings(CDixon-ICTL-1997,
 author       = "C. Dixon",
 year         = "1997",
 title        = "Using {Otter} for Temporal Resolution",
 editor       = "H. Barringer and M. Fisher and D. Gabbay and G. Gough",
 booktitle    = "ICTL",
 series       = "Applied Logic Series",
 publisher    = "Kluwer",
 pages        = "149--166",
)
@article(CDixon-AnnalsOfMathematicsAndArtificialIntelligence-1998,
 author       = "C. Dixon",
 year         = "1998",
 title        = "Temporal Resolution Using a Breadth-First Search Algorithm",
 journal      = "Ann. Math. Artif. Intell.",
 volume       = "22",
 number       = "1-2",
 pages        = "87--115",
 doi          = "10.1023/A:1018942108420",
)
@book(CEisnerDFisman-2006,
 author       = "C. Eisner and D. Fisman",
 year         = "2006",
 title        = "A Practical Introduction to {PSL}",
 publisher    = "Springer",
 doi          = "10.1007/978-0-387-36123-9",
)
@incollection(EEmerson-HandbookOfTheoreticalComputerScience-1990,
 author       = "E. Emerson",
 year         = "1990",
 title        = "Temporal and Modal Logic",
 editor       = "J. van Leeuwen",
 booktitle    = "Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)",
 publisher    = "Elsevier and MIT Press",
 pages        = "995--1072",
)
@inproceedings(MFisher-IJCAI-1991,
 author       = "M. Fisher",
 year         = "1991",
 title        = "A Resolution Method for Temporal Logic",
 booktitle    = "IJCAI",
 pages        = "99--104",
 url          = "http://ijcai.org/Past",
)
@article(MFisherCDixonMPeim-ACMTrComputationalLogic-2001,
 author       = "M. Fisher and C. Dixon and M. Peim",
 year         = "2001",
 title        = "Clausal temporal resolution",
 journal      = "ACM Trans. Comput. Log.",
 volume       = "2",
 number       = "1",
 pages        = "12--56",
 doi          = "10.1145/371282.371311",
)
@inproceedings(PGawrychowski-CIAA-2011,
 author       = "P. Gawrychowski",
 year         = "2011",
 title        = "{Chrobak} Normal Form Revisited, with Applications",
 editor       = "B. Bouchou-Markhoff and P. Caron and J. Champarnaud and D. Maurel",
 booktitle    = "CIAA",
 series       = "LNCS",
 volume       = "6807",
 publisher    = "Springer",
 pages        = "142--153",
 doi          = "10.1007/978-3-642-22256-6\_14",
)
@inproceedings(FHantryMHacid-FLACOS-2011,
 author       = "F. Hantry and M. Hacid",
 year         = "2011",
 title        = "Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages",
 editor       = "E. Pimentel and V. Valero",
 booktitle    = "FLACOS",
 series       = "EPTCS",
 volume       = "68",
 pages        = "39--53",
 doi          = "10.4204/EPTCS.68.5",
)
@phdthesis(AHarding-PhDThesis-2005,
 author       = "A. Harding",
 year         = "2005",
 title        = "Symbolic Strategy Synthesis For Games With {LTL} Winning Conditions",
 school       = "University of Birmingham",
)
@book(JHopcroftJUllman-1979,
 author       = "J. Hopcroft and J. Ullman",
 year         = "1979",
 title        = "Introduction to Automata Theory, Languages and Computation",
 publisher    = "Addison-Wesley",
)
@inproceedings(UHustadtBKonev-CADE-2003,
 author       = "U. Hustadt and B. Konev",
 year         = "2003",
 title        = "{TRP++ 2.0}: A Temporal Resolution Prover",
 editor       = "F. Baader",
 booktitle    = "CADE",
 series       = "LNCS",
 volume       = "2741",
 publisher    = "Springer",
 pages        = "274--278",
 doi          = "10.1007/978-3-540-45085-6\_21",
)
@incollection(UHustadtBKonev-CollegiumLogicum-2004,
 author       = "U. Hustadt and B. Konev",
 year         = "2004",
 title        = "{TRP++}: A temporal resolution prover",
 editor       = "M. Baaz and J. Makowsky and A. Voronkov",
 booktitle    = "Collegium Logicum",
 volume       = "8",
 publisher    = "Kurt G{\"o}del Society",
 pages        = "65--79",
)
@inproceedings(UHustadtRSchmidt-KR-2002,
 author       = "U. Hustadt and R. A. Schmidt",
 year         = "2002",
 title        = "Scientific Benchmarking with Temporal Logic Decision Procedures",
 editor       = "D. Fensel and F. Giunchiglia and D. McGuinness and M. Williams",
 booktitle    = "KR",
 publisher    = "Morgan Kaufmann",
 pages        = "533--546",
)
@inproceedings(TJussilaCSinzABiere-SAT-2006,
 author       = "T. Jussila and C. Sinz and A. Biere",
 year         = "2006",
 title        = "Extended Resolution Proofs for Symbolic SAT Solving with Quantification",
 editor       = "A. Biere and C. Gomes",
 booktitle    = "SAT",
 series       = "LNCS",
 volume       = "4121",
 publisher    = "Springer",
 pages        = "54--60",
 doi          = "10.1007/11814948\_8",
)
@article(RParikh-JACM-1966,
 author       = "R. Parikh",
 year         = "1966",
 title        = "On Context-Free Languages",
 journal      = "J. ACM",
 volume       = "13",
 number       = "4",
 pages        = "570--581",
 doi          = "10.1145/321356.321364",
)
@inproceedings(MPesicWVanDerAalst-BPM-2006,
 author       = "M. Pesic and W. van der Aalst",
 year         = "2006",
 title        = "A Declarative Approach for Flexible Business Processes Management",
 editor       = "J. Eder and S. Dustdar",
 booktitle    = "Business Process Management Workshops",
 series       = "LNCS",
 volume       = "4103",
 publisher    = "Springer",
 pages        = "169--180",
 doi          = "10.1007/11837862\_18",
)
@inproceedings(IPillSSempriniRCavadaMRoveriRBloemACimatti-DAC-2006,
 author       = "I. Pill and S. Semprini and R. Cavada and M. Roveri and R. Bloem and A. Cimatti",
 year         = "2006",
 title        = "Formal analysis of hardware requirements",
 editor       = "E. Sentovich",
 booktitle    = "DAC",
 publisher    = "ACM",
 pages        = "821--826",
 doi          = "10.1145/1146909.1147119",
)
@inproceedings(KRaviFSomenzi-TACAS-2004,
 author       = "K. Ravi and F. Somenzi",
 year         = "2004",
 title        = "Minimal Assignments for Bounded Model Checking",
 editor       = "K. Jensen and A. Podelski",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "2988",
 publisher    = "Springer",
 pages        = "31--45",
 doi          = "10.1007/978-3-540-24730-2\_3",
)
@article(KRozierMVardi-STTT-2010,
 author       = "K. Rozier and M. Vardi",
 year         = "2010",
 title        = "{LTL} satisfiability checking",
 journal      = "STTT",
 volume       = "12",
 number       = "2",
 pages        = "123--137",
 doi          = "10.1007/s10009-010-0140-3",
)
@article(ZSawa-FundamentaInformaticae-2013,
 author       = "Z. Sawa",
 year         = "2013",
 title        = "Efficient Construction of Semilinear Representations of Languages Accepted by Unary Nondeterministic Finite Automata",
 journal      = "Fundam. Inform.",
 volume       = "123",
 number       = "1",
 pages        = "97--106",
 doi          = "10.3233/FI-2013-802",
)
@misc(fullversion,
 author       = "V. Schuppan",
 year         = "2012",
 title        = "Enhancing Unsatisfiable Cores for {LTL} with Information on Temporal Relevance (full version)",
 url          = "http://www.schuppan.de/viktor/qapl13/VSchuppan-QAPL-2013-full.pdf",
)
@misc(VSchuppan-NFM-2013-full-arXiv,
 author       = "V. Schuppan",
 year         = "2012",
 title        = "Extracting Unsatisfiable Cores for {LTL} via Temporal Resolution",
 note         = "Available at \href {http://arxiv.org/abs/1212.3884v1}{{\tt arXiv:1212.3884v1 [cs.LO]}}",
)
@article(VSchuppan-SCP-2012,
 author       = "V. Schuppan",
 year         = "2012",
 title        = "Towards a notion of unsatisfiable and unrealizable cores for {LTL}",
 journal      = "Sci. Comput. Program.",
 volume       = "77",
 number       = "7-8",
 pages        = "908--939",
 doi          = "10.1016/j.scico.2010.11.004",
)
@inproceedings(VSchuppanLDarmawan-ATVA-2011,
 author       = "V. Schuppan and L. Darmawan",
 year         = "2011",
 title        = "Evaluating {LTL} Satisfiability Solvers",
 editor       = "T. Bultan and P. Hsiung",
 booktitle    = "ATVA",
 series       = "LNCS",
 volume       = "6996",
 publisher    = "Springer",
 pages        = "397--413",
 doi          = "10.1007/978-3-642-24372-1\_28",
)
@article(JSimmondsJDaviesAGurfinkelMChechik-STTT-2010,
 author       = "J. Simmonds and J. Davies and A. Gurfinkel and M. Chechik",
 year         = "2010",
 title        = "Exploiting resolution proofs to speed up LTL vacuity detection for BMC",
 journal      = "STTT",
 volume       = "12",
 number       = "5",
 pages        = "319--335",
 doi          = "10.1007/s10009-009-0134-1",
)
@inproceedings(MDeWulfLDoyenNMaquetJRaskin-TACAS-2008,
 author       = "M. De Wulf and L. Doyen and N. Maquet and J. Raskin",
 year         = "2008",
 title        = "Antichains: Alternative Algorithms for {LTL} Satisfiability and Model-Checking",
 editor       = "C. Ramakrishnan and J. Rehof",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "4963",
 publisher    = "Springer",
 pages        = "63--77",
 doi          = "10.1007/978-3-540-78800-3\_6",
)