Propositional Linear Temporal Logic with Initial Validity Semantics1

Mariusz Giero

Formalized Mathematics (2015)

  • Volume: 23, Issue: 4, page 379-386
  • ISSN: 1426-2630

Abstract

top
In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model while normal semantics means that we define the validity as satisfaction in all states of model. We prove the Deduction Theorem, and the soundness and completeness of the introduced formal system. We also prove some theorems to compare both formal systems, i.e., the one introduced in the article [10] and the one introduced in this article. Formal systems for temporal logics are applied in the verification of computer programs. In order to carry out the verification one has to derive an appropriate formula within a selected formal system. The formal systems introduced in [10] and in this article can be used to carry out such verifications in Mizar [4].

How to cite

top

Mariusz Giero. "Propositional Linear Temporal Logic with Initial Validity Semantics1." Formalized Mathematics 23.4 (2015): 379-386. <http://eudml.org/doc/276869>.

@article{MariuszGiero2015,
abstract = {In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model while normal semantics means that we define the validity as satisfaction in all states of model. We prove the Deduction Theorem, and the soundness and completeness of the introduced formal system. We also prove some theorems to compare both formal systems, i.e., the one introduced in the article [10] and the one introduced in this article. Formal systems for temporal logics are applied in the verification of computer programs. In order to carry out the verification one has to derive an appropriate formula within a selected formal system. The formal systems introduced in [10] and in this article can be used to carry out such verifications in Mizar [4].},
author = {Mariusz Giero},
journal = {Formalized Mathematics},
keywords = {temporal logic; very strict until operator; completeness},
language = {eng},
number = {4},
pages = {379-386},
title = {Propositional Linear Temporal Logic with Initial Validity Semantics1},
url = {http://eudml.org/doc/276869},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Mariusz Giero
TI - Propositional Linear Temporal Logic with Initial Validity Semantics1
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 4
SP - 379
EP - 386
AB - In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model while normal semantics means that we define the validity as satisfaction in all states of model. We prove the Deduction Theorem, and the soundness and completeness of the introduced formal system. We also prove some theorems to compare both formal systems, i.e., the one introduced in the article [10] and the one introduced in this article. Formal systems for temporal logics are applied in the verification of computer programs. In order to carry out the verification one has to derive an appropriate formula within a selected formal system. The formal systems introduced in [10] and in this article can be used to carry out such verifications in Mizar [4].
LA - eng
KW - temporal logic; very strict until operator; completeness
UR - http://eudml.org/doc/276869
ER -

References

top
  1. [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. Zbl06213858
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  3. [3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. 
  4. [4] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.[Crossref] Zbl06512423
  5. [5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990. 
  6. [6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. 
  7. [7] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. 
  8. [8] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  9. [9] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  10. [10] Mariusz Giero. The axiomatization of propositional linear time temporal logic. Formalized Mathematics, 19(2):113–119, 2011. doi:10.2478/v10037-011-0018-1.[Crossref] Zbl1276.03018
  11. [11] Adam Grabowski. Hilbert positive propositional calculus. Formalized Mathematics, 8(1): 69–72, 1999. 
  12. [12] Fred Kröger and Stephan Merz. Temporal Logic and State Systems. Springer-Verlag, 2008. Zbl1169.03001
  13. [13] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115–122, 1990. 
  14. [14] Andrzej Trybulec. Defining by structural induction in the positive propositional language. Formalized Mathematics, 8(1):133–137, 1999. 
  15. [15] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  16. [16] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733–737, 1990. 
  17. [17] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.