Document Open Access Logo

Simplifying Inductive Schemes in Temporal Logic

Authors Pablo Cordero , Inmaculada Fortes , Inmaculada P. de Guzmán , Sixto Sánchez

PDF
Thumbnail PDF

File

LIPIcs.TIME.2019.19.pdf
  • Filesize: 0.5 MB
  • 13 pages

Document Identifiers

Author Details

Pablo Cordero
  • Dept. Applied Mathematic, University of Málaga, Spain
Inmaculada Fortes
  • Dept. Applied Mathematic, University of Málaga, Spain
Inmaculada P. de Guzmán
  • Dept. Applied Mathematic, University of Málaga, Spain
Sixto Sánchez
  • Dept. Applied Mathematic, University of Málaga, Spain

Funding

  • Cordero, Pablo: Partially supported by Project TIN2017-89023-P of the Science and Innovation Ministry of Spain, co-funded by the EU Regional Development (ERDF).
  • Fortes, Inmaculada: Partially supported by Project PGC2018-095869-B-I00 of the Science and Innovation Ministry of Spain.
  • de Guzmán, Inmaculada P.: Partially supported by Project TIN2017-89023-P of the Science and Innovation Ministry of Spain, co-funded by the EU Regional Development (ERDF).

Cite AsGet BibTex

Pablo Cordero, Inmaculada Fortes, Inmaculada P. de Guzmán, and Sixto Sánchez. Simplifying Inductive Schemes in Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TIME.2019.19

Abstract

In propositional temporal logic, the combination of the connectives "tomorrow" and "always in the future" require the use of induction tools. In this paper, we present a classification of inductive schemes for propositional linear temporal logic that allows the detection of loops in decision procedures. In the design of automatic theorem provers, these schemes are responsible for the searching of efficient solutions for the detection and management of loops. We study which of these schemes have a good behavior in order to give a set of reduction rules that allow us to compute these schemes efficiently and, therefore, be able to eliminate these loops. These reduction laws can be applied previously and during the execution of any automatic theorem prover. All the reductions introduced in this paper can be considered a part of the process for obtaining a normal form of a given formula.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Linear Temporal Logic
  • Inductive Schemes
  • Loop-check

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Kyungmin Bae and José Meseguer. Model checking linear temporal logic of rewriting formulas under localized fairness. Science of Computer Programming, 99:193-234, 2015. URL: https://doi.org/10.1016/j.scico.2014.02.006.
  2. Philippe Balbiani, Andreas Herzig, François Schwarzentruber, and Nicolas Troquard. DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE. CoRR, abs/1411.7825, 2014. URL: http://arxiv.org/abs/1411.7825.
  3. Nikolaj Bjorner, Anca Browne, Eddie Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny B. Sipma, and Tomás E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems: Deductive-algorithmic verification of reactive and real-time systems. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 415-418. Springer Berlin Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61474-5_92.
  4. Alfredo Burrieza and Inma Pérez de Guzmán. A new algebraic semantic approach and some adequate connectives for computation with temporal logic over discrete time. Journal of Applied Non-Classical Logics, 2(2):181-200, 1992. URL: https://doi.org/10.1080/11663081.1992.10510781.
  5. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst., 8(2):244-263, April 1986. URL: https://doi.org/10.1145/5397.5399.
  6. Pablo Cordero, Manuel Enciso, and Inma Pérez de Guzmán. Bases for closed sets of implicants and implicates in temporal logic. Acta Inf., 38(9):599-619, 2002. URL: https://doi.org/10.1007/s00236-002-0087-2.
  7. Anatoli Degtyarev, Michael Fisher, and Boris Konev. A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. In Uwe Egly and Chritian G. Fermüller, editors, Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of Lecture Notes in Computer Science, pages 85-99. Springer Berlin Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45616-3_7.
  8. Stéphane Demri and Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation, 174(1):84-103, 2002. URL: https://doi.org/10.1006/inco.2001.3094.
  9. Razvan Diaconescu. Structural induction in institutions. Information and Computation, 209(9):1197-1222, 2011. URL: https://doi.org/10.1016/j.ic.2011.06.002.
  10. Stephan Falke and Deepak Kapur. Rewriting Induction + Linear Arithmetic = Decision Procedure. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 241-255. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_20.
  11. Michael Fisher. An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, 2011. Google Scholar
  12. Michael Fisher, Clare Dixon, and Martin Peim. Clausal Temporal Resolution. ACM Trans. Comput. Logic, 2(1):12-56, 2001. URL: https://doi.org/10.1145/371282.371311.
  13. Nicoletta De Francesco, Antonella Santone, and Gigliola Vaglini. A user-friendly interface to specify temporal properties of concurrent systems. Information Sciences, 177(1):299-311, 2007. URL: https://doi.org/10.1016/j.ins.2006.03.008.
  14. Richard Jensen, Andrew Tuson, and Qiang Shen. Finding rough and fuzzy-rough set reducts with SAT. Information Sciences, 255(0):100-120, 2014. URL: https://doi.org/10.1016/j.ins.2013.07.033.
  15. Hans Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Ucla, 1968. Google Scholar
  16. Savas Konur. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Science, 7(3):370-403, 2013. URL: https://doi.org/10.1007/s11704-013-2195-2.
  17. Artur Meski, Wojciech Penczek, and Grzegorz Rozenberg. Model checking temporal properties of reaction systems. Information Sciences, 313:22-42, 2015. URL: https://doi.org/10.1016/j.ins.2015.03.048.
  18. Manuel Enciso Pablo Cordero and Inmaculada P. de Guzmán. From the poset of literals to a temporal negative normal form. Reports on Mathematical Logic, 36:3-53, 2002. Google Scholar
  19. Amir Pnueli. The temporal logic of programs. In Foundations of Computer Science, 1977., 18th Annual Symposium on, pages 46-57, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  20. José Manuel Rodríguez-Jiménez, Pablo Cordero, Manuel Enciso, and Angel Mora. Negative Attributes and Implications in Formal Concept Analysis. In Fuad Aleskerov, Yong Shi, and Alexander Lepskiy, editors, Proceedings of the Second International Conference on Information Technology and Quantitative Management, ITQM 2014, National Research University Higher School of Economics (HSE), Moscow, Russia, June 3-5, 2014, volume 31 of Procedia Computer Science, pages 758-765. Elsevier, 2014. URL: https://doi.org/10.1016/j.procs.2014.05.325.
  21. A. P. Sistla and E. M. Clarke. The Complexity of Propositional Linear Temporal Logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact