Многоагентная логика линейного нерефлексивного нетранзитивного времени LTK.sl: семантика, унификация и свойство конечной модели