================================================================================ 0. CONTENTS ================================================================================ 1. PURPOSE 2. INSTALLATION 3. EXAMPLES 4. LEARNING MORE 5. GENEALOGY 6. VERSIONS 7. ACKNOWLEDGMENTS 8. CONTACT 9. COPYRIGHT AND LICENSES 10. REFERENCES ================================================================================ 1. PURPOSE ================================================================================ These are the sources of TRP++UC, a satisfiability solver for Linear Temporal Logic (LTL) that can extract fine-grained unsatisfiable cores for LTL. The basic notion of unsatisfiable cores used in TRP++UC is one of replacing positive-polarity occurrences of subformulas with TRUE and negative-polarity occurrences of subformulas with FALSE. This notion is refined by (i) partitioning occurrences of a proposition into different groups according to how they interact in a proof of unsatisfiability, or (ii) annotating occurrences of subformulas with the sets of time points at which they are used in a proof of unsatisfiability. TRP++UC extends TRP++, which is based on temporal resolution. For download and for updated versions see [trp++uc]. ================================================================================ 2. INSTALLATION ================================================================================ To compile do a "make release" from the directory this README is found in. Then call "./bin/trp++uc -h" (or "./bin/trp++ -h" for the version used to obtain the experimental results in [Sch13a] and [Sch13b]) to see command line options. Building TRP++UC essentially requires a standard environment for developing C++ software: something along the lines of "make", "g++", "bison", and "flex". The Boost C++ libraries are also needed. "gengetopt" is used to handle command line options. I successfully compiled the current version of TRP++UC on a number of current Linux distributions including: Arch Linux; CentOS 7.2.1511; Fedora 22, 23; Gentoo Linux 20140826 (Live DVD); Linux Mint 17.3; Mageia 5; Manjaro Linux 15.12; openSUSE 13.2, 42.1; Oracle Linux 7.2; Ubuntu 14.04, 15.04, 15.10, 16.04 (daily build). Versions that were used to obtain experimental results in [Sch13a], [Sch13b], [Sch13c], [Sch13d], [Sch15], [Sch16] were compiled and run only on the specific Linux distribution used for the experiments. Note that in some versions of TRP++UC BENCHMARKING may be #defined in src/main_aux.cc for use in experimental evaluations. For normal use #undef BENCHMARKING in src/main_aux.cc. ================================================================================ 3. EXAMPLES ================================================================================ The benchmarks used in the experiments of [Sch13a], [Sch13b], [Sch13c], [Sch13d], [Sch15], [Sch16] are available from [trp++uc]. More examples (in particular, also satisfiable ones) can be obtained from [atva]. For examples in SNF see [trp++]. ================================================================================ 4. LEARNING MORE ================================================================================ TRP++UC is described in two papers: [Sch15,Sch13a] explains extraction of unsatisfiable cores for LTL via temporal resolution, and [Sch16,Sch13c] describes how to obtain information on when parts of an unsatisfiable core are relevant for unsatisfiability. To learn about unsatisfiable cores for LTL please refer to [Sch12]. For a description of TRP++ see [HK03,HK04]. Temporal resolution in general is explained in [FDP01,Fis91]; BFS loop search as used in TRP++ is described in [Dix98,Dix97,Dix95]. A comparison of the performance of various satisfiability solvers for LTL including TRP++ can be found in [SD11]. An overview of temporal logic is given in [Eme90]. ================================================================================ 5. GENEALOGY ================================================================================ TRP++UC was obtained by extending TRP++ [HK03,trp++] by Boris Konev and Ullrich Hustadt with extraction of unsatisfiable cores and reading of LTL formulas directly in the main tool (rather than translating them to SNF via a separate program). The implementation for reading LTL formulas reuses some code from TSPASS [LH10,tspass] by Michel Ludwig and Ullrich Hustadt; it also reuses many ideas from Boris Konev's translator from LTL to SNF [trp++]. Besides those two extensions the only major change between TRP++ and TRP++UC is an upgrade to the Boost version native to the user's installation. This version of TRP++UC was based on TRP++ version 2.1. On a cursory inspection it seems to me that essentially the difference between TRP++ version 2.1 and 2.2 is a bug fix backported from TRP++UC. ================================================================================ 6. VERSIONS ================================================================================ trp++uc-v2.1-YYYYMMDD.tar.bz2 Current version released on DD.MM.YYYY. trp++uc-THEORETICALCOMPUTERSCIENCE16.tar.bz2 Version used to obtain the experimental results in [Sch16]. trp++uc-ACTAINFORMATICA15.tar.bz2 Version used to obtain the experimental results in [Sch15]. trp++uc-TIME13.tar.bz2 Version used to obtain the experimental results in [Sch13d]. trp++uc-QAPL13POSTPROCEEDINGS.tar.bz2 Version used to obtain the experimental results in [Sch13c]. trp++uc-NFM13_QAPL13.tar.bz2 Version used to obtain the experimental results in [Sch13a] and [Sch13b]. ================================================================================ 7. ACKNOWLEDGMENTS ================================================================================ I am grateful to Boris Konev and Michel Ludwig for discussions and for releasing the source code of TRP++ and TSPASS including their LTL translators. Alessandro Cimatti brought up the subject of temporal resolution and suggested to see a resolution graph as a regular language acceptor. Initial parts of the work were performed while working under a grant by the Provincia Autonoma di Trento (project EMTELOS). ================================================================================ 8. CONTACT ================================================================================ TRP++UC was written by Viktor Schuppan. Please send bug reports, comments, questions, etc to Viktor.Schuppan@gmx.de ================================================================================ 9. COPYRIGHT AND LICENSES ================================================================================ For copyright and license information see the top of each file. In existing or factored out files that I changed I only added myself to the copyright holders but did not change any licenses. I.e., files from TRP++ are still GPLv2+ and files from TSPASS are still GPLv3+. New files are GPLv3+. More formally: TRP++UC is licensed under the GNU General Public License version 3 (GPLv3) or, at your option, any later version. See the file COPYING for a copy of the GNU GPLv3. The parts of TRP++ version 2.1 used are licensed under the GNU General Public License version 2 (GPLv2) or, at your option, any later option. See the file gpl-2.0.txt for a copy of the GNU GPLv2. The parts of TSPASS version 0.95-0.17 used are licensed under the GNU General Public License version 3 (GPLv3) or, at your option, any later version. See the file COPYING for a copy of the GNU GPLv3. ================================================================================ 10. REFERENCES ================================================================================ [atva] http://www.schuppan.de/viktor/atva11/ [Dix95] C. Dixon: Strategies for Temporal Resolution. PhD thesis. Department of Computer Science, University of Manchester, 1995. [Dix97] C. Dixon: Using Otter for Temporal Resolution. In: H. Barringer, M. Fisher, D. Gabbay, and G. Gough (eds.): ICTL, pp. 149–166. Applied Logic Series. Kluwer, 1997. [Dix98] C. Dixon: Temporal Resolution Using a Breadth-First Search Algorithm. In: Ann. Math. Artif. Intell. 22 (1-2) 1998, pp. 87–115. [Eme90] E. Emerson: Temporal and Modal Logic. In: J. van Leeuwen (ed.): Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995–1072. Elsevier and MIT Press, 1990. [FDP01] M. Fisher, C. Dixon, and M. Peim: Clausal temporal resolution. ACM Trans. Comput. Log. 2 (1) 2001, pp. 12-56. [Fis91] M. Fisher: A Resolution Method for Temporal Logic. In: J. Mylopoulos and R. Reiter (eds.): Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991). Sydney, Australia, August 24-30, 1991, pp. 99-104. Morgan Kaufmann, 1991. [HK03] U. Hustadt and B. Konev: TRP++ 2.0: A Temporal Resolution Prover. In: F. Baader (ed.): Automated Deduction - CADE-19, 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 - August 2, 2003. Proceedings. Volume 2741 of Lecture Notes in Computer Science, pp. 274-278. Springer, 2003. [HK04] U. Hustadt and B. Konev: TRP++: A temporal resolution prover. In: M. Baaz, J. Makowsky, and A. Voronkov (eds.): Collegium Logicum, Vol. 8, pp. 65-79. Kurt G\"odel Society, 2004. [LH10] M. Ludwig and U. Hustadt: Implementing a fair monodic temporal logic prover. AI Commun 23 (2-3) 2010, pp. 69-96. [Sch12] V. Schuppan: Towards a Notion of Unsatisfiable and Unrealizable Cores for LTL. In: G. Sala\"un, F. Arbab, M. Sirjani (eds.): Selected Papers from Foundations of Coordination Languages and Software Architectures (FOCLASA'09), Selected Papers from Fundamentals of Software Engineering (FSEN'09), Science of Computer Programming 77 (7-8) 2012: pp. 908-939. Elsevier, 2012. [Sch13a] V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. Available from http://arxiv.org/abs/1212.3884v1. [Sch13b] V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: L. Bortolussi and H. Wiklicky (eds.): Preliminary Proceedings of the Eleventh International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013, Rome, Italy, March 23-24, 2013. [Sch13c] V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: L. Bortolussi, H. Wiklicky (eds.): Proceedings of the Eleventh International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013, Rome, Italy, March 23-24, 2013. Volume 117 of Electronic Proceedings in Theoretical Computer Science, pp. 49-65. Open Publishing Association, 2013. [Sch13d] V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. In: C. Sanchez, B. Venable, E. Zimanyi (eds.): Proceedings of the 20th International Symposium on Temporal Representation and Reasoning, TIME 2013, Pensacola, FL, USA, September 26-28, 2013, pp. 54-61. IEEE Computer Society, 2013. [Sch15] V. Schuppan: Extracting Unsatisfiable Cores for LTL via Temporal Resolution. In: C. Sanchez, B. Venable, E. Zimanyi (eds.): Special Issue: Temporal Representation and Reasoning (TIME'13) - Part 2, Acta Informatica 53 (3) 2016: pp. 247-299. Springer, 2015. doi:10.1007/s00236-015-0242-1 [Sch16] V. Schuppan: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance. In: N. Bertrand, L. Bortolussi and H. Wiklicky (eds.): Quantitative Aspects of Programming Languages and Systems (2013-14), Theoretical Computer Science 655, Part B: pp. 155-192. Elsevier, 2016. doi: 10.1016/j.tcs.2016.01.014 [SD11] V. Schuppan and L. Darmawan: Evaluating LTL Satisfiability Solvers. In: T. Bultan, P. A. Hsiung (eds.): Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Volume 6996 of Lecture Notes in Computer Science, pp. 397-413. Springer, 2011. [trp++] http://cgi.csc.liv.ac.uk/~konev/software/trp++/ [trp++uc] http://www.schuppan.de/viktor/trp++uc/ [tspass] http://cgi.csc.liv.ac.uk/~michel/software/tspass/ ================================================================================ Viktor Schuppan Füssen, Germany, 14 December 2016 Viktor.Schuppan@gmx.de http://www.schuppan.de/viktor/ ================================================================================