Intransitive Temporal Multi-agent Logic with Agents' Multi-valuations. Decidability

We study intransitive temporal multi-agent logic with agents' multi-valuations for letters and formulas. In previous wide accepted research the time and knowledge primarily were modeled by Kripke models with structure looking as simply a single time cluster with multi-relations for agents' accessibility relations. Here we develop this approach and use Kripke models with linear intransitive time and states represented by arbitrary time clusters for agents accessibility multi-relations. This logic is defined in a semantic way, as a set of formulas, which are true at linear models with multi-valued variables by agents' and clusters of states. We propose a background for such approach and a technique for computation truth values of formulas. Main result concerns decidability problem. We prove that the resulting logic is decidable and obtain a sort of finite model property.