<abstract xmlns="http://www.w3.org/1999/xhtml">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].</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].

Propositional Linear Temporal Logic with Initial Validity Semantics<xref ref-type="fn" rid="fn1_w2aab2b8c16b1b7b1ab1aaAa">1</xref>

Faculty of Economics and Informatics, University of Białystok, Kalvariju 135, LT-08221 Vilnius, Lithuania

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Propositional Linear Temporal Logic with Initial Validity Semantics

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...

Propositional Linear Temporal Logic with Initial Validity Semantics¹

Publié en ligne: 25 mars 2016

Pages: 379 - 386

Reçu: 22 oct. 2015

DOI: https://doi.org/10.1515/forma-2015-0030

Mots clés
temporal logic, very strict until operator, completeness

© 2015 Mariusz Giero, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Propositional Linear Temporal Logic with Initial Validity Semantics1

Publié en ligne: 25 mars 2016

Pages: 379 - 386

Reçu: 22 oct. 2015

DOI: https://doi.org/10.1515/forma-2015-0030

Mots cléstemporal logic, very strict until operator, completeness

© 2015 Mariusz Giero, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Propositional Linear Temporal Logic with Initial Validity Semantics¹

Mots clés
temporal logic, very strict until operator, completeness