Grouping based calculus for propositional linear temporal logic
In this paper, the authors research the problem of loops in linear temporal logic PLTL. The task involves defining the standard rule application process for the derivation procedure (as used in [4] and [5]), determining and proving properties for the absence of a loop beneath some sequent, and crea...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Vilnius University Press
2024-12-01
|
| Series: | Lietuvos Matematikos Rinkinys |
| Subjects: | |
| Online Access: | https://ojs.test/index.php/LMR/article/view/37368 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | In this paper, the authors research the problem of loops in linear temporal logic PLTL. The task involves defining the standard rule application process for the derivation procedure (as used in [4] and [5]), determining and proving properties for the absence of a loop beneath some sequent, and creating a new calculus G*TL, which uses the proposed sequent grouping method, along with the method of marks (similar marking concepts were proposed in [5] and [6]). A new type of structural rule (GROUP), along with a modification of the rule (∘) to (∘*) is introduced. Finally, it is shown that the loop checking mechanism used in calculus G*TL is efficient, comparing it with other known calculi for logic PLTL.
|
|---|---|
| ISSN: | 0132-2818 2335-898X |