Finite model property and unification for temporal logic of knowledge $LTK.sl_U$

Simultaneously with the development of computer networks and an increase in the amount of data with which they operate, there is a growing demand for the specification of systems that allow simulating their operations and internal structure.
In this regard, the popular and comfortable-to-use logical systems $\mathcal{LTL}$ and $\mathcal{CTL}$ demonstrate the limitations of their expressive capabilities: convenient properties of reflexivity and transitivity of the models for these logics become an obstacle in conditions of possible data loss and errors when working with them.
An alternative in this situation can be offered by logics that don't have these "good" properties. However, in this case many basic methods and approaches often become inapplicable.
In our study, we propose a semantic description for linear step-like temporal multi-agent logic with the universal modality $\mathcal{LTK}.sl_U$ based on the idea of non-reflexive non-transitive nature of time [1]. For this system, it was possible to establish a finite model property and to obtain a projectivity — an important result from the theory of unification.

Список литературы

1. Stepan I. Bashmakov, “Unification in linear modal logic on non-transitive time with the universal modality”, Журн. СФУ. Сер. Матем. и физ., 11:1 (2018), 3–9